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 Ms=
{ t | Ps(t) }. Then P is
true of all ground -terms if M is a -algebra.
[Prev] [Home] [BHome]