8.4.4 Premises

Prev Up Next Page 319 of 800 Search internet

The following constructs allow to assume a premise P:

   line L : Premise >> P ; N


Prop lemma PremiseExample : #y infer #x or #y end lemma

prepare proof indentation,proof of PremiseExample : line L01 : Premise >> Prop ; line L02 : Premise >> #y ; line L03 : MP ponens A1 ponens L02 >> not #x imply #y ; line L04 : Def ponens L03 >> #x or #y qed

In Line L02 we assume #y as a premise.

In Line L03 we use modus ponens MP on Axioms A1 and the premise to conclude #y imply not #x imply #y. MP as well as A1 belong to propositional calculus Prop.

In Line L04 we conclude #y infer #x or #y by definition (Rule Def).

Using a premise is the typical way to prove a lemma of form A infer B.

Line L01 assumes propositional calculus Prop as a premise. To Logiweb sequent calculus, assuming a theory is a premise like any other premise.

The lemma states Prop infer #y infer #x or #y. Since empty infer empty is right associative, that means Prop infer ( #y infer #x or #y ).

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 Prop and from L02 to #y. 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.

Prev Up Next Page 319 of 800 Search logiweb.eu

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