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?

`for p in proofs`

etc) to someone else. $\endgroup$this commentproves M halts, and M eventually finds this comment, so… $\endgroup$3more comments