"Proof" that ZFC is inconsistent using Turing machines

Here's my take on it. Use $(A \uparrow)$ to mean $A$ does not halt, and $(A \downarrow)$ to mean $A$ does halt. Let $\Phi$ be any sentence; the question uses $\lnot\operatorname{Con}\mathrm{(ZFC)}$ but this is not material. Let $\operatorname{Pvbl}(b)$ be the standard $\mathrm{ZFC}$-formalized provability predicate, which says that there is a coded proof of the formula with number $b$.

The question is right that, by the recursion theorem, we can create a specific machine $A$ such that $$ (A \downarrow) \Leftrightarrow \operatorname{Pvbl}((A\uparrow) \lor \Phi) $$

Moreover, because of the specific form of the formula $(A \downarrow)$, $\mathrm{ZFC}$ is able to prove $$ (A \downarrow) \to \operatorname{Pvbl}(A\downarrow) $$

Working in ZFC, assume $(A \downarrow)$. Then we know $\operatorname{Pvbl}(A \downarrow)$ and $\operatorname{Pvbl}((A \uparrow) \lor \Phi)$. ZFC is able to prove enough about the $\operatorname{Pvbl}$ predicate to ensure that $$\operatorname{Pvbl}(\psi) \land \operatorname{Pvbl}(\lnot \psi \lor \theta) \rightarrow \operatorname{Pvbl}(\theta) $$ for all $\psi$ and $\theta$. So we can obtain $\operatorname{Pvbl}(\Phi)$.

Now: what we have obtained is: "A does not halt or $\operatorname{Pvbl}(\Phi)$". In the fourth paragraph of the question, it instead claims we can obtain "A does not halt or $\Phi$". That is a stronger statement, and this is the first error I see in the proof. In the fourth paragraph, it is silently assumed that provability implies truth, but this is not correct for formalized provability.

$\mathrm{ZFC}$ does not prove $\operatorname{Pvbl}(\Phi) \to \Phi$ in general. In particular, $\mathrm{ZFC}$ does not prove $\operatorname{Pvbl}(0=1) \to (0=1)$ because there are models of $\mathrm{ZFC}$ in which both $\operatorname{Pvbl}(0=1)$ and $0 \not = 1$ are satisfied.

Addendum: Löb's theorem addresses this exact question. Applied to $\mathrm{ZFC}$, it states that if $\mathrm{ZFC}$ proves $\operatorname{Pvbl}(\Phi) \to \Phi$ then ZFC already proves $\Phi$. So, in particular, $\mathrm{ZFC}$ does not prove that $\operatorname{Pvbl}\mathrm{(\lnot Con(ZFC))}$ implies $\lnot \operatorname{Con}\mathrm{(ZFC)}$.


You've just proved that "either A does not halt or ZFC is inconsistent" must be true, not that this statement is provable in ZFC. There exist unprovable true statements in ZFC (if it is consistent). See Gödel's first incompleteness theorem.


For such questions, it is hard to get an intuitive understanding. I think the best way to intuitively understand it is by formalizing it using model-theory. So lets look at it.

Say you define your A as a set in ZFC, using an $\cal{L}_1$-Formula, and denote the property of "halting" as $\cal{H}$, which can also be expressed in ZFC. So by your assumption, you have $ZFC\models{\cal H}(A)\leftrightarrow(ZFC\models\bot \vee ZFC\models\lnot{\cal H}(A))$.

With a little more theory, you can imply therefore $ZFC+{\cal H}(A)\models (ZFC\models\bot\vee ZFC\models\lnot{\cal H}(A))$, and therefore, $ZFC+{\cal H}(A)\models (ZFC\models\bot)$. That is your one direction.

The other direction goes with $ZFC+\lnot{\cal H}(A)\models \lnot (ZFC\models\bot \vee ZFC\models\lnot{\cal H}(A))$ (which follows from the first assumption), i.e. $ZFC+\lnot{\cal H}(A)\models (ZFC\not\models\bot) \wedge (ZFC\not\models\lnot{\cal H}(A))$. That is, in every model of ZFC, in which $\lnot{\cal H}(A)$ holds, every "sub-model" which can be created doint meta-theory inside that one, does neither model $\bot$ nor model $\lnot{\cal H}(A)$.