1
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.