nLab
induction

This entry is about induction in the sense of logic. For induction (functors) in representation theory see induced module, induced comodule, cohomological induction.

---

Idea

The principle of induction says that if a proposition $n\in \mathbb{N}⊢P(n)$ that depends on the natural numbers has the property that

1. it is true for $0\in \mathbb{N}$;

2. 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.

The dual notion is that of coinduction.

Formalization

By initial algebras over endofunctors

The induction principle my neatly be formalized in terms of the notion of initial algebras of an endofunctor.

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.

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.

Related concepts

• deduction

• inductive type

• inductive definition

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)