Nuprl Definition : proveable

A generic definition of provability.
It says that a sequent is provable if there is a correct proof tree.
A proof tree proof-tree is a well-founded tree
(for those we use Martin-Lof's, W type, W)
with a sequent and a rule labeling each node.
The proof is correct for sequent s if the sequent labeling the top node is
s and for every node, the effect of the given rule on the given sequent
does not fail and the successors of the node
are correct proofs of the generated subgoal sequents.⋅

proveable(Sequent;Rule;effect;s) == ∃pf:{proof-tree(Sequent;Rule;effect)| correct_proof(Sequent;effect;s;pf)}

Definitions occuring in Statement : correct_proof: correct_proof(Sequent;effect;s;pf), proof-tree: proof-tree(Sequent;Rule;effect), sq_exists: ∃x:{A| B[x]}
Definitions occuring in definition : sq_exists: ∃x:{A| B[x]}, proof-tree: proof-tree(Sequent;Rule;effect), correct_proof: correct_proof(Sequent;effect;s;pf)
FDL editor aliases : proveable

Latex:
proveable(Sequent;Rule;effect;s) == \mexists{}pf:\{proof-tree(Sequent;Rule;effect)| correct\_proof(Sequent;effect;s;pf)\} Date html generated: 2016_07_08-PM-04_59_38 Last ObjectModification: 2015_09_23-AM-07_42_50 Theory : general Home Index