Go backward to 4 Numbers Go up to Top Go 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.