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

  • 1
    $\begingroup$ And why isn't the answer "System T"? $\endgroup$ Oct 6, 2022 at 15:42
  • $\begingroup$ @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. $\endgroup$ Oct 6, 2022 at 17:56
  • $\begingroup$ Primitive recursive functions can be encoded in System T in a straightforward manner. $\endgroup$ Oct 6, 2022 at 20:38
  • $\begingroup$ 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? $\endgroup$ Oct 6, 2022 at 20:48
  • $\begingroup$ 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. $\endgroup$ Oct 7, 2022 at 4:25

1 Answer 1


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

  • $\begingroup$ 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}$). $\endgroup$ Oct 7, 2022 at 17:15
  • $\begingroup$ Good point @EmilJeřábek! $\endgroup$
    – cody
    Oct 8, 2022 at 18:11
  • 1
    $\begingroup$ Something like this is even mentioned in Gödel's original paper link.springer.com/article/10.1007/BF00247744 "The system T has the same deductive strength as a system of recursive number theory which allows complete induction over any ordinal < ε₀ (in the usual representation)." $\endgroup$ Nov 3, 2022 at 16:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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