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

Question

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).

Answer 1

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!

Answer 2

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.