Is this theorem equivalent to Transfinite Recursion Theorem

ordinalsset-theorytransfinite-recursion

Let $V$ be the class of all sets, $\operatorname{Ord}$ be the class of all ordinals, and $G:V\to V$ be a class function.

Transfinite Recursion Theorem:

There exists a class function $F:\operatorname{Ord}\to V$ such that $F(\alpha)=G(F\restriction \alpha)$ for all $\alpha\in\operatorname{Ord}$.


While I'm able to prove that Transfinite Recursion Theorem implies the below theorem, I have tried but to no avail in proving that the theorem implies Transfinite Recursion Theorem.

I would like to ask if it is possible to prove that this theorem implies Transfinite Recursion Theorem.

Thank you for your help!


Theorem:

Let $G_1,G_2,G_3$ be class functions from $V$ to $V$. There exists a class function $F:\operatorname{Ord}\to V$ such that

(1) $F(0)=G_1(\emptyset)$

(2) $F(\alpha+1)=G_2(F(\alpha))$ for all $\alpha\in\operatorname{Ord}$

(3) $F(\alpha)=G_3(F\restriction\alpha)$ for all limit $\alpha\neq 0$

Best Answer

The trick is to not construct $F$ itself, but to construct the function $H$ which sends $\alpha$ to $F\restriction \alpha$. That way, at successor steps you have access to the entire history of the recursion so far and not just the last step.

In detail, given $G:V\to V$, we define $G_1$, $G_2$, and $G_3$ as follows: $$G_1(x)=\emptyset$$ $$G_2(x)=x\cup\{(\operatorname{dom}(x),G(x))\}$$ $$G_3(x)=\bigcup\operatorname{ran}(x)$$ By the theorem, we then get a function $H:Ord\to V$ such that $H(0)=G_1(\emptyset)$, $H(\alpha+1)=G_2(H(\alpha))$, and $H(\alpha)=G_3(H\restriction\alpha)$ for $\alpha\neq 0$ limit. It is then easy to prove by induction that $H(\alpha)$ is a function with domain $\alpha$ for each $\alpha$, with $H(\alpha)\restriction \beta=H(\beta)$ for all $\beta<\alpha$. So, defining $F=\bigcup\operatorname{ran}(H)$, $F$ is a function on $Ord$ with $F\restriction\alpha=H(\alpha)$ for each $\alpha$. For each $\alpha$, we then have $$F(\alpha)=H(\alpha+1)(\alpha)=G_2(H(\alpha))(\alpha)=G_2(F\restriction\alpha)(\alpha).$$ Since $\operatorname{dom}(F\restriction\alpha)=\alpha$, our definition of $G_2$ tells us that $$F(\alpha)=G_2(F\restriction\alpha)(\alpha)=G(F\restriction\alpha),$$ as desired.