The Parametric Transfinite Recursion Theorem (PTRT) states:
For each operation $\mathbf{G}$, there is an operation $\mathbf{F}$ such that $\mathbf{F}(z,\alpha)=\mathbf{G}(z,\mathbf{F}_z\restriction \alpha)$.
$\mathbf{F}_z$ is just the operation given by $\mathbf{F}_z(x)=\mathbf{F}(z,x)$.
The Transfinite Double Recursion Theorem (TDRT) states:
For each operation $\mathbf{G}$, there is an operation $\mathbf{F}$ such that $\mathbf{F}(\alpha,\beta)=\mathbf{G}(\mathbf{F} \restriction (\alpha \times \beta))$ for all ordinals $\alpha, \beta$.
Is there any hope to use the PTRT to prove the TDRT? I've been trying for quite some time now, but have not come up with any useful idea yet. I'm starting to wonder if the PTRT can even be used to prove the TDRT.
Best Answer
Yes, you can do this. The idea is to construct the operation $\alpha\mapsto\mathbf{F}\restriction(\alpha\times\alpha)$, which intuitively you can do by ordinary transfinite recursion since the rule $\mathbf{F}(\gamma,\delta)=\mathbf{G}(\mathbf{F} \restriction (\delta \times \gamma))$ tells you how to define $\mathbf{F}$ on $\alpha\times\alpha$ if you already know it on $\beta\times\beta$ for all $\beta<\alpha$ (since $\delta\times\gamma$ is contained in some such $\beta\times\beta$).
To make this precise, let $\mathbf{G}'$ be the operation defined as follows. Suppose $f$ is a function whose domain is an ordinal $\alpha$, and moreover assume that $f(\beta)$ is a function with domain $\beta\times\beta$ for each $\beta<\alpha$. We then define $\mathbf{G}'(f)$ be the function $g$ with domain $\alpha\times\alpha$ defined by $g(\gamma,\delta)=\mathbf{G}(f(\beta)\restriction(\delta\times\gamma))$ where $\beta=\max(\gamma,\delta)$. (If $f$ is not such a function, we define $\mathbf{G}'(f)=\emptyset$.)
By the PTRT (ignoring the parameter), there is an operation $\mathbf{F}'$ such that $\mathbf{F}'(\alpha)=\mathbf{G}'(\mathbf{F}'\restriction\alpha)$ for all ordinals $\alpha$. It is straightforward to prove by induction that $\mathbf{F}'(\alpha)$ is a function with domain $\alpha\times\alpha$ for each $\alpha$, and if $\beta<\alpha$ then $\mathbf{F}'(\beta)$ is the restriction of $\mathbf{F}'(\alpha)$ to $\beta\times\beta$. Now define $\mathbf{F}(\alpha,\beta)=\mathbf{F}'(\gamma)(\alpha,\beta)$ where $\gamma=\max(\alpha,\beta)+1$. It is now easy to verify that $\mathbf{F}$ is the desired operation.