= Solution
An approximation is a function $s:n+1\to X$ with $s(0)=x_0$ and $s(k+1)=g(s(k))$ for $k<n$. By induction on $n$, there is such a function: start with $\{(0,x_0)\}$ and append the uniquely specified value $g(s(n))$.
Any two approximations agree on their common domain, by induction from their common initial value and the same transition <function> $g$. The collection $\mathcal S$ of all approximations is a set, being a definable subset of $\mathcal P(\omega\times X)$. Therefore $f=\bigcup\mathcal S$ is a <function>. Existence of approximations of every finite length gives $\operatorname{dom}(f)=\omega$. Each defining equation appears in a sufficiently long approximation, so
$$
\boxed{f:\omega\to X,\qquad f(0)=x_0,\qquad f(n+1)=g(f(n)).}
$$
This proves the <natural-number recursion theorem> without the <axiom of choice>; no arbitrary sequence of choices was made.
Back to article page
