# Extension of primitive recursion, that is as powerful as System-T

I know that System-T restricted to first-order types is exactly as powerful as primitive recursive functions, because I proved it in Agda.

I asked myself, if there is a extension of primitive recursive functions, that is exactly as powerful as System-T.

Best Regards

• And why isn't the answer "System T"? Commented Oct 6, 2022 at 15:42
• @AndrejBauer I only know a version of System-T with binders, function-application and variables. Primitive Recursion is defined with basic functions and operators. I'm looking for a version of System-T, that is also defined like this. Commented Oct 6, 2022 at 17:56
• Primitive recursive functions can be encoded in System T in a straightforward manner. Commented Oct 6, 2022 at 20:38
• My point is, System T, which is just simply-typed $\lambda$-calculus with natural numbers, is more general. You could try to backport it to some sort of old-style notation for primitive recursion, but why would you do that? What are you trying to accomplish? Commented Oct 6, 2022 at 20:48
• It is just interesting for me to see how to express the constructs in the extended simply typed lambda calculus with the operators of primitive recursion. Commented Oct 7, 2022 at 4:25

If you're just talking about the expressiveness of functions $$\mathbb{N}\rightarrow\mathbb{N}$$, then you can extend primitive recursion to allowing a recursive call over a Cantor normal form, where the recursive calls need to be made at smaller ordinals.
In this way you have well-founded recursion up to $$\varepsilon_0$$, which gives you the same functions as System-T over naturals, which is well-known, but hard to find a clean reference for (usually one proves $$\varepsilon_0$$-induction $$\Leftrightarrow$$ $$\mathrm{PA}$$-definable functions $$\Leftrightarrow$$ System-T functions at baset type).
• I think this is too much. Induction up to $\epsilon_0$ gives you more than PA (it proves the consistency of PA, for instance). In PA, you only have induction up to $\alpha$ for every particular $\alpha<\epsilon_0$. So you would need infinitely many operators, the $n$th one allowing you to make recursive calls over Cantor normal forms of ordinals below $\omega_n$ (where $\omega_1=\omega$, $\omega_{n+1}=\omega^{\omega_n}$). Commented Oct 7, 2022 at 17:15