Consider the following Turing machine $M$: it searches over valid ZFC proofs, in lexicographic order, and if it finds a proof that $M$ halts, then it halts.


If we fix a particular model of Turing machine (say single-tape Turing machine), and if we fix an algorithm to verify that a given string is a valid ZFC proof of the fact that $M$ halts, this should constitute an unambiguous description of a Turing machine $M$.


(Standard arguments in computability theory, i.e., Kleene's recursion theorem, allows $M$ to compute functions of its own description).


Does $M$ halt?


I find this question puzzling because there's no apparent logical contradiction either way. There could be a proof, in which case it will halt. If there is no proof, then it doesn't halt. What would the answer "depend" on? $M$ either halts or doesn't halt, but could its behavior be independent of ZFC?


I should note that a closely related Turing machine $M'$ can be used to give a simple proof of Godel's incompleteness theorem. It's much more "rebellious" in its behavior, where if it finds a proof that it halts, it doesn't halt, and if it finds a proof that it doesn't halt, it halts. It follows that there cannot be a proof of its halting or non-halting in ZFC (unless ZFC is inconsistent).


However $M$ is just earnestly trying to figure out its fate. Which is it?



Will this Turing machine find a proof of its halting?
It is a very nice question. The answer is yes, the machine will find a proof of its own halting nature, and it will halt when it does so.


I claim this is a consequence of [Löb's theorem](https://en.wikipedia.org/wiki/L%C3%B6b%27s_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 they do all halt.


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 can prove in ZFC that $M$ halts, as I claimed. It follows that we can prove in PA and much less that $M$ halts, since once we have the actual ZFC proof that it halts, then we can prove in a very weak theory that the actual Turing machine computation halts in whatever specific number of steps it would take to verify the finding of it.


That argument uses the ZFC version of Löb's theorem, but we can get by with the standard PA version, even though M is searching for proofs in ZFC. The reason is that in PA we can prove that $\text{Pr}\_{PA}(\ulcorner\psi\urcorner)\to\psi$, since if PA proves that $M$ halts, then we can prove that ZFC will prove it as well, and so $M$ will halt. Thus, we need only the standard PA version of Löb's theorem to see that PA proves that $M$ halts.


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](https://arxiv.org/abs/1801.04599).


