# If two Turing machines halt iff they find a proof that the other halts, does either of them necessarily halt?

This question was inspired by this excellent question on MathOverflow.

Assume that there are two Turing machines $$M$$ and $$N$$ that search through all ZFC proofs in some order, and if either of them finds a proof that the other halts, then it would halt. If the machines are identical in design, then, by the answers on the MathOverflow question, they would halt. However, if the machines are different, can they continue running forever or would one of them halt at some point? If one halts, then the other would halt because it was proven to halt.

• I think yes, arguing as follows: arguing as in the other thread, we have that if "$M_1$ halts or $M_2$ halts" is (provably) provable (which, as I understand, is your hypothesis), then (provably) $M_1$ halts or $M_2$ halts. Then, as you say, it follows that they both in fact halt. It'd rather not post this as an answer, though, since I may not have enough background to miss some nuances here. Commented Dec 27, 2022 at 2:23
• Both might run forever, however... Commented Dec 27, 2022 at 2:24
• If provably one of them halts, then no, they can't. Commented Dec 27, 2022 at 2:26
• How did you interpret my question? Commented Dec 27, 2022 at 2:26
• That you have two Turing machines with the property that each of them halts if the other provably halts, and you ask whether they do, in fact, halt. Commented Dec 27, 2022 at 2:28

$$\mathsf{ZFC}$$-provably, both machines will halt. The argument is pretty much identical to the MO question you linked to: it's a consequence of Lob's theorem and $$\Sigma_1$$-completeness of the theory involved.
Let's focus on $$M$$ WLOG (the proof for $$N$$ is identical).
The following reasoning takes place in $$\mathsf{ZFC}$$: suppose $$\mathsf{ZFC}$$ proves that $$M$$ halts. Then $$N$$ will find such a proof, and so $$N$$ will halt. Since $$\mathsf{ZFC}$$ is $$\Sigma_1$$-complete, this means that $$\mathsf{ZFC}$$ can prove "$$N$$ halts" and so $$M$$ will eventually halt.
This means that $$\mathsf{ZFC}$$ proves "If $$\mathsf{ZFC}$$ proves that $$M$$ halts, then $$M$$ halts." But applying Lob's theorem, this gives us a $$\mathsf{ZFC}$$-proof of "$$M$$ halts."
• @mathlander A theory is $\Sigma_1$-complete if it proves every true $\Sigma_1$ fact about the natural numbers. Equivalently, it proves all true (but not necessarily only true) halting facts about specific Turing machines on specific inputs. $\mathsf{ZFC}$ is $\mathsf{ZFC}$-provably $\Sigma_1$-complete; see here. Commented Dec 27, 2022 at 4:32