Logiweb(TM)

8.6.6 Line L03 of 3.2a'

Prev Up Next Page 352 of 800 Search internet


Recall again 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 L03, the FOL rule unitac sees that Gen1 is a meta-theorem and thus passes it to the standard rule unitac. Lemma Gen1 is generalization enriched by a hypothesis #h:

FOL lemma Gen1 : All #h ,, #x ,, #a : #x avoid #h endorse #h imply #a infer #h imply all #x : #a end lemma

prepare proof indentation,proof of Gen1 : line L01 : Premise >> FOL ; line L02 : Arbitrary >> #h ,, #x ,, #a ; line L03 : Condition >> #x avoid #h ; line L04 : Premise >> #h imply #a ; line L05 : Gen ponens L04 >> all #x : ( #h imply #a ) ; line L06 : A5 probans L03 >> all #x : ( #h imply #a ) imply ( #h imply all #x : #a ) ; line L07 : MP ponens L06 ponens L05 >> #h imply all #x : #a qed

The number 1 in Gen1 indicates that the rule performs one generalization. The Peano page also defines Gen2 and Gen3 for performing 2 and 3 generalizations, respectively.

In conclusion, the proof expands into something like the following:

PA lemma 3.2aL03 : all x : x = x end lemma

prepare proof indentation,proof of 3.2aL03 : 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 ; line L02 : MP' ponens ( MP' ponens ( LAP4' ponens ( A1' ponens S1 ) ) ponens L01 ) ponens L01 >> tt imply x = x ; line L03 : Gen1 ponens L02 >> tt imply all x : x = x ; line L99 : LElimHyp ponens L03 >> all x : x = x qed

Prev Up Next Page 352 of 800 Search logiweb.eu

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