Transfinite Recursion Theorem, Paramatric Version:
Let $G$ be an operation.
$f$ is a computation of length $\alpha$ $\iff$ $f$ is a function such that $\operatorname{dom}f=\alpha+1$ and $\forall\beta\le\alpha:f(\beta)=G(z,f\restriction\beta)$ .
Let $P(z,x,y)$ be the property
$\begin{cases}&x\in\operatorname{Ord}&\wedge\quad y=f(x)\text{ for some computation }f\text{ of length }x\\ \text{ or }&x\notin\operatorname{Ord}&\wedge\quad y=\emptyset \end {cases}$
Then $P(z,x,y)$ defines an operation $F$ such that $F(z,\alpha)=G(z,F_z\restriction\alpha)$ for all $\alpha\in\operatorname{Ord}$ and for all sets z.
Proof:
- $P(z,x,y)$ defines an operation
We have to show that, for each $x$ , there is a unique $y$ such that $P(z,x,y)$ . This is obvious for $x\notin\operatorname{Ord}$ . For ordinals, it suffices to show that for all $\alpha\in\operatorname{Ord}$ : there is a unique computation of length $\alpha$ .
Assume that for all $\beta<\alpha$ : there is a unique computation of length $\beta$ . We next prove the existence and uniqueness of a computation of length $\alpha$ .
Existence
By Axiom Schema of Replacement applied to the property $y$ is a computation of length $x$ and the set $\alpha$ , there exists a set $$F=\{f\mid \exists\beta<\alpha:f\text{ is a unique computation of length }\beta\}$$
Moreover, IH implies that for every $\beta<\alpha$ : there is a unique $f\in F$ such that the length of $f$ is $\beta$ . Let $f'=\bigcup F$ and $f_{\alpha}=f'\cup\{\langle \alpha,G(z,f') \rangle\}$ . We prove that $f_{\alpha}$ is a computation of length $\alpha$ .
- $\operatorname{dom}f_{\alpha}=\alpha+1$
$\operatorname{dom}f'=\bigcup_{f\in F}\operatorname{dom}f=\bigcup_{\beta\in\alpha}(\beta+1)=\alpha$ . Hence $\operatorname{dom}f_{\alpha} =\{\alpha\}\cup \operatorname{dom}f'=\{\alpha\}\cup\alpha=\alpha+1$ .
- $f_{\alpha}$ is a function
Since $\alpha\notin\operatorname{dom}f'$ , it is enough to prove that $f'$ is a function. This follows from the fact that $F$ is a compatible system of functions.
Indeed, let $f_1,f_2\in F$ be arbitrary, and let $\operatorname{dom} f_1=\beta_1$ and $\operatorname{dom} f_2=\beta_2$ . Assume that $\beta_1\le\beta_2$ and thus $\beta_1\subseteq\beta_2$ . It suffices to prove by Transfinite Induction that $f_1(\gamma)=f_2(\gamma)$ for all $\gamma<\beta_1$ . So assume that $f_1(\gamma)=f_2(\gamma)$ for all $\gamma<\beta$ . Then $f_1\restriction\beta=f_2\restriction\beta$ and thus $G(z,f_1\restriction\beta) = G(z,f_2\restriction\beta)$ . Hence $f_1(\beta)=f_2(\beta)$ .
- $\forall\beta\le\alpha:f_{\alpha}(\beta)=G(z,f_{\alpha}\restriction\beta)$
If $\beta=\alpha$ , then $f_{\alpha}(\beta)=G(z,f')=G(z,f_{\alpha}\restriction\alpha)$ . If $\beta<\alpha$ , then $f_{\alpha}(\beta)=f(\beta)$ for some $f\in F$ . Moreover, $f(\beta)=G(z,f\restriction\beta)=G(z,f_{\alpha}\restriction\beta)$ since $f\subseteq f_{\alpha}$ .
Uniqueness
Suppose that $f,f'$ are two computations of length $\alpha$ . We will prove $f=f'$ . As $\operatorname{dom}f=\operatorname{dom}f'=\alpha+1$ , it suffices to prove by Transfinite Induction that$f(\beta)=f'(\beta)$ for all $\beta\le\alpha$ . Assume that $f(\gamma)=f'(\gamma)$ for all $\gamma<\beta$ and thus $f\restriction\beta=f'\restriction\beta$ . Then $G(z,f\restriction\beta)=G(z,f'\restriction\beta)$ and thus $f(\beta)=f'(\beta)$ . The assertion follows.
This concludes the proof that the property $P(z,x,y)$ defines an operation $F$ . We go on to prove $F(z,\alpha)=G(z,F_z\restriction\alpha)$ .
First, we prove that for any computations $f_1$ of length $\beta_1$ and $f_2$ of length $\beta_2$ with $\beta_1\subseteq\beta_2$ : $f_1\subseteq f_2$ . It suffices to prove by Transfinite Induction that $f_1(\gamma)=f_2(\gamma)$ for all $\gamma\le\beta_1$ . So assume that $f_1(\gamma)=f_2(\gamma)$ for all $\gamma<\beta$ and thus $f_1\restriction\beta=f_2\restriction\beta$ . Then $G(z,f_1\restriction\beta) = G(z,f_2\restriction\beta)$ and thus $f_1(\beta)=f_2(\beta)$ .
$F(z,\alpha)=f_{\alpha}(\alpha)=G(z,f_{\alpha}\restriction\alpha)=G(z,\{\langle \beta,f_{\alpha}(\beta)\rangle\mid \beta<\alpha\})=G(z,\{\langle \beta,f_{\beta}(\beta)\rangle\mid \beta<\alpha\})=G(z,\{\langle \beta,F(z,\beta)\rangle\mid \beta<\alpha\})=G(z,F_z\restriction\alpha).$
We do not actually need the parametric version of Theorem 4.11. In fact, Theorem 4.11 implies Theorem 4.12. This is what your textbook says.
Let $G_1$, $G_2$ and $G_3$ is a class function such that
$G_1(0)=(\{(0,a)\}, 0)$,
$$G_2(x) = \begin{cases}(G(f,n),n+1) & \text{if $x=(f,n)$ for some $n$ and $f$,}\\ \varnothing & \text{otherwise,}\end{cases}$$
and $G_3(x)=\varnothing$. You can see that $F(n) = (f_n,n)$. That is, the sequence of the first component of $F(n)$ is our desired sequence.
Best Answer
How can you prove that $F\restriction\alpha$ is a set otherwise? This is literally a way to formulate the Replacement axiom schema: a class function restricted to a set is a set.
The point is that if you want to argue that $F(\alpha)=G(F\restriction\alpha)$, then you need to prove that $F\restriction\alpha$ is in the domain of $G$, or in other words, a set. Arguably, you could prove that $F\restriction\alpha+1=f_\alpha$, but this too will require you to appeal to Replacement (or its formulation via transfinite induction).
One good way to see this is to try and recreate the proof in a setting where we know it is bound to fail. Work in $V_{\omega+\omega}$ and consider $G(x)=\omega+n$ if $x\in V_{\omega+n+1}\setminus V_{\omega+n}$, or if $x\in V_{n+1}\setminus V_n$, and otherwise $G(x)=0$.
Now define by recursion this $F$. Then $F(0)=G(\varnothing)=0$, then $F(1)=G(F\restriction 1)=\omega+k$ for some appropriate $k$ (depending on your coding of ordered pairs and functions, of course). As you continue on, you realize that $F\restriction\omega$ is no longer a set. So how could you define $F(\omega)$?