# A Proof of Transfinite Recursion Theorem

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

1. $$\operatorname{dom}f_{\alpha} = \alpha+1$$

2. $$\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.

1. $$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.

1. $$\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$$

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

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:

1. $$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$$ .

1. $$\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$$ .

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

1. $$\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).$$

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(f\restriction\beta)$$.

Let $$P(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(x,y)$$ defines an operation $$F$$ such that $$F(\alpha)=G(F\restriction\alpha)$$ for all $$\alpha\in\operatorname{Ord}$$.

Proof:

1. $$P(x,y)$$ defines an operation

We have to show that, for each $$x$$, there is a unique $$y$$ such that $$P(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(f') \rangle\}$$. We prove that $$f_{\alpha}$$ is a computation of length $$\alpha$$.

1. $$\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$$.

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(f_1\restriction\beta) = G(f_2\restriction\beta)$$ . Hence $$f_1(\beta)=f_2(\beta)$$ .

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(\beta)$$ for some $$f\in F$$ . Moreover, $$f(\beta)=G(f\restriction\beta)=G(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(f\restriction\beta)=G(f'\restriction\beta)$$ and thus $$f(\beta)=f'(\beta)$$ . The assertion follows.

This concludes the proof that the property $$P(x,y)$$ defines an operation $$F$$. We go on to prove $$F(\alpha)=G(F\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(f_1\restriction\beta) = G(f_2\restriction\beta)$$ and thus $$f_1(\beta)=f_2(\beta)$$ .

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

Transfinite Recursion Theorem, Parametric Version:

Let $$G$$ be an operation.

$$f$$ is a computation of length $$\alpha$$ based on $$G$$ and $$z$$ $$\iff$$ $$f$$ is a function with $$\operatorname{dom}f=\alpha+1$$ and $$\forall\beta\le\alpha:f(\beta)=G(z,f\restriction\beta)$$ .

Let $$P(z,\alpha,y)$$ be the property

$$\begin{cases}&\alpha\in\operatorname{Ord}&\wedge\quad y=f(\alpha)\text{ for some computation }f\text{ of length }\alpha\text{ based on }G\text{ and }z\\ \text{ or }&\alpha\notin\operatorname{Ord}&\wedge\quad y=\emptyset \end {cases}$$

Then $$P(z,\alpha,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:

1. $$P(z,\alpha,y)$$ defines an operation

We have to show that, for each $$(z,\alpha)$$ , there is a unique $$y$$ such that $$P(z,\alpha,y)$$ . This is obvious for $$\alpha\notin\operatorname{Ord}$$.

For $$\alpha\in\operatorname{Ord}$$, it suffices to show that for each $$(z,\alpha)$$: there is a unique computation $$f$$ of length $$\alpha$$ based on $$G$$ and $$z$$, or equivalently for each $$\alpha$$: there is a unique computation $$f$$ of length $$\alpha$$ based on $$G$$ and $$z$$.

Assume that for each $$\beta<\alpha$$: there is a unique computation of length $$\beta$$ based on $$G$$ and $$z$$. We next prove the existence and uniqueness of a computation of length $$\alpha$$ based on $$G$$ and $$z$$.

Existence

Axiom Schema of Replacement asserts that there exists a set $$F=\{f\mid \exists\beta<\alpha:f\text{ is a unique computation of length }\beta\text{ based on }G\text{ and }z\}$$

Moreover, IH implies that for each $$\beta<\alpha$$: there is a unique $$f\in F$$ based on $$G$$ and $$z$$ 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$$ based on $$G$$ and $$z$$.

1. $$\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$$ .

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

1. $$\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$$ based on $$G$$ and $$z$$. 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,\alpha,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$$ based on $$G$$ and $$z$$, and $$f_2$$ of length $$\beta_2$$ based on $$G$$ and $$z$$, 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)$$ .

Let $$f_{\alpha}$$ be the computation of length $$\alpha$$ based on $$G$$ and $$z$$ for all $$\alpha\in\operatorname{Ord}$$.

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

Why do you ignore the base case in your proof? Was it too trivial to write down? Transfinite induction requires a base case, correct? (I honestly don't know, this isn't a criticism) Thanks!