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 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 @cody'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 @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.