nLab
induction

Idea

In the category Set, the initial algebra for the endofunctor $F:X\to 1+X$ is $⟨0,s⟩:1+\mathbb{N}\to \mathbb{N}$, where $\mathbb{N}$ is the set of natural numbers, $0$ is the smallest natural number, and $s$ is the successor operation. The principle of induction states 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.

More generally, the corresponding property of any initial algebra may be called induction. We then have induction over lists, trees, terms in a logic, and so on.

The dual notion is that of coinduction.

Related concepts

• inductive type

References

• 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)