The $n$th Church numeral $\underline{n}$ is the operation of “iteration $n$ times”, sending a function $f$ to its $n$th iterate. Thus $\underline{0}(f)$ is the identity function, $\underline{1}(f) = f$, $\underline{2}(f) = f\circ f = \lambda x. f(f(x))$, and so on.

Connection to realizability

The Church numeral $\underline{n}$ can be regarded as a realizer or “proof” that we can do induction up to $n$. See this discussion.

Last revised on June 26, 2021 at 16:14:42.
See the history of this page for a list of all contributions to it.