Logiweb(TM)

6.7.10 Line L09 of the proof

Prev Up Next Page 96 of 800 Search internet


Recall the proof of 3.2l:

prepare proof indentation,PA proof of 3.2l : line L01 : S7 >> 0 * 0 = 0 ; line L02 : Block >> Begin ; line L03 : Hypothesis >> 0 * x = 0 ; line L04 : S8 >> 0 * x suc = 0 * x + 0 ; line L05 : S5 >> 0 * x + 0 = 0 * x ; line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ; line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ; line L08 : Block >> End ; line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ; line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed

Line L09 references Lemma Induction which says:

PA lemma Induction : All #x ,, #h ,, #a ,, #z ,, #i : sub ( #z , #a , #x , 0 ) endorse sub ( #i , #a , #x , #x suc ) endorse #x avoid #h endorse #h imply #z infer #h imply #a imply #i infer #h imply #a end lemma

The unification tactic is not smart enough to see that induction is in x. Thus, the meta variable #x of the Induction lemma has to be instantiated to the object variable x explicitly. That is done by the instantiation operator "@" of the Logiweb sequent calculus in Line L09.

Apart from that, the unification tactic is smart enough to guess how all the other meta variables have to be instantiated. Furthermore, it guesses that the two side conditions have to be verified by evaluating them, so it adds two 'verify' sequent operators x Verify. The verify sequent operator eliminates a side condition by evaluating it and checking that the result is true. Finally, the unification tactic uses meta modus ponens two times to get rid of the two premisses. The #h in the Induction rules allows to do induction under an arbitrary hypothesis #h. That is needed if induction is used inside a hypothetical proof.

Prev Up Next Page 96 of 800 Search logiweb.eu

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