Halting problem unsolvability leads to a contradiction - where's the mistake?

Question

You are all familiar with the halting problem so I won't repeat it.

Suppose $H$ is a Turing machine which takes as input an encoding of another Turing machine $M$, then searches all possible proof strings until it finds a proof that $M$ halts or a proof that $M$ does not halt. Of course, if there is no such proof then it will search forever, so I do not claim that $H$ decides the halting problem.

Suppose $Q$ is the usual counterexample that first invokes $H$ on $Q$ as a subroutine (this is possible using quine techniques). Then if $H$ reports that $Q$ doesn't halt, it halts. If $H$ reports that $Q$ does halt, it enters a trivial infinite loop.

Now consider what the subroutine $H$ returns. If $H$ would report that $Q$ would halt, that would mean it had found a specific proof that $Q$ would halt, despite the fact that $Q$ obviously would not halt and we could see it enter a trivial infinite loop after a finite number of steps. Assuming that the proof system is consistent, we can be certain that there is no proof that $Q$ halts. Likewise, we can be certain that there is no proof that $Q$ does not halt.

Since there is no proof that $Q$ halts and no proof that $Q$ does not halt, we can be certain that $H$ will never find either one, therefore the $H$ subroutine of $Q$ will continue searching proofs forever, QED. We have proved that $Q$ does not halt.

Wait, what? The fact there is no proof gives a proof. Of course, if there is a proof, that proof is wrong. What's going on here? Where is the error in my reasoning?

(Credits to raoof for the "proof" sketch)

Answer 1

This is a very natural question, and it hinges on a logical subtlety: when you describe the machine $H$'s behavior as

search[ing] all possible proof[s] until it finds a proof that $M$ halts or a proof that $M$ does not halt,

what exactly do you mean by "proof"? The only way you derive a contradiction is if there is some system $T$ such that (i) by "proof" you mean "proof in $T$" and (ii) the argument of your post goes through in $T$. However, one crucial assumption you've made about proofs in your post is that they are correct: we never prove false halting or non-halting facts. This means that the argument of your post can't go through in the same theory that it implicitly talks about, by (a consequence of) Godel's second incompleteness theorem. So you don't get a contradiction at all.

At the end of the day, what you're essentially doing is proving that the halting problem is creative.

---

The following might help clarify the situation. Let $T$ be a "reasonable" theory (e.g. any consistent r.e. extension of Robinson arithmetic), and let $A_T,B_T$ be the "$T$-solvable parts" of the halting problem: $A_T$ is the set of machines $T$ proves halt, and $B_T$ is the set of machines $T$ proves don't halt. Then we have:

• $A_T$ and $B_T$ are disjoint r.e. sets, and the halting problem is a proper subset of $A_T$.

• If $T$ is $\Sigma_1$-sound, then $A_T$ is exactly the usual halting problem.

• Meanwhile, since Robinson arithmetic is $\Sigma_1$-complete, we have by mere consistency of $T$ that $B_T$ is disjoint from the true halting problem.

• But (almost) none of the above is provable in $T$ itself, since $T$ doesn't even know that $T$ is consistent.

Answer 2

Of course, if there is no such proof then it will search forever.

This is your mistake: since we permit $H$ to loop forever, the language accepted by $H$ is recognizable but not necessarily decidable. The conventional proof is that Halting Problem is undecidable – that no $H$ exists that can accept or reject any input TM in finite time.

The existence of the Universal Turing Machine proves the Halting Problem to be recognizable, as one can simply simulate any input TM and accept the ones that halt in finite time.

Answer 3

The "halting problem" is about finding a Turing machine X that DECIDEs whether another Turing machine Y halts with input Z, for every Y and Z. You were instead talking about a Turing machine that RECOGNIZEs whether another Turing machine halts. That is a very different problem. And building a halting recognizer is trivial and doesn't lead to conflicts (well, it's an awful lot of work to build it, but not difficult).

For a DECIDER to exist, it must be true that for every Turing machine Y and input Z either there is a proof that Y halts on input Z, or there is a proof that Y doesn't halt on input Z. And that isn't true.