I have been studying the book, Introduction to Set Theory written by Hrbacek and Jech.
In this book the Recursion Theorem is stated as follows:
For any set $A$, any $a\in A$, and any function $g: A \times \mathbb{N} \rightarrow A$, there exists a unique infinite sequence $f: \mathbb{N} \rightarrow A$ such that
(a)$f_0=a$;
(b)$f_{n+1} = g(f_n , n)$ for all $n\in \mathbb{N}$.
Then the proof begins with defining $m$-step computation.
A function $t:(m+1) \rightarrow A$ is called an $m$-step computation based on $a$ and $g$ if $t_0 =a$, and, for all $k$ such that $0 \leq k < m$, $t_{k+1} = g(t_k, k)$.
And then, by using $m$-step computations, $f$ is defined, and the proof proceeds.
It is my question. Is $m$-step computation $t$ really a function?
I think $t$ is also defined recursively.
It means that the way to define either $f$ or $t$ is really similar.
Thus I have got some confusion,
"Why isn't $f$ directly a function, and is $t$ (obviously) a function?"
Please help me.
Recall a set $f$ is a function if it is a set of ordered pairs that has the property that if $\langle m,n\rangle$ and $\langle m,n'\rangle$ are in $f,$ then $n=n'.$
So, a priori, (a) and (b) do not constitute the definition of a function since they do not directly specify some set with the above property. Instead, (a) and (b) are merely some properties a function might have. The point of this theorem is to show that there is a unique function with these two properties. Once we have done so, then we may say henceforth that (a) and (b) define a function.
(Part of the confusion here is that it is fairly obvious from our intuition for recursion that such a function exists and is unique. The point of this theorem is to turn this intuition into a formal ZF proof. Then once we've done so, we know ZF is powerful enough to prove what we knew all along about recursion, and we can feel free to appeal to the principle.)
An $m$-step computation is defined to be a function with certain properties. Thus an $m$-step computation is a function by definition. What requires proof is the fact that for any $m,$ there is exactly one unique $m$-step computation. This can be proved by induction: There is exactly one $0$-step computation, $\{\langle 0, a\rangle\},$ and if there is exactly one $m$-step computation $t^m,$ then there is exactly one $m+1$-step computation $t^{m+1}=t^m\cup\{\langle m+1, g(t^m(m), m)\rangle\}.$ Again, it is important to emphasize we are not “defining functions by recursion” here. We are proving a sequence of functions with certain properties exists by induction.
Finally, we define $f = \{\langle m, t^m(m)\rangle :m\in\mathbb N\},$ where $t^m$ is the unique $m$-step computation. Then, we can prove that $f$ is a function with properties (a) and (b). That a function satisfying (a) and (b) must be unique can be proven by induction.