Logiweb(TM)

6.7.6 Line L02-L08 of the proof

Prev Up Next Page 92 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 L02-L08 constitute a block, i.e. a proof within the proof. The 'block begin' in Line L02 and the 'block end' in Line L08 are part of the same, syntactic construct.

The construct used for expressing Line L01 reads:

   line l : a >> x ; n

where l is L01, a is S7, x is 0 * 0 = 0, and n is the rest of the proof (Line L02-L10). The construct used for expressing the block reads:

   line l : Block >> Begin ; x line k : Block >> End ; n

where l is L02, x is the block (Line L03-L07), k is L08, and n is the rest of the proof (Line L09-L10).

The block proves 0 * x = 0 imply 0 * x suc = 0. The line number at the end of the block can be used for referring to this conclusion as is done in Line L09.

The line number L02 at the beginning of the block is purely decorative.

Peano arithmetic PA itself does not permit blocks and hypothetical reasoning. But PA satisfies the deduction theorem of first order predicate calculus which says that proofs which do contain blocks can be translated into proofs which do not contain blocks.

Mendelson: 'Introduction to mathematical logic' contains a proof of the deduction theorem which translates a block containing n proof lines into a straight proof containing 3 * n + 2 proof lines.

It is legal to nest blocks or to have multiple hypotheses in one block. If one uses the algorithm of Mendelson on nested blocks or multiple hypotheses, one gets a blowup by a factor 3 for each hypothesis. The algorithm used by the tactic of FOL on the Peano page handles multiple hypotheses by forming a conjunction of all hypotheses. That is more complicated but avoids the exponential blowup.

Different theories may have different deduction theorems. The deduction theorem of first order predicate calculus FOL is slightly more complicated than that of the propositional calculus Prop. That is why FOL and Prop have slightly different proof level tactics as mentioned earlier.

Map theory is a radically different theory and has a radically different deduction theorem so it needs a radically different proof level tactic. Logiweb was originally developed to support map theory, so you would not have been able to use FOL deduction if deduction had been hardwired into the system.

Prev Up Next Page 92 of 800 Search logiweb.eu

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