8.6.3 Lemma 3.2a'

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:

Line L91

Here we assume so that the rules of are available.

Line L92

Here we use the Rule tactic to prove Prop. The Rule tactic takes as an argument the rule it is supposed to prove and then tries to look up that rule in all assumed theories. Since Prop is part of PA, the Rule tactic succeeds. After Line L92 we can use all Prop lemmas.

Line L93

After Line L93 we can use all FOL lemmas.

Line L01

This is like Line L01 in the unexpanded proof, but we prove under the dummy hypothesis .

Line L02-L03

This is like Line L01.

Line L99

Here we discard the dummy hypothesis so that the proof proves what it is supposed to prove.

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

hide...end hide

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