Page 324 of 800
| 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:
Using a hypothesis is the typical way to prove a lemma of form 
.
In contrast, a premise is the typical way to prove a lemma of form 
. 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.
| Page 324 of 800 | Search logiweb.eu |