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.^{1}

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))$.^{2}

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. ↩︎