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.

A general definition of induction for (initial models of) a specification (,E) takes a little work: call a signature with equations G inductive for ( ,E) iff: (1) under the equations (E G) every ground ( )-term equals some -term; and (2) every ground -term equals some -term.

Now given an S-indexed family of predicates P on ground -terms, if (,G) is inductive for (,E), then we can prove P by the following induction scheme: show P(c) for each constant c in , and then show P(g(t1,...,tk)) for each g in , assuming P(ti) for each i and using (E G).

This gives the familiar induction schemes in the usual cases, noting that P is often defined to be true except on one particular sort.

To show soundness of this proof rule, we define an S-sorted set M of ground -terms by M_s= { t | P_s(t) }. Then P is true of all ground -terms if M is a -algebra.