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).$
Best Answer
You have a little problem with $\beta$, you never defined it.
I think you meant to say in $P$ that $\forall \beta(\alpha<\beta\implies...)$ and then at $\delta<\gamma<\beta$ it is for arbitrary $\beta$.
If this is what you meant you proof is correct.
Here is a different way, which avoid the use of proper class(apart from $V$).
Let $f:\alpha\to V,g:\gamma\to V, f(x)=G(f\restriction x), g(y)=G(g\restriction y)$
Assume $\gamma\in\alpha(\gamma<\alpha)$.
Let $\delta<\gamma$ satisfy the induction requirements, for all ordinals lesser than $\delta$ we have $f,g$ equal.
From assumption we have $f\restriction \delta=g\restriction \delta$
Thus $G(f\restriction \delta)=G(g\restriction \delta)$
But this is nothing more than $f(\delta)=g(\delta)$.
This means that $\forall\delta\in\gamma(\delta<\gamma)(f(\delta)=g(\delta))$ hence $f\restriction \gamma=g$.
This is exactly the same as yours apart from the fact that my $f,g$ are fixed so it is easier to follow in my opinion.