Go backward to 4 NumbersGo up to TopGo forward to 6 More on Functions |

The domain of natural numbers has a property (implied by the first two Peano
axioms) that allows us to *define functions and predicates inductively*,
i.e., by sets of equations respectively equivalences with a particular
structure. Likewise, the third Peano axiom give us *induction* as a
technique for proving properties about natural numbers. In this chapter, we
investigate these two aspects of induction, defining and proving, and
demonstrate their relationship by proving properties of inductively/recursively
defined functions. We also generalize the concept of inductive definitions and
proofs from natural numbers to *inductively defined sets* which are
prominent in computer science.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999