<p>Alright I'll give a crack at it: In general for a given type system $T$, the following is true:</p>

<blockquote>
  <p><strong>If</strong> all well-type terms in the calculus $T$ are normalizing, then $T$ is <em>consistent</em> when viewed as a logic.</p>
</blockquote>

<p>The proof generally proceeds by assuming you have a term $\mathrm{absurd}$ of type $\mathrm{False}$, using subject reduction to get a normal form, and then proceeding by induction on the structure of such a term to get a contradiction.</p>

<p>It is natural to wonder if the converse holds, i.e.</p>

<blockquote>
  <p>For any type system $T$, if $T$ is <em>logically consistent</em>, then every well-typed term in $T$ is normalizing.</p>
</blockquote>

<p>The problem with this is that there is no real most general notion of "type system", and even less agreement on the meaning of logical consistency for such systems. However, we can empirically verify that</p>

<blockquote>
  <p>For <em>most known type systems</em> which have a logical interpretation, the converse does indeed hold.</p>
</blockquote>

<p>How does this tie into Turing Completeness? Well, for one, if type-checking is <strong>decidable</strong>, then <a href="https://cstheory.stackexchange.com/questions/24986/a-total-language-that-only-a-turing-complete-language-can-interpret/24994#24994">Andrej's argument</a> shows that one of the following <em>must</em> hold:</p>

<ol>
<li>The set of all well-typed programs is <em>not</em> Turing Complete.</li>
<li>There is a non-terminating well typed program.</li>
</ol>

<p>This tends to suggest that:</p>

<blockquote>
  <p>Type systems which have a logical interpretation <strong>and</strong> are consistent <strong>and</strong> are recursively enumerable are <strong>not</strong> Turing Complete.</p>
</blockquote>

<p>Giving an actual theorem rather than a suggestion requires making the notion of type systems and logical interpretations mathematically precise.</p>

<p>Now two remarks come to mind:</p>

<ol>
<li><p>There is an <em>undecidable</em> type system, the <a href="http://projecteuclid.org/download/pdf_1/euclid.ndjfl/1040067315" rel="noreferrer">intersection type system</a> which has a logical interpretation and can represent every normalizing $\lambda$-term. As you remark, this isn't quite the same as being Turing Complete, as the type of a total function may need to be updated (refined, in fact) before applying it to the desired argument. The calculus is a "curry style" calculus and is equal to STLC +
$$ \frac{\Gamma\vdash M:\tau\quad \Gamma\vdash M:\sigma}{\Gamma\vdash M:\tau\cap\sigma} $$
and
$$\frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\tau}\quad \frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\sigma}$$
It is clear that the "interpretation" $\cap=\wedge$ leads to a consistent logical interpretation.</p></li>
<li><p>There is a class of type systems, the <a href="http://en.wikipedia.org/wiki/Pure_type_system" rel="noreferrer">Pure Type Systems</a>, in which such a question might be made precise. In this framework however, the logical interpretation is less clear. One might be tempted to say: "a PTS is consistent if it has an uninhabited type". But this doesn't work, since types may live in different "universes", where some might be consistent and some not.
<a href="https://hal.inria.fr/inria-00159085/document" rel="noreferrer">Coquand and Herbelin</a> define a notion of <em>Logical Pure Type Systems</em>, in which the question makes sense, and show</p>

<blockquote>
  <p>Every inconsistent, <em>non-dependent</em> LPTS has a looping combinator (and so is Turing Complete)</p>
</blockquote>

<p>Which answers the question in one direction (inconsistent $\Rightarrow$ TC) in this case. As far as I know, the question for general LPTS is still open and quite difficult.</p></li>
</ol>

<hr>

<p><strong>Edit:</strong> The converse of the Coquand-Herbelin result is not as easy as I thought! Here is what I came up with so far.</p>

<p>A <em>Logical Pure Type System</em> is a PTS with (at least) the sorts $\mathrm{Prop}$ and $\mathrm{Type}$, (at least) the axiom $\mathrm{Prop}:\mathrm{Type}$ and (at least) the rule $(\mathrm{Prop},\mathrm{Prop},\mathrm{Prop})$, with the further requirement that there are no sorts of type $\mathrm{Prop}$.</p>

<p>Now I'm going to assume a particular statement of Turing Completeness: fix an LPTS $L$ and let $\Gamma$ be the context</p>

<p>$$ \Gamma = \mathrm{nat}:\mathrm{Prop},\ 0:\mathrm{nat},\ S:\mathrm{nat}\rightarrow \mathrm{nat}$$</p>

<p>$L$ is <em>Turing Complete</em> iff for every total computable function $f:\mathbb{N}\rightarrow\mathbb{N}$ there is a term $t_f$ such that
$$ \Gamma \vdash t_f : \mathrm{nat}\rightarrow \mathrm{nat}$$
and for every $n\in\mathbb{N}$
$$ t_f\ (S^n\ 0)\rightarrow^*_{\beta} S^{f(n)}\ 0$$</p>

<p>Now Andrej's diagonalization argument shows that there are non-terminating $t$ of type $\mathrm{nat}$.</p>

<p>Now it seems like we are half-way there! Given a non terminating term $\Gamma \vdash \mathrm{loop}:\mathrm{nat}$, we want to replace occurrences of $\mathrm{nat}$ by some generic type $A$ and get rid of $0$ and $S$ in $\Gamma$, and we will have our inconsistency ($A$ is inhabited in the context $A:\mathrm{Prop}$)!</p>

<p>Unfortunately this is where I get stuck, since it is easy to replace $S$ by the identity, but the $0$ is much harder to get rid of. Ideally we would like to use some Kleene recursion theorem, but I haven't figured this out yet.</p>

CC BY-SA 3.0
2015-04-30T19:42:00.833Z
OK, so first two clarifications about your remark (1). What do you mean when you say that this system of intersection types is not recursively enumerable? Certainly the set of theorems of the system is r.e., because you've given it as a straightforward sequent calculus. Also, the result I see proven in the paper you linked is that the terms typable in the system are exactly the strongly normalizing terms; but isn't that different from saying that it can type exactly the total computable functions? E.g., isn't $\lambda x. xx$ strongly normalizing, but not total?
Morgan Thomas
CC BY-SA 3.0
2015-04-30T19:45:57.547Z
Now a question about your remark (2). It looks to me like the theorem you quote is not what we're interested in. It says that for every non-dependent LPTS, if it's inconsistent then it's Turing complete. But we'd like to know whether for every LPTS, if it's Turing complete then it's inconsistent. Am I misunderstanding something here?
Morgan Thomas
CC BY-SA 3.0
2015-05-01T14:31:08.913Z
@MorganThomas: Ah, you are correct about the first point: what I meant to say is that the type system can not be *decidable*, that is, given $\Gamma, t, A$, the statement $\Gamma\vdash t:A$ is undecidable. I'll correct this in the post.
cody
CC BY-SA 3.0
2015-05-01T14:42:14.897Z
The second point: you are also correct that one can have a non-total function that is well-typed (though one may not necessarily apply it to a given argument). I'll amend the answer.
cody
CC BY-SA 3.0
2015-05-01T14:56:27.120Z
Third point. You are correct again! However the converse (in the special case of LPTS) is rather trivial. I'll outline the argument.
cody
CC BY-SA 3.0
2015-04-29T18:45:28.307Z
2015-05-01T21:24:01.263Z
2017-04-13T12:32:30.623Z
cody
<p>Here is an answer to a variant of @cody's precisification of my question. There is a consistent LPTS which is Turing complete in roughly @cody's sense, if we allow the introduction of additional axioms and $\beta$-reduction rules. Thus strictly speaking the system is <em>not</em> an LPTS; it is merely something much like one.</p>

<p>Consider the calculus of constructions (or your favorite member of the $\lambda$-cube). This is an LPTS, but we're going to add extra stuff which makes it not an LPTS. Choose constant symbols $\text{nat}, 0, S$, and add the axioms:</p>

<p>$$ \vdash \text{nat} : \ast $$
$$ \vdash 0 : \text{nat} $$
$$ \vdash S : \text{nat} \to \text{nat} $$</p>

<p>Index the Turing machine programs by natural numbers, and for each natural number $e$, choose a constant symbol $f_e$, add the axiom $f_e : \text{nat} \to \text{nat}$, and for all $e,x \in \mathbb{N}$, add the $\beta$-reduction rule</p>

<p>$$ f_e(x) \to_\beta \Phi_e(x), $$</p>

<p>where as usual $\Phi_e(x)$ is the output of the $e$th Turing machine program on $x$. If $\Phi_e(x)$ diverges then this rule doesn't do anything. Note that by adding these axioms and rules the system's theorems remain recursively enumerable, though its set of $\beta$-reduction rules is no longer decidable, but merely recursively enumerable. I believe we could easily keep the set of $\beta$-reduction rules decidable by spelling out explicitly the details of a model of computation in the syntax and rules of the system.</p>

<p>Now, this theory is clearly Turing complete in roughly @cody's sense, just by brute force; but the claim is that it's also consistent. Let's construct a model of it.</p>

<p>Let $U_1 \in U_2 \in U_3$ be three sets, such that:</p>

<ul>
<li>$\emptyset, \mathbb{N}, 0, S \in U_1$ (where $S$ is the successor function).</li>
<li>Each set is transitive; if $a \in b \in U_i$, then $a \in U_i$.</li>
<li>Each set is closed under the formation of function spaces; i.e., if $A, B \in U_i$, then $B^A \in U_i$.</li>
<li>Each set is closed under the formation of dependent products; i.e., if $A \in U_i$ and $f : A \to U_i$, then $\prod_{a \in A} f(a) \in U_i$.</li>
</ul>

<p>The existence of such sets follows, for example, from ZFC plus the axiom that every cardinal is bounded by an inaccessible cardinal; we can take each set $U_i$ to be a Grothendieck universe.</p>

<p>We define an "interpretation" to be a mapping $v$ from the set of variable names to elements of $U_2$. Given an interpretation $v$, we can define an interpretation $I_v$ of terms of the system in the evident way:</p>

<ul>
<li>$I_v(x) = v(x)$, for $x$ a variable name.</li>
<li>$I_v(\ast) = U_1, I_v(\Box) = U_2$.</li>
<li>$I_v(\text{nat}) = \mathbb{N}, I_v(0) = 0, I_v(S) = S$.</li>
<li>$I_v(f_e) = \Phi_e$, i.e., the function $\mathbb{N} \to \mathbb{N}$ defined by the $e$th Turing program.</li>
<li>$I_v(AB) = I_v(A)(I_v(B))$, if $I_v(A)$ is a function with $I_v(B)$ in its domain, or $I_v(AB) = 0$ otherwise (just an arbitrary choice).</li>
<li>$I_v(\lambda x : A. B)$ is the function which maps an element $a \in I_v(A)$ to $I_{v[x:=a]}(B)$.</li>
<li>$I_v(\Pi x : A. B) = \prod_{a \in I_v(A)} I_{v[x:=a]}(B)$.</li>
</ul>

<p>We have that for all terms $A$, $I_v(A) \in U_3$. Now we say that an interpretation $v$ satisfies $A : B$, written $v \models A : B$, if $I_v(A) \in I_v(B)$. We say that $\Gamma \models A : B$ if for all interpretations $v$, if $v \models x : C$ for all $(x : C) \in \Gamma$, then $v \models A : B$.</p>

<p>It is straightforward to check that if $\Gamma \vdash A : B$, then $\Gamma \models A : B$, so this is a model of the system. But, for any variables $x,y$, it is not the case that $y : \ast \models x : y$, because we can interpret $y$ by $\emptyset$, so the system is consistent.</p>

<p>Now, this is an answer to my original question, in the sense that this is something that it's reasonable to call a typed lambda calulus, which is consistent and Turing complete. However, it's not an answer to @cody's question, because this is not an LPTS, because of the addition of extra axioms and $\beta$-reduction rules. I imagine that the answer to @cody's question is much harder.</p>

CC BY-SA 3.0
2015-05-09T21:40:24.837Z
This is a nice answer, but I'm not sure you need to go through all those calisthenics to prove consistency: a term of type $A$ in the empty context can be "de-sugared" to a term in the CoC: I'll call the $f_e(x)\rightarrow \Phi_e(x)$ rules *$\iota$-rules* and keep $\beta$ for the usual ones. Perform all $\beta$-reductions (this terminates since you have only added constants), and replace every term of the form $f_e(x)$ by its reduct *if it has one*. The idea here is that the $\iota$-rules only operate on ground terms, so you can do all the $\beta$-reductions first to get them out of the way.
cody
CC BY-SA 3.0
2015-05-10T06:26:56.413Z
I think you're right. This is not my field, so I'm a bit clumsy doing things. :-) I think your proof works, and one interesting consequence, if I'm right, is that this theory doesn't have very much consistency strength. It looks like a potentially very powerful theory, since it has types and natural numbers, which should let you interpret set theory; but apparently you can't, because you can prove it consistent without using powerful set theory!
Morgan Thomas
CC BY-SA 3.0
2015-05-02T16:44:01.617Z
2015-05-02T17:02:35.447Z
2015-05-02T17:02:35.447Z
Morgan Thomas
<p>Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function?</p>

<p>This is admittedly an imprecise question, lacking a precise definition of "typed lambda calculus." I'm basically wondering whether there are either (a) known examples of this, or (b) known impossibility proofs for something in this area.</p>

<p>Edit: @cody gives a precise version of this question in his answer below: is there a logical pure type system (LPTS) which is consistent and Turing complete (in a sense defined below)?</p>

CC BY-SA 3.0
2015-04-26T11:09:33.750Z
There is no recursively axiomatizable calculus (lambda or otherwise) whose provably total recursive functions are all recursive functions, so your calculus would have to involve non-terminating terms.
Emil Jeřábek
CC BY-SA 3.0
2015-04-26T14:53:32.610Z
I published a proof on this forum once, as it keeps coming up. Let'see if I can find it.
Andrej Bauer
CC BY-SA 3.0
2015-04-26T15:57:07.947Z
[This answer](http://cstheory.stackexchange.com/questions/24986/a-total-language-that-only-a-turing-complete-language-can-interpret/24994#24994) has a theorem which says you can't have *any* sort of calculus that is both Turing-complete *and* total.
Andrej Bauer
CC BY-SA 3.0
2015-04-26T19:56:35.183Z
@EmilJeřábek: Just to clarify, are you stating something that would be true of such a system, but which is not meant to answer the question, or does your comment answer the question (in a way that I don't see)?
Morgan Thomas
CC BY-SA 3.0
2015-04-26T19:58:07.167Z
@AndrejBauer: I read your proof, but I'm having a hard time understanding how it fits into the picture. Are you expanding on Emil's point? Does your proof answer the question (in a way that I don't see)? Apologies for being slow.
Morgan Thomas
CC BY-SA 3.0
2015-04-26T20:10:51.603Z
It will likely answer your question once you make it sufficiently precise. I think Andrej’s proof is unnecessarily complicated (but it shows more): the point is simply that if there were an effectively described system where all recursive function were representable in such a way that you can syntactically certify that an expression is an honest representation of a recursive function (e.g., by checking that it is correctly typed in the system), then you would obtain a universal total recursive function, which is impossible.
Emil Jeřábek
CC BY-SA 3.0
2015-04-26T20:51:29.433Z
In my proof you can read "programming language" as "some sort of $\lambda$-calculus". Your "consistency" requirement translates to "the programming language is total" (for if you have diverging terms then the calculus is "inconsistent" in the sense that all types are inhabited). The theorem says that such a language cannot simulate itself, but "simulate itself" is a computable map, therefore no such language can be Turing-complete.
Andrej Bauer
CC BY-SA 3.0
2015-04-26T23:57:14.230Z
Of course a classic answer to this kind of question could be: typed $\lambda$-calculus with [intersection types](http://www.doc.ic.ac.uk/~svb/Research/Papers/Survey.pdf), since it types every (and only those) terms which are strongly normalizing. It's more of a philosophical question to ask whether or not the calculus admits a "Curry-Howard interpretation" though.
cody
CC BY-SA 3.0
2015-04-27T00:03:15.550Z
@AndrejBauer: OK, I am beginning to see what you and Emil are getting at. I guess the gap in my understanding is that I don't see why it follows from the existence of diverging terms that all types are inhabited. Why does that follow?
Morgan Thomas
CC BY-SA 3.0
2015-04-27T20:19:07.580Z
Well, it doesn't exactly follow. There are probably situations in which you could inhabit every type by fiat, without having any diverging terms (in $\lambda$-calculus we should probably say "normalizing" instead of "divirging"). But in nature the typical reason that all types are inhabited is existence of a fixed-point operator, which leads to divergent terms.
Andrej Bauer
CC BY-SA 3.0
2015-04-28T05:57:12.023Z
It's hard to be more precise here because the question is not precise.
Andrej Bauer
<type-theory><lambda-calculus><typed-lambda-calculus><curry-howard>
Is there a typed lambda calculus which is consistent and Turing complete?
Morgan Thomas
# Is there a typed lambda calculus which is consistent and Turing complete?

(Asked by: username_0 on 2015-04-26)

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function?

This is admittedly an imprecise question, lacking a precise definition of "typed lambda calculus." I'm basically wondering whether there are either (a) known examples of this, or (b) known impossibility proofs for something in this area.

Edit: @username_3 gives a precise version of this question in his answer below: is there a logical pure type system (LPTS) which is consistent and Turing complete (in a sense defined below)?

**Tags:** type-theory, lambda-calculus, typed-lambda-calculus, curry-howard

> **Comments:**
> **username_1**: There is no recursively axiomatizable calculus (lambda or otherwise) whose provably total recursive functions are all recursive functions, so your calculus would have to involve non-terminating terms.  
> **username_2**: I published a proof on this forum once, as it keeps coming up. Let'see if I can find it.  
> **username_2**: [This answer](http://cstheory.stackexchange.com/questions/24986/a-total-language-that-only-a-turing-complete-language-can-interpret/24994#24994) has a theorem which says you can't have *any* sort of calculus that is both Turing-complete *and* total.  
> **username_0**: @EmilJeřábek: Just to clarify, are you stating something that would be true of such a system, but which is not meant to answer the question, or does your comment answer the question (in a way that I don't see)?  
> **username_0**: @AndrejBauer: I read your proof, but I'm having a hard time understanding how it fits into the picture. Are you expanding on Emil's point? Does your proof answer the question (in a way that I don't see)? Apologies for being slow.  
> **username_1**: It will likely answer your question once you make it sufficiently precise. I think Andrej’s proof is unnecessarily complicated (but it shows more): the point is simply that if there were an effectively described system where all recursive function were representable in such a way that you can syntactically certify that an expression is an honest representation of a recursive function (e.g., by checking that it is correctly typed in the system), then you would obtain a universal total recursive function, which is impossible.  
> **username_2**: In my proof you can read "programming language" as "some sort of $\lambda$-calculus". Your "consistency" requirement translates to "the programming language is total" (for if you have diverging terms then the calculus is "inconsistent" in the sense that all types are inhabited). The theorem says that such a language cannot simulate itself, but "simulate itself" is a computable map, therefore no such language can be Turing-complete.  
> **username_3**: Of course a classic answer to this kind of question could be: typed $\lambda$-calculus with [intersection types](http://www.doc.ic.ac.uk/~svb/Research/Papers/Survey.pdf), since it types every (and only those) terms which are strongly normalizing. It's more of a philosophical question to ask whether or not the calculus admits a "Curry-Howard interpretation" though.  
> **username_0**: @AndrejBauer: OK, I am beginning to see what you and Emil are getting at. I guess the gap in my understanding is that I don't see why it follows from the existence of diverging terms that all types are inhabited. Why does that follow?  
> **username_2**: Well, it doesn't exactly follow. There are probably situations in which you could inhabit every type by fiat, without having any diverging terms (in $\lambda$-calculus we should probably say "normalizing" instead of "divirging"). But in nature the typical reason that all types are inhabited is existence of a fixed-point operator, which leads to divergent terms.  
> **username_2**: It's hard to be more precise here because the question is not precise.  

---

## 2 answers

### Answer by username_3 on 2015-04-29. Score: 26

Alright I'll give a crack at it: In general for a given type system $T$, the following is true:

> **If** all well-type terms in the calculus $T$ are normalizing, then $T$ is *consistent* when viewed as a logic.

The proof generally proceeds by assuming you have a term $\mathrm{absurd}$ of type $\mathrm{False}$, using subject reduction to get a normal form, and then proceeding by induction on the structure of such a term to get a contradiction.

It is natural to wonder if the converse holds, i.e.

> For any type system $T$, if $T$ is *logically consistent*, then every well-typed term in $T$ is normalizing.

The problem with this is that there is no real most general notion of "type system", and even less agreement on the meaning of logical consistency for such systems. However, we can empirically verify that

> For *most known type systems* which have a logical interpretation, the converse does indeed hold.

How does this tie into Turing Completeness? Well, for one, if type-checking is **decidable**, then [Andrej's argument](https://cstheory.stackexchange.com/questions/24986/a-total-language-that-only-a-turing-complete-language-can-interpret/24994#24994) shows that one of the following *must* hold:

1. The set of all well-typed programs is *not* Turing Complete.
2. There is a non-terminating well typed program.

This tends to suggest that:

> Type systems which have a logical interpretation **and** are consistent **and** are recursively enumerable are **not** Turing Complete.

Giving an actual theorem rather than a suggestion requires making the notion of type systems and logical interpretations mathematically precise.

Now two remarks come to mind:

1. There is an *undecidable* type system, the [intersection type system](http://projecteuclid.org/download/pdf_1/euclid.ndjfl/1040067315) which has a logical interpretation and can represent every normalizing $\lambda$-term. As you remark, this isn't quite the same as being Turing Complete, as the type of a total function may need to be updated (refined, in fact) before applying it to the desired argument. The calculus is a "curry style" calculus and is equal to STLC +
   $$ \frac{\Gamma\vdash M:\tau\quad \Gamma\vdash M:\sigma}{\Gamma\vdash M:\tau\cap\sigma} $$
   and
   $$\frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\tau}\quad \frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\sigma}$$
   It is clear that the "interpretation" $\cap=\wedge$ leads to a consistent logical interpretation.
2. There is a class of type systems, the [Pure Type Systems](http://en.wikipedia.org/wiki/Pure_type_system), in which such a question might be made precise. In this framework however, the logical interpretation is less clear. One might be tempted to say: "a PTS is consistent if it has an uninhabited type". But this doesn't work, since types may live in different "universes", where some might be consistent and some not.
   [Coquand and Herbelin](https://hal.inria.fr/inria-00159085/document) define a notion of *Logical Pure Type Systems*, in which the question makes sense, and show

   > Every inconsistent, *non-dependent* LPTS has a looping combinator (and so is Turing Complete)

   Which answers the question in one direction (inconsistent $\Rightarrow$ TC) in this case. As far as I know, the question for general LPTS is still open and quite difficult.

---

**Edit:** The converse of the Coquand-Herbelin result is not as easy as I thought! Here is what I came up with so far.

A *Logical Pure Type System* is a PTS with (at least) the sorts $\mathrm{Prop}$ and $\mathrm{Type}$, (at least) the axiom $\mathrm{Prop}:\mathrm{Type}$ and (at least) the rule $(\mathrm{Prop},\mathrm{Prop},\mathrm{Prop})$, with the further requirement that there are no sorts of type $\mathrm{Prop}$.

Now I'm going to assume a particular statement of Turing Completeness: fix an LPTS $L$ and let $\Gamma$ be the context

$$ \Gamma = \mathrm{nat}:\mathrm{Prop},\ 0:\mathrm{nat},\ S:\mathrm{nat}\rightarrow \mathrm{nat}$$

$L$ is *Turing Complete* iff for every total computable function $f:\mathbb{N}\rightarrow\mathbb{N}$ there is a term $t\_f$ such that
$$ \Gamma \vdash t\_f : \mathrm{nat}\rightarrow \mathrm{nat}$$
and for every $n\in\mathbb{N}$
$$ t\_f\ (S^n\ 0)\rightarrow^\*\_{\beta} S^{f(n)}\ 0$$

Now Andrej's diagonalization argument shows that there are non-terminating $t$ of type $\mathrm{nat}$.

Now it seems like we are half-way there! Given a non terminating term $\Gamma \vdash \mathrm{loop}:\mathrm{nat}$, we want to replace occurrences of $\mathrm{nat}$ by some generic type $A$ and get rid of $0$ and $S$ in $\Gamma$, and we will have our inconsistency ($A$ is inhabited in the context $A:\mathrm{Prop}$)!

Unfortunately this is where I get stuck, since it is easy to replace $S$ by the identity, but the $0$ is much harder to get rid of. Ideally we would like to use some Kleene recursion theorem, but I haven't figured this out yet.

> **Comments:**
> **username_0**: OK, so first two clarifications about your remark (1). What do you mean when you say that this system of intersection types is not recursively enumerable? Certainly the set of theorems of the system is r.e., because you've given it as a straightforward sequent calculus. Also, the result I see proven in the paper you linked is that the terms typable in the system are exactly the strongly normalizing terms; but isn't that different from saying that it can type exactly the total computable functions? E.g., isn't $\lambda x. xx$ strongly normalizing, but not total?  
> **username_0**: Now a question about your remark (2). It looks to me like the theorem you quote is not what we're interested in. It says that for every non-dependent LPTS, if it's inconsistent then it's Turing complete. But we'd like to know whether for every LPTS, if it's Turing complete then it's inconsistent. Am I misunderstanding something here?  
> **username_3**: @MorganThomas: Ah, you are correct about the first point: what I meant to say is that the type system can not be *decidable*, that is, given $\Gamma, t, A$, the statement $\Gamma\vdash t:A$ is undecidable. I'll correct this in the post.  
> **username_3**: The second point: you are also correct that one can have a non-total function that is well-typed (though one may not necessarily apply it to a given argument). I'll amend the answer.  
> **username_3**: Third point. You are correct again! However the converse (in the special case of LPTS) is rather trivial. I'll outline the argument.  

---

### Answer by username_0 on 2015-05-02. Score: 11

Here is an answer to a variant of @username_3's precisification of my question. There is a consistent LPTS which is Turing complete in roughly @username_3's sense, if we allow the introduction of additional axioms and $\beta$-reduction rules. Thus strictly speaking the system is *not* an LPTS; it is merely something much like one.

Consider the calculus of constructions (or your favorite member of the $\lambda$-cube). This is an LPTS, but we're going to add extra stuff which makes it not an LPTS. Choose constant symbols $\text{nat}, 0, S$, and add the axioms:

$$ \vdash \text{nat} : \ast $$
$$ \vdash 0 : \text{nat} $$
$$ \vdash S : \text{nat} \to \text{nat} $$

Index the Turing machine programs by natural numbers, and for each natural number $e$, choose a constant symbol $f\_e$, add the axiom $f\_e : \text{nat} \to \text{nat}$, and for all $e,x \in \mathbb{N}$, add the $\beta$-reduction rule

$$ f\_e(x) \to\_\beta \Phi\_e(x), $$

where as usual $\Phi\_e(x)$ is the output of the $e$th Turing machine program on $x$. If $\Phi\_e(x)$ diverges then this rule doesn't do anything. Note that by adding these axioms and rules the system's theorems remain recursively enumerable, though its set of $\beta$-reduction rules is no longer decidable, but merely recursively enumerable. I believe we could easily keep the set of $\beta$-reduction rules decidable by spelling out explicitly the details of a model of computation in the syntax and rules of the system.

Now, this theory is clearly Turing complete in roughly @username_3's sense, just by brute force; but the claim is that it's also consistent. Let's construct a model of it.

Let $U\_1 \in U\_2 \in U\_3$ be three sets, such that:

* $\emptyset, \mathbb{N}, 0, S \in U\_1$ (where $S$ is the successor function).
* Each set is transitive; if $a \in b \in U\_i$, then $a \in U\_i$.
* Each set is closed under the formation of function spaces; i.e., if $A, B \in U\_i$, then $B^A \in U\_i$.
* Each set is closed under the formation of dependent products; i.e., if $A \in U\_i$ and $f : A \to U\_i$, then $\prod\_{a \in A} f(a) \in U\_i$.

The existence of such sets follows, for example, from ZFC plus the axiom that every cardinal is bounded by an inaccessible cardinal; we can take each set $U\_i$ to be a Grothendieck universe.

We define an "interpretation" to be a mapping $v$ from the set of variable names to elements of $U\_2$. Given an interpretation $v$, we can define an interpretation $I\_v$ of terms of the system in the evident way:

* $I\_v(x) = v(x)$, for $x$ a variable name.
* $I\_v(\ast) = U\_1, I\_v(\Box) = U\_2$.
* $I\_v(\text{nat}) = \mathbb{N}, I\_v(0) = 0, I\_v(S) = S$.
* $I\_v(f\_e) = \Phi\_e$, i.e., the function $\mathbb{N} \to \mathbb{N}$ defined by the $e$th Turing program.
* $I\_v(AB) = I\_v(A)(I\_v(B))$, if $I\_v(A)$ is a function with $I\_v(B)$ in its domain, or $I\_v(AB) = 0$ otherwise (just an arbitrary choice).
* $I\_v(\lambda x : A. B)$ is the function which maps an element $a \in I\_v(A)$ to $I\_{v[x:=a]}(B)$.
* $I\_v(\Pi x : A. B) = \prod\_{a \in I\_v(A)} I\_{v[x:=a]}(B)$.

We have that for all terms $A$, $I\_v(A) \in U\_3$. Now we say that an interpretation $v$ satisfies $A : B$, written $v \models A : B$, if $I\_v(A) \in I\_v(B)$. We say that $\Gamma \models A : B$ if for all interpretations $v$, if $v \models x : C$ for all $(x : C) \in \Gamma$, then $v \models A : B$.

It is straightforward to check that if $\Gamma \vdash A : B$, then $\Gamma \models A : B$, so this is a model of the system. But, for any variables $x,y$, it is not the case that $y : \ast \models x : y$, because we can interpret $y$ by $\emptyset$, so the system is consistent.

Now, this is an answer to my original question, in the sense that this is something that it's reasonable to call a typed lambda calulus, which is consistent and Turing complete. However, it's not an answer to @username_3's question, because this is not an LPTS, because of the addition of extra axioms and $\beta$-reduction rules. I imagine that the answer to @username_3's question is much harder.

> **Comments:**
> **username_3**: This is a nice answer, but I'm not sure you need to go through all those calisthenics to prove consistency: a term of type $A$ in the empty context can be "de-sugared" to a term in the CoC: I'll call the $f_e(x)\rightarrow \Phi_e(x)$ rules *$\iota$-rules* and keep $\beta$ for the usual ones. Perform all $\beta$-reductions (this terminates since you have only added constants), and replace every term of the form $f_e(x)$ by its reduct *if it has one*. The idea here is that the $\iota$-rules only operate on ground terms, so you can do all the $\beta$-reductions first to get them out of the way.  
> **username_0**: I think you're right. This is not my field, so I'm a bit clumsy doing things. :-) I think your proof works, and one interesting consequence, if I'm right, is that this theory doesn't have very much consistency strength. It looks like a potentially very powerful theory, since it has types and natural numbers, which should let you interpret set theory; but apparently you can't, because you can prove it consistent without using powerful set theory!  

---

