Logiweb(TM)

8.6.5 Line L02 of 3.2a'

Prev Up Next Page 351 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 L02, the FOL rule unitac changes S1 into A1' ponens S1 as before. Then x mp y applies Lemma MP'. Lemma MP' is modus ponens enriched by a hypothesis #h:

Prop lemma MP' : All #h ,, #a ,, #b : #h imply #a imply #b infer #h imply #a infer #h imply #b end lemma prepare proof indentation,proof of MP' : line L01 : Premise >> Prop ; line L02 : Arbitrary >> #h ,, #a ,, #b ; line L03 : Premise >> #h imply #a imply #b ; line L04 : Premise >> #h imply #a ; line L05 : A2 >> ( #h imply #a imply #b ) imply ( #h imply #a ) imply #h imply #b ; line L06 : MP ponens L05 ponens L03 >> ( #h imply #a ) imply #h imply #b ; line L07 : MP ponens L06 ponens L04 >> #h imply #b qed

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

PA lemma 3.2aL02 : tt imply x = x end lemma

prepare proof indentation,proof of 3.2aL02 : 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 qed

Prev Up Next Page 351 of 800 Search logiweb.eu

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