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

Question

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.

Answer 1

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

Answer 2

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.

Answer 3

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.