if it is true for $n \in \mathbb{N}$ then it is true for $n+1$;

then it is true for every $n \in \mathbb{N}$.

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 $\mathbb{N}$; that is, the only subalgebra is $\mathbb{N}$ 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
(67.81.95.215)