Definition by recursion

Summary

A definition by recursion defines a function on the natural numbers in two parts. It gives the value at $0$, and a rule that gives the value at $n + 1$ from the value at $n$. The recursion theorem says that such a definition always gives exactly one function. Precisely, let $X$ be a set, let $a$ be an element of $X$ and let $g \colon \mathbb{N} \times X \to X$ be a function. Then there is exactly one function $f \colon \mathbb{N} \to X$ with $f(0) = a$ and $f(n + 1) = g(n, f(n))$ for each $n$ in $\mathbb{N}$.