Curry’s paradox in Turing machine land?

Question

Background

There’s an excellent question on MathOverflow that talks about the following: imagine that $M$ is a TM that searches over all ZFC proofs and halts if and only if it finds a proof that it halts. The answer is yes because it’s possible to adapt the logic behind Löb’s theorem to Turing machines.

At that question is a remarkable answer by Akiva Weinberger that spells out an explicit argument, based on the proof of Löb’s theorem, showing why this machine $M$ halts:

Build a second machine $N$. $N$ searches for a proof in ZFC of, "if $N$ halts then $M$ halts". If it finds one, it halts.

ZFC can argue as follows. "Suppose $N$ halts. Then it found a proof that if $N$ halts then $M$ halts. This, combined with the trace of $N$ halting, would be a ZFC proof that $M$ halts. Thus $M$ finds this and halts."

That paragraph is a ZFC proof that if $N$ halts then $M$ halts… which $N$ finds, so $N$ halts. Thus, by the same logic as above, there is a proof that $M$ halts, which it will find and then halt on.

Löb’s theorem is closely related to Curry’s paradox. Briefly, Curry’s paradox envisions a statement $P$ that says “if $P$ is true, then $\phi$ is true,” where $\phi$ is some arbitrary statement. The paradox is that this seems to imply that $\phi$ is true regardless of what $\phi$ is.

My Question

Pick any statement $\phi$. I’m going to argue that ZFC proves $\phi$. (Clearly it doesn’t, so there has to be a flaw in the following reasoning. However, I’m not sure what it is!) This is essentially a minimally-modified version of Akiva Weinberger’s MO answer but applied to Curry’s paradox rather than Löb’s theorem. To make it easier to see the changes, I’ve bolded all parts that differ from the original.

Consider a TM $M$ that searches over all ZFC proofs and halts if and only if it finds a proof of the statement “if $M$ halts, then $\phi$ is true.”

Build a second machine $N$. $N$ searches for a proof in ZFC of, "if $N$ halts, then if $M$ halts, then $\phi$ is true.” If it finds one, it halts.

ZFC can argue as follows. "Suppose $N$ halts. Then it found a proof that if $N$ halts, then if $M$ halts, then $\phi$ is true. This, combined with the trace of $N$ halting, would be a ZFC proof that if $M$ halts, then $\phi$ is true. Thus $M$ finds this and halts. This, combined with a trace of $M$ halting, would be a ZFC proof of $\phi$.

That paragraph is a ZFC proof that if $N$ halts, then if $M$ halts, then $\phi$ is true… which $N$ finds, so $N$ halts. Thus, by the same logic as above, there is a proof that $M$ halts, which it will find and then halt on. And since $M$ halts, a trace of $M$ halting, plus the preceding argument, gives a ZFC proof of $\phi$.

There has to be something wrong with the above argument, but I confess I’m not seeing what it is. Can someone point out where I’m telling lies? :-)

Answer 1

I don't see a contradiction anywhere. Let $\varphi$ be a statement in the language of $\mathsf{ZFC}$. Let $\ulcorner\varphi\urcorner$ be a string encoding $\varphi$. Let $\text{prov}(\ulcorner\varphi\urcorner)$ be the formula that says there exists a string encoding a proof of $\varphi$ from the axioms of $\mathsf{ZFC}$.

For a Turing machine $M$ and a string $\ulcorner M\urcorner$ encoding $M$, let $\text{halt}(\ulcorner M\urcorner)$ be the formula that says there exists a string encoding a run of $M$ halting on the empty input.

What you showed is that there is a Turing machine $M_\varphi$, encoded by a string $\ulcorner M_\varphi\urcorner$ such that $$\mathsf{ZFC}\vdash\text{halt}(\ulcorner M_\varphi\urcorner)\rightarrow\text{prov}(\ulcorner\varphi\urcorner)$$

and also that there is a Turing machine $N_\varphi$ encoded by $\ulcorner N_\varphi\urcorner$ such that $$\mathsf{ZFC}\vdash(\text{halt}(\ulcorner N_\varphi\urcorner)\land\text{halt}(\ulcorner M_\varphi\urcorner))\rightarrow\text{prov}(\ulcorner\varphi\urcorner)$$

but unless $\mathsf{ZFC}\vdash(\text{halt}(\ulcorner N_\varphi\urcorner)\land\text{halt}(\ulcorner M_\varphi\urcorner))$ or $\mathsf{ZFC}\vdash\text{halt}(\ulcorner M_\varphi\urcorner)$ you cannot conclude from this that $\mathsf{ZFC}\vdash\text{prov}(\ulcorner\varphi\urcorner)$.

It's difficult to understand why you need either $M$ or $N$. You can build a machine $M$ that searches the space of strings for proofs of $\varphi$ in $\mathsf{ZFC}$ directly. Why do you need a machine $M$ to search for proofs that 'If $M$ halts on the empty input then $\varphi$ is provable in $\mathsf{ZFC}$'? A machine that searches for proofs of $\varphi$ will halt on the empty input if and only if $\varphi$ is provable in $\mathsf{ZFC}$.

Answer 2

The problem is this part:

That paragraph is a ZFC proof that if N halts, then if M halts, then ϕ is true

The relevant paragraph only talks about proofs of $\phi,$ not $\phi$ itself. So all you can say at that point is:

That paragraph is a ZFC proof that if N halts, then if M halts, then ZFC proves ϕ

which isn't as useful.

---

A good way to find the mistake is to take $\phi=\bot$ (i.e. any contradiction). Then using the 2nd incompleteness theorem it's easy to see that these are equivalent in a weak metatheory:

• $M$ halts
• $N$ halts
• ZFC is inconsistent

In particular we (and ZFC) can prove "if $M$ and $N$ halt then $\mathsf{ZFC}\vdash \phi$". But ZFC cannot prove "if $M$ and $N$ halt then $\phi$", unless it's inconsistent.