patternMajor
Can a program exist that halts only if it can prove that it doesn't halt?
Viewed 0 times
haltscanprogramexistprovedoesnthathaltonly
Problem
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.
Solution
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).
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).
Context
StackExchange Computer Science Q#139590, answer score: 20
Revisions (0)
No revisions yet.