The role of Axiom Schema of Replacement in the proof of Transfinite Recursion Theorem

Question

Transfinite Recursion Theorem:

Let $G:V\to V$ be a class function. Then there is a unique function $F:\operatorname{Ord}\to V$ such that $$\forall \alpha\in \operatorname{Ord}:F(\alpha)=G(F\restriction\alpha)$$

---

I found that the proof of this theorem often follows:

1. First, it proves that

For all $\alpha\in\operatorname{Ord}$, there exists a unique function $f_{\alpha}$ that satisfies

(1) $\operatorname{dom}f_{\alpha} = \alpha+1$

(2) $\forall \beta\le\alpha:f_{\alpha}(\beta) = G(f_{\alpha}\restriction\beta)$

2. Second, it defines $F$

For all $\alpha\in\operatorname{Ord}$, $F(\alpha):=f_{\alpha}(\alpha)$.

3. It proves that $F\restriction\alpha$ is a set with the following reasoning

We have $F\restriction\alpha=\{\langle \beta,F(\beta)\rangle\mid \beta<\alpha\}$, so by Axiom of Schema Replacement, $F\restriction\alpha$ is a set.

---

My questions:

1. Of my understanding, After define $F$ by $\forall\alpha\in\operatorname{Ord}:F(\alpha):=f_{\alpha}(\alpha)$. I think I've finished our task, which is to define $F$.

I'm unable to understand why the proof goes on to prove that $F\restriction\alpha$ is a set for all $\alpha\in\operatorname{Ord}$.

2. Of my understanding, $F$ is a function and $F\restriction\alpha$ is a restriction on $F$ and thus is a set.

I'm unable to understand what is the role of Axiom of Schema Replacement here.

Thank you so much for your response!

Answer 1

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)$?