Logiweb(TM)

6.7.7 Line L03 of the proof

Prev Up Next Page 93 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 L03 assumes 0 * x = 0 for the duration of the enclosing block. The hypothesis can be used in Line L04-L07. In the example above, the hypothesis is used in Line L07.

The Logiweb sequent calculus also permits hypothetical reasoning. Actually, it permits two kinds of hypothetical reasoning.

In the first kind of hypothetical reasoning, you assume a statement as a 'premise'. As an example, the proof above is one, big hypothetical proof which uses Peano arithmetic PA as premise. In other words, the proof takes as a premise that all rules of Peano arithmetic hold.

In the second kind of hypothetical reasoning, you assume a side condition as a 'condition'. As an example, you may assume that #x does not occur free in #a and then prove something under this condition.

Thus, you can use premisses and conditions at meta level and hypotheses at object theory level. The kind of hypothetical reasoning possible at object theory level depends on the object theory.

Prev Up Next Page 93 of 800 Search logiweb.eu

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