Skip to main content
1 of 3
Joel David Hamkins
  • 236.4k
  • 44
  • 777
  • 1.4k

The answer is yes, the machine will find a proof of its own halting, and it will halt when it does so.

I claim this is a consequence of Löb's theorem. Let $M$ be a Turing machine such as you describe. Note that it is not quite correct to say "the" Turing machine that does what you say, since there will be infinitely many different machines $M$ that search for proofs that they themselves halt. It may not be clear initially that they all have the same behavior, but let me show that indeed that they do.

Let $\psi$ be the assertion "$M$ halts." Thus, we can prove in ZFC that if $\psi$ is provable, then it is true, since $M$ would discover the proof. Thus, ZFC proves $\text{Pr}_{ZFC}(\ulcorner\psi\urcorner)\to\psi$. But this is exactly the situation that Löb's theorem is about, and it tells us that we can prove $\psi$ directly in ZFC. So we have proved that $M$ halts, as I claimed.

Incidentally, regarding the negated version and the proof of the incompleteness theorem you mention at the end of the post, these ideas are also the basis of the universal algorithm. See my paper The modal logic of arithmetic potentialism and the universal algorithm.

Joel David Hamkins
  • 236.4k
  • 44
  • 777
  • 1.4k