Logiweb(TM)

8.4.9 Hypotheses

Prev Up Next Page 324 of 800 Search internet


The following constructs allow to assume a hypothesis H:

   line L : Hypothesis >> H ; N

The construct above is used for expressing Line L02 and L08 of the multzero proof:

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

Using a hypothesis is the typical way to prove a lemma of form A imply B.

In contrast, a premise is the typical way to prove a lemma of form A infer B. Premises are defined at the level of the Logiweb sequent calculus and is available in connection with any theory. Hypotheses are only available in theories which support them. Support for hypotheses both require the theory used to satisfy some deduction theorem and also requires the tactic for the theory to be able to expand blocks containing hypotheses into plain axioms and inference rules.

Only use hypotheses in proof of form

   T proof of L : P

where T is a theory which supports hypotheses. The Prop, FOL, and Peano theories from the Peano page are examples of such theories.

Prev Up Next Page 324 of 800 Search logiweb.eu

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