Logiweb(TM)

8.2.5 Side conditions

Prev Up Next Page 308 of 800 Search internet


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

x avoid y
This side conditions expresses that x avoids (i.e. does not occur free in) y. The side condition is useful to express Mendelsons axiom A5: All #x ,, #a ,, #b : #x avoid #a endorse all #x : ( #a imply #b ) imply #a imply all #x : #b.
sub ( a , b , x , t )
This side condition expresses that a is equal to the result of replacing x by t in b (with renaming of bound variables). The side condition is useful to express Mendelsons axiom A4: All #t ,, #x ,, #a ,, #b : sub ( #b , #a , #x , #t ) endorse all #x : #a imply #b. The side condition is also useful for expressing the axiom of induction in which one has to replace the induction variable x by 0 and x suc.
def ( x , y )
This side condition expresses that x and y are identical except for application of 'math' definitions. The side condition is useful for expressing the 'definition' rule All #x ,, #y : def ( #x , #y ) endorse #x infer #y 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:

math define x or y as not x imply y end define

The definition defines the 'math/kg' aspect of x or y to be not x imply y. The definition has no effect in itself but has effect through the definition rule. As an example, one may use Mendelsons axiom A1 to prove #b imply ( not #a imply #b ) and then use the definition rule to conclude #b imply ( #a or #b )

For examples of use see Prop, FOL and Peano.

Prev Up Next Page 308 of 800 Search logiweb.eu

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