<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 username_3'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 username_3'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**: @username_2 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**: @username_3: 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 username_1' 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 username_1 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.  

---

