## 8.4.5 Conditions

Page 320 of 800 |
| Search internet |

The following constructs allow to assume that a side condition holds:

line L : Condition >> C ; N

Example:

We say that the variable *avoids* the term , written if the variable does not occur free in the term . The lemma above says that if avoids and if then . The proof of the lemma reads:

In Line L01 we assume that avoids .

In Line L02 we assume as a premise and in Line L03 we generalize the premise.

Axiom of first order predicate calculus says:

In Line L04 we use *modus probans* on Axiom and the side condition we assumed in Line L01. Finally, we use modus ponens on Line L04 and Line L03.

Using a condition is the typical way to prove a lemma of form .

Do not use conditions in proof of form

T proof of L : P qed

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 conditions.

Page 320 of 800 |
| Search logiweb.eu |

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