Is there a typed lambda calculus which is consistent and Turing complete? 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: @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)?
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 shows that one of the following must hold:


The set of all well-typed programs is not Turing Complete.
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:


There is an undecidable type system, the intersection type system 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.
There is a class of type systems, the Pure Type Systems, 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 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.