Page 319 of 800
| Page 319 of 800 | Search internet |
The following constructs allow to assume a premise P:
line L : Premise >> P ; N
Example:
In Line L02 we assume 
as a premise.
In Line L03 we use modus ponens 
on Axioms 
and the premise to conclude 
. as well as belong to propositional calculus 
.
In Line L04 we conclude 
by definition (Rule 
).
Using a premise is the typical way to prove a lemma of form 
.
Line L01 assumes propositional calculus as a premise. To Logiweb sequent calculus, assuming a theory is a premise like any other premise.
The lemma states 
. Since 
is right associative, that means 
.
Tactic evaluation of
line L : Premise >> P ; N
is done by the tactic-premise-line function from the check page. That function adds an association from L to P in the tactic state and then tactic evaluates N. After tactic evaluation of N, tactic-premise-line adds the sequent operator needed for assuming the premise P.
During tactic evaluation of Line L03 in the proof above, the tactic state contains an association from L01 to and from L02 to . Thus, when the argumentation in Line L03 refers to L02, the tactic evaluation can look up what L02 means in the tactic state.
See the section on hypotheses for a comparison of premises and hypotheses.
Do not use premises in proof of form
T proof of L : P
where T is Prop, FOL, or Peano from the Peano page. The tactics of Prop, FOL, and Peano are not intended to be used together with premisses.
| Page 319 of 800 | Search logiweb.eu |