This proof takes me a huge amount of time to formulate, so I hope that someone can help me verify it. There're possibly subtle mistakes that I'm unable to recognize. Thank you for your dedicated help!
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)$$
My attempt:
We will show that, for all $\alpha\in\operatorname{Ord}$, there exists a unique function $f_{\alpha}$ that satisfies
-
$\operatorname{dom}f_{\alpha} = \alpha+1$
-
$\forall \beta\le\alpha:f_{\alpha}(\beta) = G(f_{\alpha}\restriction\beta)$
Uniqueness
Suppose that $f'_{\alpha}$ also satisfies the conditions. We will prove $f_{\alpha}=f'_{\alpha}$. As $f_{\alpha}$ and $f'_{\alpha}$ are functions and $\operatorname{dom}f_{\alpha} = \alpha+1=\operatorname{dom}f'_{\alpha}$, it suffices to prove by Transfinite Induction that $f_{\alpha}(\beta)=f'_{\alpha}(\beta)$ for all $\beta\le\alpha$.
Assume that $f_{\alpha}(\gamma)=f'_{\alpha}(\gamma)$ for all $\gamma<\beta$. Then $f_{\alpha}\restriction\beta=f'_{\alpha}\restriction\beta$ and thus $G(f_{\alpha}\restriction\beta)=G(f'_{\alpha}\restriction\beta)$. Thus $f_{\alpha}(\beta)=f'_{\alpha}(\beta)$. The assertion follows.
Existence
Assume that for all $\beta<\alpha$, there exists a unique function $f_{\beta}$ that satisfies the conditions.
Let $f=\bigcup_{\beta<\alpha}f_{\beta}$. The Axiom of Schema of Replacement asserts that $f$ is a set. Let $f_{\alpha}=f\cup\{\langle\alpha,G(f)\rangle\}$ Next we prove that $f_{\alpha}$ satisfies the conditions.
- $f_{\alpha}$ is a function
Since $\alpha\notin\operatorname{dom}f$, it is enough to prove that $f$ is a function.
We prove that $\forall \alpha_1<\alpha_2<\alpha:f_{\alpha_1}\subsetneq f_{\alpha_2}$. It suffices to prove by Transfinite Induction that $f_{\alpha_1}(\beta)=f_{\alpha_2}(\beta)$ for all $\beta\le\alpha_1$. So assume that $f_{\alpha_1}(\gamma)=f_{\alpha_2}(\gamma)$ for all $\gamma<\beta$. Then $f_{\alpha_1}\restriction\beta=f_{\alpha_2}\restriction\beta$ and thus $G(f_{\alpha_1}\restriction\beta)=G(f_{\alpha_2}\restriction\beta)$. Hence $f_{\alpha_1}(\beta)=f_{\alpha_2}(\beta)$. The assertion follows. Hence $\{f_{\beta}\mid\beta<\alpha\}$ is a system of compatible functions and thus $f$ is a function.
- $\operatorname{dom}f_{\alpha} = \alpha+1$
$\operatorname{dom}f=\bigcup_{\beta<\alpha}\operatorname{dom}f_{\beta}=\bigcup_{\beta<\alpha}\beta+1=\alpha$. Hence $\operatorname{dom}f_{\alpha} =\{\alpha\}\cup \operatorname{dom}f=\{\alpha\}\cup\alpha=\alpha+1$
- $\forall \beta\le\alpha:f_{\alpha}(\beta) = G(f_{\alpha}\restriction\beta)$
If $\beta=\alpha$, then $f_{\alpha}(\beta)=G(f)=G(f_{\alpha}\restriction\alpha)$. If $\beta<\alpha$, then $f_{\alpha}(\beta)=f_{\alpha_1}(\beta)$ for some $\alpha_1<\beta$. Moreover, $f_{\alpha_1}(\beta)=G(f_{\alpha_1}\restriction\beta)=G(f_{\alpha}\restriction\beta)$ since $f_{\alpha_1}\subseteq f_{\alpha}$.
Finally, we move on to prove our main theorem. We define $F$ by $F(\alpha)=f_{\alpha}(\alpha)$ for all $\alpha\in\operatorname{Ord}$. I claim that $F$ satisfies the requirement of the theorem.
$F(\alpha)=f_{\alpha}(\alpha)=G(f_{\alpha}\restriction\alpha)=G(\{\langle \beta,f_{\alpha}(\beta)\rangle\mid \beta<\alpha\})=G(\{\langle \beta,f_{\beta}(\beta)\rangle\mid \beta<\alpha\})=G(\{\langle \beta,F(\beta)\rangle\mid \beta<\alpha\})=G(F\restriction\alpha).$
Best Answer
Transfinite Recursion Theorem, Paramatric Version:
Proof:
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'=\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$ .
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)$ .
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).$