Logiweb(TM)

6.7.9 Line L06-L07 of the proof

Prev Up Next Page 95 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 L06 references Lemma 3.2c which says:

PA lemma 3.2c : all x ,, y ,, z : ( x = y imply y = z imply x = z ) end lemma

The unification tactic instantiates x, y, and z to 0 * x suc, 0 * x + 0, and 0 * x, respectively. The instantiation is 'parallel': first x, y, and z are instantiated to three fresh variables, and then those three fresh variables are instantiated to 0 * x suc, 0 * x + 0, and 0 * x, respectively. That is necessary to avoid problems when x, y, and z are replaced by terms which may themselves contain x, y, and z.

The unification tactic uses the conclusions of L04, L05, and L06 to guess the values for x, y, and z. If you make a bug, unification may be unable to find values for variables, and then you get an error message from the unification tactic.

The term x mp y denotes MP ponens x ponens y where MP is modus ponens of the object theory and x ponens y is the meta modus ponens operator of the Logiweb sequent calculus. Thus, x mp y denotes modus ponens in the object theory and x ponens y denotes meta modus ponens. Several concepts have versions both in the Logiweb sequent calculus and in FOL:

Operation Meta level Object level
Modus ponens x ponens y x mp y
Infer/Imply x infer y x imply y
Quantification All x : A all x : A
Conjunction x oplus y x and y
Falsehood False ff
Variable #x x

Prev Up Next Page 95 of 800 Search logiweb.eu

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