<p>There is no total language where all total computable <span class="math-container">$\mathbb{N} \to \mathbb{N}$</span> functions are definable. In a total language, an interpreter for the same language is not definable because if it were then general recursion could be recovered by diagonalization; <a href="https://dl.acm.org/doi/pdf/10.1145/2837614.2837623?casa_token=XyBfL2RjntIAAAAA:tsuq5dPxcyxpIIlrcI0k6BxNTmWlOyYivlCaSmF73A-dmmZvd9BYIklnAf74cCaTpbO2WufhNaDw" rel="nofollow noreferrer">see theorem 3.2 here</a>. This is analogous to Gödel's second incompleteness theorem.</p>
<p>The range of definable total functions in a theory is called <em>proof-theoretic strength</em>. The calculus of constructions has the same strength as System F<span class="math-container">$\omega$</span>. That is in turn at least as strong as System F, and probably strictly stronger (see cody's answer). System F has the same strength as second-order arithmetic. You can read about this in chapter 15 of Girard's <a href="http://tlca.di.unito.it/opltlca/opltlca.pdf" rel="nofollow noreferrer">Proofs and Types</a>. Second-order arithmetic is in turn weaker than ZFC, but it's strong enough to be beyond the reach of <a href="https://ncatlab.org/nlab/show/ordinal+analysis" rel="nofollow noreferrer">ordinal analysis</a>, which tries to measure proof-theoretic strength by ordinal notations.</p>
<p>EDIT: taking cody's remarks into account.</p>

CC BY-SA 4.0
2022-06-08T08:36:41.173Z
A mminor quibble: in the last sentence, it is better to say "by ordinal notations" or "by ordinal number notations".
Andrej Bauer
CC BY-SA 4.0
2022-06-08T11:14:59.617Z
@AndrejBauer fair point. Edited.
András Kovács
CC BY-SA 4.0
2022-06-08T14:40:04.793Z
Really helpful answer, thanks! I have some reading to do
Jonathan
CC BY-SA 4.0
2022-06-08T15:35:13.113Z
I think you're incorrect in invoking the Uzyczyn conjecture here Andras: typability of an (unannotated) term does not necessarily translate into the size of the computable functions $\mathbb{N}\rightarrow\mathbb{N}$: e.g. *all* normal forms are typeable in system F (but they aren't necessarily typed *as functions* $\mathbb{N}\rightarrow\mathbb{N}$)
cody
CC BY-SA 4.0
2022-06-08T15:37:06.807Z
I should also note that $\mathrm{F}_1$ is *not* system $\mathrm{F}$: rather it is the system which additionally allows constructors of sort $*\rightarrow *$.
cody
CC BY-SA 4.0
2022-06-08T17:38:58.380Z
@cody: OK, thanks. Then, do you know a reference for the strength of F-omega? Also, for that CoC has the same strength as F-omega.
András Kovács
CC BY-SA 4.0
2022-06-08T19:45:36.333Z
Kind of for the second one (but not for the first), let me write up an answer.
cody
CC BY-SA 4.0
2022-06-08T06:06:48.373Z
2022-06-08T21:41:08.493Z
2022-06-08T21:41:08.493Z
András Kovács
<p>My understanding of András' answer is that, while it gets the gist correct, his final conclusion is not quite right: The &quot;standard&quot; way to determine the strength of the function space in a logical calculus, like CoC is traditionally via <em>realizability</em>, as was used by Girard to justify the strength of <span class="math-container">$\mathrm{HA}_2$</span> having exactly the <code>nat -&gt; nat</code> functions of system F as definable functions.</p>
<p>However in CoC, it's possible to directly look at the proof terms, and &quot;erase&quot; parts of it to obtain system <span class="math-container">$\mathrm{F}_\omega$</span> terms, which have the same reduction behavior in the case of <code>nat -&gt; nat</code> functions. This is done in detail in section 5.3 of Barendregt's <a href="https://home.ttic.edu/%7Edreyer/course/papers/barendregt.pdf" rel="noreferrer">Lambda Calculi with Types</a>, which he attributes to Berardi.</p>
<p>I suspect a realizability argument along the lines of the one given by Berger and Hou in <a href="https://www.semanticscholar.org/paper/A-realizability-interpretation-of-Church%27s-simple-Berger-Hou/21ad7e205990fadcc3588e59484ea4fb40995257" rel="noreferrer">A realizability interpretation of Church's simple theory of types</a> would additionally show that all of Church's simple type theory can be accounted for, i.e. the provably definable functions of that theory are exactly those definable in system <span class="math-container">$\mathrm{F}_\omega$</span>.</p>
<p>This would mean that there are strictly more such functions in CoC than in system F, by some standard Gödelian argument.</p>
<p>Why does this not contradict the conjecture András refers to? I actually asked this to Pawel Uzyczyn a while back: the question asked there is actually about which <em>untyped</em> terms can be assigned <em>some</em> type in various systems. There is no guarantee that <span class="math-container">$\mathrm{F}_\omega$</span> and <span class="math-container">$\mathrm{F}_1$</span> would assign the <em>same</em> type, much less the type <code>nat -&gt; nat</code>! As such, the question is more about type assignment systems than logical theories.</p>

CC BY-SA 4.0
2022-06-08T21:38:32.747Z
Did you mean "all of CoC can be accounted for"?
András Kovács
CC BY-SA 4.0
2022-06-08T21:55:27.567Z
No, but my phrasing is unclear: I meant "CSTT is a well-known theory that is also exactly at the same expressiveness". In some ways, CoC and CSTT are incomparable: CoC has dependent types, and CSTT has axioms.

CSTT is an appropriate environment to formalize large parts of math, CoC needs at least a couple axioms to be suitable.
cody
CC BY-SA 4.0
2022-06-08T20:17:03.997Z
2022-06-08T20:17:03.997Z
cody
<p>The calculus of constructions (CoC) without <code>fix</code> is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: Is there a decidable problem that cannot be computed in the CoC?</p>
<p>I found Statman's theorem, which says that the simply typed lambda calculus is limited computationally (I think? I find it hard to understand), but I'm pretty sure the CoC should be more powerful than the simply typed lambda calculus. Are there any theoretical results on that?</p>

<type-theory><lambda-calculus><calculus-of-constructions>
What is the computational power of the Calculus of Constructions?
Jonathan
# What is the computational power of the Calculus of Constructions?

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

The calculus of constructions (CoC) without `fix` is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: Is there a decidable problem that cannot be computed in the CoC?

I found Statman's theorem, which says that the simply typed lambda calculus is limited computationally (I think? I find it hard to understand), but I'm pretty sure the CoC should be more powerful than the simply typed lambda calculus. Are there any theoretical results on that?

**Tags:** type-theory, lambda-calculus, calculus-of-constructions

---

## 2 answers

### Answer by username_1 on 2022-06-08. Score: 7 | Accepted answer

There is no total language where all total computable $\mathbb{N} \to \mathbb{N}$ functions are definable. In a total language, an interpreter for the same language is not definable because if it were then general recursion could be recovered by diagonalization; [see theorem 3.2 here](https://dl.acm.org/doi/pdf/10.1145/2837614.2837623?casa_token=XyBfL2RjntIAAAAA:tsuq5dPxcyxpIIlrcI0k6BxNTmWlOyYivlCaSmF73A-dmmZvd9BYIklnAf74cCaTpbO2WufhNaDw). This is analogous to Gödel's second incompleteness theorem.

The range of definable total functions in a theory is called *proof-theoretic strength*. The calculus of constructions has the same strength as System F$\omega$. That is in turn at least as strong as System F, and probably strictly stronger (see cody's answer). System F has the same strength as second-order arithmetic. You can read about this in chapter 15 of Girard's [Proofs and Types](http://tlca.di.unito.it/opltlca/opltlca.pdf). Second-order arithmetic is in turn weaker than ZFC, but it's strong enough to be beyond the reach of [ordinal analysis](https://ncatlab.org/nlab/show/ordinal+analysis), which tries to measure proof-theoretic strength by ordinal notations.

EDIT: taking cody's remarks into account.

> **Comments:**
> **username_2**: A mminor quibble: in the last sentence, it is better to say "by ordinal notations" or "by ordinal number notations".  
> **username_1**: @AndrejBauer fair point. Edited.  
> **username_0**: Really helpful answer, thanks! I have some reading to do  
> **username_3**: I think you're incorrect in invoking the Uzyczyn conjecture here Andras: typability of an (unannotated) term does not necessarily translate into the size of the computable functions $\mathbb{N}\rightarrow\mathbb{N}$: e.g. *all* normal forms are typeable in system F (but they aren't necessarily typed *as functions* $\mathbb{N}\rightarrow\mathbb{N}$)  
> **username_3**: I should also note that $\mathrm{F}_1$ is *not* system $\mathrm{F}$: rather it is the system which additionally allows constructors of sort $*\rightarrow *$.  
> **username_1**: @cody: OK, thanks. Then, do you know a reference for the strength of F-omega? Also, for that CoC has the same strength as F-omega.  
> **username_3**: Kind of for the second one (but not for the first), let me write up an answer.  

---

### Answer by username_3 on 2022-06-08. Score: 6

My understanding of András' answer is that, while it gets the gist correct, his final conclusion is not quite right: The "standard" way to determine the strength of the function space in a logical calculus, like CoC is traditionally via *realizability*, as was used by Girard to justify the strength of $\mathrm{HA}\_2$ having exactly the `nat -> nat` functions of system F as definable functions.

However in CoC, it's possible to directly look at the proof terms, and "erase" parts of it to obtain system $\mathrm{F}\_\omega$ terms, which have the same reduction behavior in the case of `nat -> nat` functions. This is done in detail in section 5.3 of Barendregt's [Lambda Calculi with Types](https://home.ttic.edu/%7Edreyer/course/papers/barendregt.pdf), which he attributes to Berardi.

I suspect a realizability argument along the lines of the one given by Berger and Hou in [A realizability interpretation of Church's simple theory of types](https://www.semanticscholar.org/paper/A-realizability-interpretation-of-Church%27s-simple-Berger-Hou/21ad7e205990fadcc3588e59484ea4fb40995257) would additionally show that all of Church's simple type theory can be accounted for, i.e. the provably definable functions of that theory are exactly those definable in system $\mathrm{F}\_\omega$.

This would mean that there are strictly more such functions in CoC than in system F, by some standard Gödelian argument.

Why does this not contradict the conjecture András refers to? I actually asked this to Pawel Uzyczyn a while back: the question asked there is actually about which *untyped* terms can be assigned *some* type in various systems. There is no guarantee that $\mathrm{F}\_\omega$ and $\mathrm{F}\_1$ would assign the *same* type, much less the type `nat -> nat`! As such, the question is more about type assignment systems than logical theories.

> **Comments:**
> **username_1**: Did you mean "all of CoC can be accounted for"?  
> **username_3**: No, but my phrasing is unclear: I meant "CSTT is a well-known theory that is also exactly at the same expressiveness". In some ways, CoC and CSTT are incomparable: CoC has dependent types, and CSTT has axioms.  CSTT is an appropriate environment to formalize large parts of math, CoC needs at least a couple axioms to be suitable.  

---

