|Page 349 of 800||Search internet|
Proofs stated using the FOL tactic are more convenient but less general than proofs stated directly in the sequent calculus. The FOL tactic is suited for reasoning inside first order theories but is unsuited for meta-reasoning about first order theories. If one needs to state metatheorems about e.g. Peano Arithmetic, one has to resort to sequent proofs of to tailor-made meta-theories expressed on top of the sequent calculus.
To see how the the FOL tactic works, consider the following proof:
The proof is tactic expanded by the FOL tactic because the proof has form and because the Peano page defines the tactic aspect of to be .
After tactic expansion, the proof resembles this proof:
The proof proceeds thus:
Without Line L92 and L93, the PA proof would only be able to reference PA lemmas. In first order theories, however, it is convenient to be able to use also Prop and FOL lemmas. In that way, tautologies and theorems which hold in all first order theories only need to be proved once.
The dummy hypothesis introduced in Line L01, L02, and L03 serve as a preparation for doing hypothetical reasoning. This will be explained in more detail later.
The proof of above macro expands into a definition of the 'proof' aspect of .
There are two proofs of above, however. One which is correct, and one in which is formally incorrect because argumentations are replaced by ellipses .
If you put your mouse over the formally incorrect proof above, you will see that the proof is enclosed in a
construct. The hide...end hide construct hides definitions from harvesting. In particular, it hides proofs so the hide construct can be used for including formally incorrect proofs in a text.
|Page 349 of 800||Search logiweb.eu|