When formulated in one of the formalizations below, one finds that this principle is but the simplest special case of a very general notion of induction over inductive types. Other examples are induction over lists, trees, terms in a logic, and so on.
In terms of this the principle of induction is equivalent to saying that there is no proper subalgebra of ; that is, the only subalgebra is itself. This follows from the general property of initial objects that monomorphisms to them are isomorphisms.
Jiří Adámek, Stefan Milius, Lawrence Moss, Initial algebras and terminal coalgebras: a survey (pdf)
Bart Jacobs, Jan Rutten, A tutorial on (co)algebras and (co)induction, pdf EATCS Bulletin (1997); extended and updated version: An introduction to (co)algebras and (co)induction, In: D. Sangiorgi and J. Rutten (eds), Advanced topics in bisimulation and coinduction, p.38-99, 2011, pdf 62 pp.
Revised on July 1, 2015 10:23:49
by Todd Trimble