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.



The principle of induction says that if a property of the natural numbers

  1. is true for 00 \in \mathbb{N};

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

then it is true for every nn \in \mathbb{N}. The intuitive notion of a property is in practical mathematics identified with (belonging to) a subset SS\subseteq\mathbb{N}. Thus the mathematical induction says that if 0S0\in S and if n\forall n\in\mathbb{N} nSn+1Sn\in S\implies n+1\in S then S=S = \mathbb{N}. This is the way in the formal Dedekind-Peano arithmetics. Usually in logic one however uses a weaker form of induction which can be stated in a first order language (or in a type theory), namely where one limits to properties given by the predicates P(n)P(n) depending on natural numbers. The corresponding conclusion is the proposition nP(n)n \in \mathbb{N} \vdash P(n). The latter version of the principle of induction is weaker because there are only 0\aleph_0 predicates but 2 02^{\aleph_0} subsets of \mathbb{N}.

When formulated in one of the formalizations below, one finds that the principle of induction for propositions depending on natural numbers is 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.


By initial algebras over endofunctors

The induction principle may 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:X1+XF: X \to 1 + X is 0,s:1+\langle 0, s \rangle : 1 + \mathbb{N} \to \mathbb{N}, where \mathbb{N} is the set of natural numbers, 00 is the smallest natural number, and ss 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.


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

  • Ch. 3, Formal arithmetics, in: Elliott Mendelson, Introduction to mathematical logic, D. Van Nostrad 1964

Last revised on June 17, 2022 at 22:58:05. See the history of this page for a list of all contributions to it.