Logiweb(TM)

8.6.4 Line L01 of 3.2a'

Prev Up Next Page 350 of 800 Search internet


Recall the proofs of 3.2a':

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

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

In Line L01 we use S5 to prove x + 0 = x. After tactic expansion, Line L01 proves tt imply x + 0 = x. Axioms S5 says:

rule S5 : all x : x + 0 = x end rule

Thus, the tactic expanded argumentation in Line L01 must add tt imply *** and must eliminate the object quantifier in Axiom S5.

The FOL tactic installs non-standard lemma, rule, and conclude unitacs. The FOL rule unitac has standard behavior on meta-terms but a non-standard behavior on object terms. The contents of S5 is an object term and thus the FOL rule unitac applies its own, non-standard behavior and changes the argumentation into something like A1' ponens S5 where A1' is the following lemma:

Prop lemma A1' : All #h ,, #a : #a infer #h imply #a end lemma

prepare proof indentation,proof of A1' : line L01 : Premise >> Prop ; line L02 : Arbitrary >> #h ,, #a ; line L03 : Premise >> #a ; line L04 : MP ponens A1 ponens L03 >> #h imply #a qed

In that way, the FOL rule unitac changes all x : x + 0 = x to tt imply all x : x + 0 = x.

Then the FOL conclude unitac takes over and sees that it has to instantiate object quantifiers. It does so using parallel instantiation. Parallelism is unimportant in this case where only one quantifier is instantiated. The Fol conclude unitac changes A1' ponens S5 to something like LAP4' ponens ( A1' ponens S5 ) where LAP4' is the following lemma:

FOL lemma LAP4' : All #h ,, #a ,, #b : inst ( #a , #b ) endorse #h imply #a infer #h imply #b end lemma

prepare proof indentation,proof of LAP4' : line L01 : Premise >> FOL ; line L02 : Arbitrary >> #h ,, #a ,, #b ; line L03 : Condition >> inst ( #a , #b ) ; line L04 : Premise >> #h imply #a ; line L05 : AP4 probans L03 >> #a imply #b ; line L06 : Mend1.47b ponens L04 ponens L05 >> #h imply #b qed

Thus, the proof until Line L01 tactic expands into something like the following:

PA lemma 3.2aL01 : tt imply x + 0 = x end lemma

prepare proof indentation,proof of 3.2aL01 : line L91 : Premise >> PA ; line L92 : Prop Rule >> Prop ; line L93 : FOL Rule >> FOL ; line L01 : LAP4' ponens ( A1' ponens S5 ) >> tt imply x + 0 = x qed

Actually, the proof does not tactic expand to the proof above. Rather, it expands into a sequent proof which resembles what the proof above expands into.

Prev Up Next Page 350 of 800 Search logiweb.eu

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