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

110 Views Asked by At

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.

1

There are 1 best solutions below

2
On BEST ANSWER

$\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."