How does Prof D. J. H. Garling generalize recursion theorem?

Question

From textbook A Course in Mathematical Analysis by Prof D. J. H. Garling, I'm not able to understand how he generalizes recursion theorem.

In the first step, he states the theorem:

Here, mapping $s:P→P$ satisfies Peano’s axioms.

In the second step, he reasons:

Finally, he gets the theorem in a more general form:

My confusion is that:

1. In the original theorem, for each $\bar{a}$, there exists a unique mapping $a:P → A$ such that $a_{0}=\bar{a}$ and $a_{s(n)}=f(a_{n})$ $\forall n\in P$. We substitute $P$ by $Z^{+}$. As a result, for each $\bar{a}$, there exists a unique mapping $a:Z^{+} → A$ such that $a_{0}=\bar{a}$ and $a_{s(n)}=f(a_{n})$ $\forall n\in Z^{+}$. However, I don't understand how the author derives the mapping $f^{n}:A → A$ from the mapping $a:Z^{+} → A$.

2. In the second step, the author lets $f^{n}(\bar{a})=a_{n}$. This means $f^{0}(\bar{a})=a_{0}$, $f^{1}(\bar{a})=a_{1}$, $f^{2}(\bar{a})=a_{2}$, ..., $f^{n}(\bar{a})=a_{n}$. From my understanding, he only defines $f^{0}, f^{1}, f^{2}, f^{3},..., f^{n}$ for only $\bar{a}$. I don't understand how the author defines $f^{0}, f^{1}, f^{2}, f^{3},..., f^{n}$ for the other elements in A.

3. $(f^{n}(\bar{a})=a_{n}$ and it is possible that $ran(a)\subsetneq A) → ran(f^{n})\subsetneq A$. How can $f^{n}$ be defined for all $a\in A$?

For the sake of clarity, there is a screenshot of full proof of recursion theorem by the author at Possible typos in the proof of Recursion Theorem.

Many thanks for clarifying my doubt!

Answer 1

Intuitively, to construct $f^n$ we must specify $f^n(\bar a)$ for each $\bar a\in A$. So for each $\bar a\in A$, apply Theorem 1.8.1 to obtain a sequence $a$ (this depends on $\bar a$), and let $f^n(\bar a)=a(n)$.

More formally we could define $f^n$ as $$ \{p\in A\times A:\text{there exists }g:\mathbf Z^+\to A\text{ with }g\circ s=f\circ g,\,g(0)=p_1,\,g(n)=p_2\}. $$ I claim that for all $a\in A$, $|f^n\cap(\{a\}\times A)|=1$. Indeed fix $a\in A$. By Theorem 1.8.1, there exists $g:\mathbf Z^+\to A$ with $g\circ s=f\circ g$ and $g(0)=a$. Then $(a,g(n))\in f^n$. Conversely if $p\in f^n\cap(\{a\}\times A)$ then there exists $g':\mathbf Z^+\to A$ with $g'\circ s=f\circ g$, $g'(0)=p_1=a$ and $g'(n)=p_2$. By the uniqueness in Theorem 1.8.1, $g'=g$, so $p_2=g(n)$. Thus $f^n\cap(\{a\}\times A)=\{(a,g(n))\}$. This shows $f^n$ is a function.