Induction is only valid for proving sentences about algebras that are definable with initial semantics. In our applications, the data algebra is usually defined this way, and so proofs by induction are valid for it. For example, the integers or naturals are often part of the data algebra, and lemmas about them are usually needed for all but the simplest proofs.

Initial specifications generally have more than one induction scheme; even the natural numbers have many different schemes. The most familiar one proves P(n) for all n by proving P(0) and then proving that P(n) implies P(s n). However, we could instead prove P(0) and P(s 0), and then prove that P(n) implies P(s s n). These two schemes correspond to different choices of generators: the first takes 0, s as generators, while the second takes 0, s0, ss. There are infinitely many such schemes.

[Prev] [Home] [BHome]

28 October 1996