## 8.2.5 Side conditions

Page 308 of 800 |
| Search internet |

The Peano page defines several side conditions. Here are some examples:

- This side conditions expresses that
*avoids* (i.e. does not occur free in) . The side condition is useful to express Mendelsons axiom : .
- This side condition expresses that is equal to the result of replacing by in (with renaming of bound variables). The side condition is useful to express Mendelsons axiom : . The side condition is also useful for expressing the axiom of induction in which one has to replace the induction variable by and .
- This side condition expresses that and are identical except for application of 'math' definitions. The side condition is useful for expressing the 'definition' rule which says that one can replace terms by their math definitions and vice versa. For an example, see below.

The Peano page contains the following definition:

The definition defines the 'math/kg' aspect of to be . The definition has no effect in itself but has effect through the definition rule. As an example, one may use Mendelsons axiom to prove and then use the definition rule to conclude

For examples of use see Prop, FOL and Peano.

Page 308 of 800 |
| Search logiweb.eu |

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