Page 92 of 800
| Page 92 of 800 | Search internet |
Recall the proof of 
:
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 
. 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 
itself does not permit blocks and hypothetical reasoning. But 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 
proof lines into a straight proof containing 
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 
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 is slightly more complicated than that of the propositional calculus 
. That is why and 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 deduction if deduction had been hardwired into the system.
| Page 92 of 800 | Search logiweb.eu |