Logiweb(TM)

6.7.5 Line L01 of the proof

Prev Up Next Page 91 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 L01 says that 0 * 0 = 0 follows from rule S7. Rule S7 says

rule S7 : all x : x * 0 = 0 end rule,"\mbox{}"

Line L01 comprises a label L01, an argumentation S7, and a conclusion 0 * 0 = 0 bound together by a unification tactic "\gg".

The label L01 is a variable. You can use arbitrary variables as labels, so feel free to name your lines P or y _ { 117 } or whatever you like. The check page defines L00 to L99 as 100 individual variables.

Inside the proof, L01 can be used as shorthand for the conclusion 0 * 0 = 0.

The unification tactic "\gg" takes the argumentation S7 and the conclusion 0 * 0 = 0 and tries to prove the conclusion using the argumentation. The unification tactic returns an argumentation formulated as a Logiweb sequent term. At that time the conclusion has disappeared. The conclusion 0 * 0 = 0 is merely used by the unification tactic to see what to do with the argumentation. Later on, when the proof checker evaluates the sequent term returned by the unification tactic, the proof checker will see that the sequent term indeed proves 0 * 0 = 0.

During proof checking, the following happens:

The unitac of S7 knows that it is a unitac for a rule. So it first generates the Logiweb sequent operators needed for extracting the rule S7 from the theory at hand. So now we have a proof of all x : x * 0 = 0.

The unitac then compares all x : x * 0 = 0 with the expected conclusion 0 * 0 = 0 and sees that it must eliminate a quantifier. Thus, it generates a suitable instance of rule A4:

rule A4 : All #t ,, #x ,, #a ,, #b : sub ( #b , #a , #x , #t ) endorse all #x : #a imply #b end rule,"\mbox{}"

plus a suitable instance of modus ponens:

rule MP : All #x ,, #y : #x imply #y infer #x infer #y end rule,"\mbox{}"

The unification tactic uses unification to see that x has to be instantiated to 0. Thus, the metavariable #t in rule A4 is set to 0.

Rule A4 says that for all object terms #t, #x, #a, and #b, the side condition sub ( #b , #a , #x , #t ) endorses the conclusion all #x : #a imply #b. The side condition is true if #b is identical except for naming of bound variables to the result of replacing #x by #t in #a with suitable renaming of bound variables to avoid collisions. The "\Pi" is a meta-quantifier which quantifies over all object terms. The "\forall" is an object quantifier which belongs to first order predicate calculus and Peano arithmetic.

Rule MP says that if one has proved #x imply #y and #x then one is allowed to conclude #y by modus ponens.

Prev Up Next Page 91 of 800 Search logiweb.eu

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