[Math] n effective theory which “solves” the halting problem

computabilitycomputer sciencelogicmeta-mathpeano-axioms

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

Best Answer

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!

Related Question