Is there an effective theory which "solves" the halting problem?

I'm looking for an effective theory $T$ that solves the halting problem, in the sense that for every Turing machine $M$, $T$ either proves that $M$ halts, or that it does not halt.

On the face of it, this would violate Turing's theorem that you can not solve the halting problem. The trick is that $T$ would not actually be sound, i.e., there would be at least one Turing machine $M$ such that $T$ proves that $M$ halts, but it really doesn't. (So it would not actually solve the halting problem.) (For example $PA+\lnot Con(PA)$ proves that the Turing machine that looks for a contradiction in $PA$ halts, when it in fact this machine does not.)

As to avoid trivial answers (such as a theory that simply asserts that every turing machine halts), I'm also going to require that $T$ proves all the axioms of PA, and is consistient.

Some notes:

• Since Turing's theorem can be internalized to $T$ (since it can in $PA$), $T$ can proves that $T$ does not solve the halting problem. This is okay though, since $T$ is not sound.
  • This implies that in any model of $T$, there would be a nonstandard Turing machine $M$ such that $T$ cannot prove whether or not $M$ halts.
• $T$ proves that $T$ is inconsistent, since it would proves that the machine that looks for a contradiction in $T$ halts (otherwise, it would need to prove that this machine does not halt, proving itself consistent, in violation of Goedel's second incompleteness theorem).

No such $T$ exists (at least, no such $T$ extending PA (or similar) exists). The key fact is that the recursion theorem is internal, in the following sense:

For each $e$, there is some $c$ such that PA proves the sentence "If $\Phi_e$ is total, then $\Phi_{\Phi_e(c)}\cong\Phi_c$."

In fact, the proof and the $c$ are just the usual ones - the point being that PA is strong enough to prove that the index constructed in the proof of the recursion theorem does what it should!

We now apply the recursion theorem, "internalized" as above, in the natural way. Let $T$ be a consistent computably axiomatized theory extending PA. By the internal recursion theorem, we can find an $e$ such that PA proves:

• If $T$ proves $\Phi_e(e)\downarrow$ before it proves $\Phi_e(e)\uparrow$ (that is, via a proof which appears first in some standard ordering of proofs), then $\Phi_e(e)\uparrow$.

• If $T$ proves $\Phi_e(e)\uparrow$ before it proves $\Phi_e(e)\downarrow$, then $\Phi_e(e)\downarrow$.

• If $T$ proves neither, then $\Phi_e(e)\uparrow$.

(First think about why an $e$ with these properties exists classically, using the recursion theorem as normally stated.)

Since $T$ extends PA, $T$ also proves these facts. But then if $T$ solves the halting problem in your sense, it is inconsistent:

• If $T$ proves $\Phi_e(e)\downarrow$ before it proves $\Phi_e(e)\uparrow$, then $T$ sees that, and so by the above $T$ also proves $\Phi_e(e)\uparrow$.

• If $T$ proves $\Phi_e(e)\uparrow$ before it proves $\Phi_e(e)\downarrow$, then $T$ sees that, and so by the above $T$ also proves $\Phi_e(e)\downarrow$.

In fact, what we've really shown is that the sets of indices which PA proves halt and which PA proves don't halt are recursively inseparable!

You're asking for a theory $T$ such that (1) $T$ is recursively axiomatized, (2) $T$ extends $PA$, (3) if a Turing machine $M$ halts, then $T$ proves that $M$ halts, and (4) for every Turing machine $M$, either $T$ proves that $M$ halts, or $T$ proves that it doesn't. We will argue that no such $T$ exists by way of the well-known

$\bf Theorem\ of\ Kleene:$ There is a pair of computably enumerable sets $A, B$ of natural numbers such that $A \cap B = \emptyset$, and such that for no computable set $C$ do we have $A \subseteq C \subseteq \bar B$, where $\bar B$ is the complement of $B$. Such a pair $A,B$ is called $\it computably\ inseparable$.

Fix $A$ and $B$ as in the theorem. We claim that if your $T$ exists, then we can exhibit a computable $C$ of the kind forbidden by the theorem, a contradiction. For each $n$, let $M_n$ be a Turing machine which halts if $n$ enters $A$ without first entering $B$, and let $M_n'$ be one that halts if $n$ enters $B$ without first entering $A$. (Although $A$ and $B$ are disjoint, the 'without first' clause can still come into play in nonstandard models.) Now fix $n$; we will decide whether to put $n$ into $C$ or into its complement $\bar C$. Since $T$ is consistent, it doesn't prove that both $M_n$ and $M_n'$ halt. If $T$ proves $M_n$ halts, put $n$ into $C$; if $T$ proves $M_n'$ halts, put $n$ into $\bar C$; and if neither of these happens, then by design of $T$, it proves that both fail to halt, and we arbitrarily put $n$ into $C$.

Doing this for every $n \in \mathbb{N}$, we arrive at a computable $C$. We claim that $A \subseteq C$ and $B \subseteq \bar C$. To see $A \subseteq C$, fix any $n \in A$, and notice that $M_n$ halts, so that by choice of $T$, $T$ proves that $M_n$ halts, and therefore we placed $n$ into $C$ in the construction. The proof that $B \subseteq \bar C$ is similar. Thus $C$ is a computable separator for $A$ and $B$, as forbidden by the theorem above, and we are done.