<p>If you're just talking about the expressiveness of functions <span class="math-container">$\mathbb{N}\rightarrow\mathbb{N}$</span>, then you can extend primitive recursion to allowing a recursive call over a <a href="https://en.wikipedia.org/wiki/Ordinal_arithmetic#Cantor_normal_form" rel="nofollow noreferrer">Cantor normal form</a>, where the recursive calls need to be made at smaller ordinals.</p>
<p>In this way you have well-founded recursion up to <span class="math-container">$\varepsilon_0$</span>, 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 <span class="math-container">$\varepsilon_0$</span>-induction <span class="math-container">$\Leftrightarrow$</span> <span class="math-container">$\mathrm{PA}$</span>-definable functions <span class="math-container">$\Leftrightarrow$</span> System-T functions at baset type).</p>

CC BY-SA 4.0
2022-10-07T17:15:35.453Z
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}$).
Emil Jeřábek
CC BY-SA 4.0
2022-10-08T18:11:07.883Z
Good point @EmilJeřábek!
cody
CC BY-SA 4.0
2022-11-03T16:31:31.940Z
Something like this is even mentioned in Gödel's original paper https://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)."
Lê Thành Dũng 'Tito' Nguyễn
CC BY-SA 4.0
2022-10-07T16:28:44.530Z
2022-10-07T16:28:44.530Z
cody
<p>I know that System-T restricted to first-order types is exactly as powerful as primitive recursive functions, because I proved it in Agda.</p>
<p>I asked myself, if there is a extension of primitive recursive functions, that is exactly as powerful as System-T.</p>
<p>Best Regards</p>

CC BY-SA 4.0
2022-10-06T15:42:09.837Z
And why isn't the answer "System T"?
Andrej Bauer
CC BY-SA 4.0
2022-10-06T17:56:35.870Z
@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.
ghostOfTomJoad
CC BY-SA 4.0
2022-10-06T20:38:57.823Z
Primitive recursive functions can be encoded in System T in a straightforward manner.
Andrej Bauer
CC BY-SA 4.0
2022-10-06T20:48:44.740Z
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?
Andrej Bauer
CC BY-SA 4.0
2022-10-07T04:25:31.940Z
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.
ghostOfTomJoad
CC BY-SA 4.0
2022-10-07T11:34:09.140Z
What you said in your last comment sounds like you want to extend STL with primitive recursion, but your original question is the other way around. The problem of extending PR to higher-order computation is that you somehow have to control recursion, without just getting back single-typed λ-calculus. Extending STL seems the most natural path. You may be interested in Sec. 5.C of Barendregt et al., "Lambda Calculus with Types" and Eilenberg & Elgot, "Recursiveness".
Henning Basold
<computability><pl.programming-languages><typed-lambda-calculus><recursion>
Extension of primitive recursion, that is as powerful as System-T
ghostOfTomJoad
# Extension of primitive recursion, that is as powerful as System-T

(Asked by: username_0 on 2022-10-06)

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

**Tags:** computability, pl.programming-languages, typed-lambda-calculus, recursion

> **Comments:**
> **username_1**: And why isn't the answer "System T"?  
> **username_0**: @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.  
> **username_1**: Primitive recursive functions can be encoded in System T in a straightforward manner.  
> **username_1**: 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?  
> **username_0**: 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.  
> **username_2**: What you said in your last comment sounds like you want to extend STL with primitive recursion, but your original question is the other way around. The problem of extending PR to higher-order computation is that you somehow have to control recursion, without just getting back single-typed λ-calculus. Extending STL seems the most natural path. You may be interested in Sec. 5.C of Barendregt et al., "Lambda Calculus with Types" and Eilenberg & Elgot, "Recursiveness".  

---

## 1 answers

### Answer by username_3 on 2022-10-07. Score: 4

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](https://en.wikipedia.org/wiki/Ordinal_arithmetic#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).

> **Comments:**
> **username_4**: 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}$).  
> **username_3**: Good point @EmilJeřábek!  
> **username_5**: Something like this is even mentioned in Gödel's original paper https://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)."  

---

