Logiweb(TM)

8.6.7 Hypothetical reasoning

Prev Up Next Page 353 of 800 Search internet


Now consider the following proof:

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

prepare proof indentation,PA proof of 3.2d : line L00 : Block >> Begin ; line L01 : Hypothesis >> x = z ; line L02 : Hypothesis >> y = z ; line L03 : 3.2b mp L02 >> z = y ; line L04 : 3.2c mp L01 mp L03 >> x = y ; line L05 : Block >> End ; line L06 : Gen3 ponens L05 >> all x ,, y ,, z : ( x = z imply y = z imply x = y ) qed

After tactic expansion, the proof resembles this proof:

hide prepare proof indentation,proof of 3.2d : line L91 : Premise >> PA ; line L92 : Prop Rule >> Prop ; line L93 : FOL Rule >> FOL ; line L01 : *** >> tt and x = z imply x = z ; line L02 : *** >> tt and x = z and y = z imply y = z ; line L03 : *** >> tt and x = z and y = z imply z = y ; line L04 : *** >> tt and x = z and y = z imply x = y ; line L05 : *** >> tt imply x = z imply y = z imply x = y ; line L06 : *** >> tt imply all x ,, y ,, z : ( x = z imply y = z imply x = y ) ; line L99 : LElimHyp ponens L03 >> all x ,, y ,, z : ( x = z imply y = z imply x = y ) qed end hide

Each conclusion has the form that a hypothesis conjunction implies a consequence. The hypothesis conjunction starts out being the dummy hypothesis tt. One can then add conjuncts to the hypothesis conjunction by stating hypotheses as is done in Line L01 and L02. And one can subtract from the hypothesis conjunction by leaving a block.

Nothing particular happens when entering a block. But when leaving a block, the hypothesis conjunction is reset to the value it had when entering the block. Additional hypotheses made inside the block are moved from the hypothesis conjunction to the consequence. An example of this can be seen in Line L05 where two hypotheses are moved from hypothesis conjunction to consequence.

Furthermore, when leaving a block, the lines inside the block become inaccessible so that one cannot refer e.g. to Line L04 from Line L06 in the proof above. Nothing prevents lines inside a block from referencing lines that occur before the beginning of the block.

A mentioned earlier, the conclusions of proof lines are accumulated in s [[ !"pre" ]] of the tactic state s. The value of s [[ !"pre" ]] is a list of entries of form << l ,, c ,, a >> where l is the line number, c is the conclusion of the line, and a is an argumentation in the form of a sequent term to include in proofs whenever a the given line is referenced.

When leaving a block, s [[ !"pre" ]] is reset to the value it had before entering the block and then the conclusion of the block is added.

Each hypothesis line modifies all entries in s [[ !"pre" ]] by adding the hypothesis to each entry. As an example, Line L01 adds tt and x = z imply x = z to s [[ !"pre" ]] but Line L02 modifies the conclusion of Line L01 to tt and x = z and y = z imply x = z in s [[ !"pre" ]]. Line L02 also modifies the argumentation such that the argumentation proves the new conclusion.

Now consider Line L04 in the proof above. The argumentation refers to Line L01 and L03. Due to the modifications to s [[ !"pre" ]] made by Line L02, both L01 and L03 have hypothesis tt and x = z and y = z imply x = z when seen from Line L04.

The modifications done by Line L02 disappear when leaving the block because s [[ !"pre" ]] is reset to the value it had before entering the block. The conclusion of the block is added after resetting s [[ !"pre" ]] so that one can use the result of the block.

Prev Up Next Page 353 of 800 Search logiweb.eu

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