8.6.3 Lemma 3.2a'

Prev Up Next 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:

PA lemma 3.2a' : all x : x = x end lemma

prepare proof indentation,PA proof of 3.2a' : line L01 : S5 >> x + 0 = x ; line L02 : S1 mp L01 mp L01 >> x = x ; line L03 : Gen1 ponens L02 >> all x : x = x qed

The proof is tactic expanded by the FOL tactic because the proof has form show PA proof of *** : *** end show and because the Peano page defines the tactic aspect of PA to be \ u . tactic-FOL ( u ).

After tactic expansion, the proof resembles this proof:

hide prepare proof indentation,proof of 3.2a' : line L91 : Premise >> PA ; line L92 : Prop Rule >> Prop ; line L93 : FOL Rule >> FOL ; line L01 : *** >> tt imply x + 0 = x ; line L02 : *** >> tt imply x = x ; line L03 : *** >> tt imply all x : x = x ; line L99 : LElimHyp ponens L03 >> all x : x = x qed end hide

The proof proceeds thus:

Line L91
Here we assume PA so that the rules of PA 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 x + 0 = x under the dummy hypothesis tt.
Line L02-L03
This is like Line L01.
Line L99
Here we discard the dummy hypothesis tt 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 tt 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 3.2a' above macro expands into a definition of the 'proof' aspect of 3.2a'.

There are two proofs of 3.2a' 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.

Prev Up Next Page 349 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05