# On the proof of a normal form theorem for ordinal (primitive) recursion

Consider the following statement (which follows easily from various results found in the literature):

(†) There exists a primitive recursive (“p.r.”) relation $T$ on the ordinals such that, if $(f_e)_{e<\omega}$ is a standard numbering of the p.r. functions of one variable on the ordinals, we have $f_e(x)=y$ iff $\exists z.T(e,x,y,z)$; moreover, there then exists such a $z$ which is less than the smallest p.r.-closed ordinal $\geq x$.

One straightforward consequence of (†) is a Kleene normal form theorem for $\alpha$-recursion: there exists a p.r. relation $T'$ on the ordinals such that, if $(\varphi_e)_{e<\omega}$ is a standard numbering of the partial recursive functions of one variable on the admissible ordinal $\alpha$, we have $\varphi_e(x)\simeq y$ iff $\exists z<\alpha.T'(e,x,y,z)$. (One straightforward consequence of that is that there exists a “universal” partial recursive $g$ on $\alpha$ with the property that $g(e,x) \simeq \varphi_e(x)$.)

Now every proof of (†) that I was able to find boils down to something like this: if $f_e(x)=y$ then for $\beta$ large enough (larger than all the intermediate computation values) we have $L_\beta \models f_e(x)=y$, and “$L_\beta \models f_e(x)=y$” is a p.r. relation of the ordinals $e,x,y,\beta$ because it is a p.r. relation of the sets $e,x,y,\beta$ and p.r. relations on ordinals and on sets that happen to be ordinals coincide.

This proof is explicit, in the sense that it actually gives $T$, but the $T$ in question seems rather insanely complicated (as a p.r. relation on ordinals) because of the process of converting a p.r. relation on sets to one on ordinals and because of the route through formulas and the $L_\beta$.

Question: Can the statement (†) above be proved entirely at the level of p.r. functions and relations on the ordinals? Variant: Can we give an explicit $T$ that is reasonably short?

In the case of ordinary recursion, it is not too difficult. What I would like to understand is whether there is some reason why the transfinite ordinal case should be harder or whether it is just an artefact of the way things are written in the literature.

Motivation: Partially from trying to get a better understanding of this question I asked recently; partially from thinking about how, if $\alpha$-recursion is viewed as a transfinite programming language, one would proceed to write an “interpreter” for the language in the language itself (=universal function).

• My personal view is that p.r. on sets is the natural notion, as this restricts to ordinal p.r. recursion nicely enough. So asking for a $T$ predicate for the ordinal p.r. recursion, to be explicitly given in terms of only ordinal p.r. recursion, is tying one hand behind one's back. Aug 8, 2017 at 7:21
• @PhilipWelch I see what you mean. Maybe the problem is that I still don't understand why ordinal p.r. recursion suffices to get all of set p.r. recursion: reading the proof in Jensen&Carp just looks like "magic happens". Do you happen to know if there have been any simplifications, summaries, or simply re-expositions of this proof? (Maybe I should make this a different question, but maybe it's not worth it.) Aug 8, 2017 at 12:23
• Gro-Tsen: I think once you see set equality and membership copied on to the ordinal p.r. functions then the rest are built up in a not unfamiliar fashion. The p.r. functions are not used so much these dyas, and I am sorry I dont know of any more recent exposition, although proof theorists may know of such. (Any reaction to my final answer to your other p.r. question?) Aug 8, 2017 at 13:25