# Can a program exist that halts only if it can prove that it doesn't halt?

Consider a program P that enumerates possible proofs in some proof system and halts only if it finds a valid proof that P does not halt. Clearly no such proof exists, or the program would eventually find it, causing a contradiction. But that argument itself appears to constitute exactly such a proof. It seems like that means that P cannot exist (for proof systems sufficiently powerful to express that argument), but I can't otherwise see why that should be the case.

• I think you are correct. However, you will need to formally define what proof system you are using, and make sure that you can write out the statement "P doesn't halt" in this proof system. – nir shahar Apr 27 at 17:14
• Also the proof you wrote here would still be required to be a proof that $P$ doesn't exist using that sufficiently strong proof system – nir shahar Apr 27 at 17:24
• This means its practically impossible to formally define and prove this statement, however it is still an interesting thinking problem :) – nir shahar Apr 27 at 17:25
• @nirshahar: It is not correct; such a program can exist, and the error is somewhere else. – user21820 Apr 28 at 7:21
• I can write lots of software programs/funcs/apps which won't prove they cannot halt, so they never will halt. I think your statement needs to be a bit more specific, i.e. that the program is "honestly" trying to prove said contradiction. – Carl Witthoft Apr 29 at 17:41

We can define a sound proof system as a computable function $$\Pi$$ which maps strings (proofs) to strings (statements proved), with the following property: if $$\Pi(\pi) = p$$, then $$p$$ encodes a true statement. We think of $$\pi$$ as a proof of $$p$$. (If $$\pi$$ is not a valid proof, then $$\Pi$$ outputs some fixed true statement.) We consider sound proof systems which are rich enough to prove statements about the halting of Turing machines.

Let $$Q(q)$$ be the program that enumerates over all strings, and halts if it ever finds a string $$\pi$$ such that $$\Pi(\pi) = p$$, where $$p$$ is an encoding of "The Turing machine encoded by $$q$$ never halts when run on $$q$$". Let $$[Q]$$ be an encoding of $$Q$$. If we run $$Q$$ on $$[Q]$$, then $$Q$$ halts iff there is a $$\Pi$$-proof that $$Q$$ doesn't halt when running on $$[Q]$$.

(Using the recursion theorem, we can transform $$Q$$ to a Turing machine $$P$$ which runs $$Q$$ on $$[P]$$, which is the setup in the original post.)

If there is a $$\Pi$$-proof that $$Q$$ doesn't halt when running on $$[Q]$$, then $$Q$$ doesn't halt when running on $$[Q]$$. We conclude that there cannot be any $$\Pi$$-proof that $$Q$$ doesn't halt when running on $$[Q]$$, because if such a $$\Pi$$-proof existed, then $$Q$$ would halt when running on $$[Q]$$. Therefore $$Q$$ doesn't halt when running on $$[Q]$$. However, there is no $$\Pi$$-proof of this fact.

This is an example of incompleteness. The proof system $$\Pi$$ is unable to formalize the argument above. One reason is that $$\Pi$$ cannot even prove its own consistency (i.e., that it does not prove a contradiction, as per Gödel's second incompleteness theorem), not to say soundness (which $$\Pi$$ may not even be able to express).

• Comments are not for extended discussion; this conversation has been moved to chat. – D.W. May 10 at 6:44

Your program P may halt if the proof system it is using is inconsistent, allowing it to prove a self-contradictory statement.

The fact that no (sufficiently expressive) proof system can prove its own consistency is exactly what is shown by Gödel's second incompleteness theorem (which, not coincidentally, is in many ways analogous to Turing's halting theorem).

So, in short, your program P will never halt if the proof system it uses is consistent. But that's not something P, or anything else using the same proof system, can prove.

Nor, for that matter, can we definitely and objectively prove that any sufficiently complex proof system is consistent, since the only way to do that would be using a "meta-proof" in some other, more powerful proof system whose consistency we would then also need to prove…

In fact, if the proof system used by P features the principle of explosion, which allows deducing any statement from a contradiction, then P will halt if and only if that proof system is inconsistent — since if it is, P will eventually find a proof that first proves a contradictory statement and then deduces "P does not halt" from it. Or at least that's what P will do if it indeed correctly enumerates and evaluates all valid proofs in the system, which is something that we again cannot prove in general without making use of some proof system subject to the incompleteness theorem.

Succinctly, your argument (that there is no such proof that P does not halt) is a proof but not in the same proof system that P is using to search for proofs! In fact, this very kind of computability-based argument can be used to great effect to prove the generalized incompleteness theorems, even the Rosser strengthening.