Recursion Theorem

Why

It is natural to want to define a sequence by giving its first term and then giving its later terms as functions of its earlier ones. In other words, we want to define sequences inductively.¹

Let $X$ be a set, let $a \in X$ and let $f: X \to X$. There exists a unique function $u$ so that $u(0) = a$ and $u(\ssuc{n}) = f(u(n))$.²

When one uses the recursion theorem to assert the existence of a function with the desired properties, it is called definition by induction.

Future editions will expand on this. We are really headed toward natural addition, multiplication and exponentiation. ↩︎
The account is somewhat straightforward, given a good understanding of the results of Peano Axioms. The full account will appear in future editions. ↩︎