# "Proof" that ZFC is inconsistent using Turing machines

I came across the following "proof" for the inconsistency of ZFC and can't find the flaw in it (if there is one...):

Construct a Turing machine A which sequentially runs on all proofs in ZFC and checks if the claim "A does not halt or ZFC is inconsistent" is proved. If such a proof is found, A halts.

Note that A can know its encoding - see Kleene's recursion theorem - and even if it can't this "obstacle" can be overcome. So it seems to me such A is constructible.

Now, if A halts then it is because it has found a proof for "A does not halt or ZFC is inconsistent". Since A halted, it is implied that ZFC is inconsistent. So either A does not halt, or ZFC is inconsistent.

Now (and my guess is that this is the part where this proof "cheats") we have just proved the claim "A does not halt or ZFC is inconsistent", so such a proof exists in ZFC. So A must halt on this proof - and we have seen that this implies that ZFC is inconsistent.

Where is the mistake?

• In the antepenultimate paragraph, did you mean *"So either A does not halt, or ZFC is inconsistent"? Also: how do you justify that "such a proof exists in ZFC"? Commented Sep 24, 2010 at 14:36
• Surely ZFC is consistent, and is rather not complete? Commented Sep 24, 2010 at 19:49
• @Noldorin: Hence the question. Commented Sep 25, 2010 at 3:11
• If you ran into this in a published document, could you give a pointer? It would be a nice exercise for beginning grad students learning logic Commented Sep 25, 2010 at 11:46
• No, I heard this in another forum. Commented Sep 25, 2010 at 14:22

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)}$.

• Thank you very much. My intuition still bothers me about that fact that if ZFC proves that X is provable, it still does not say that X is true - after all, isn't it what the standard interpretation of ZFC should ensure? Commented Sep 25, 2010 at 8:33
• It's a subtle point. It's true that if ZFC proves Pvbl($\Phi$) then, because Pvbl($\Phi$) must hold in every model of ZFC and ZFC has an &omega;-model, $\Phi$ really is provable. However, ZFC doesn't prove the scheme $\mathrm{Pvbl}(\Phi)\to\Phi$ because this scheme fails in some models of ZFC. The Pvbl predicate quantifies over the "natural numbers" in a given model of ZFC, which might not be the actual natural numbers. If Pvbl($\Phi$) holds in a non-$\omega$-model, and the number that witnesses the existential quantifier is nonstandard, then that "coded proof" is not an actual proof. Commented Sep 25, 2010 at 11:40
• Gadi constructed a Turing machine enumerating possible proofs of a statement P that is by construction true but not provable in ZFC. The only flaw I see in his reasoning is (as he originally pointed it) where he assumes that because he just proved that P must be true, then his proof can be formalized in ZFC. You say that Gadi assumed that provability in ZFC implies truth, which seems to me to be the very reason why we constructed ZFC in the first place, assuming it is consistent. To me, it looks like Gadi has assumed that truth implies provability in ZFC.
– user519
Commented Sep 25, 2010 at 13:54
• I said that the problem is that the question assumed that formalized provability implies truth: that is, it assumed that Pvbl($\Phi$) implies $\Phi$, which is not right. The issue is that Pvbl only corresponds to actual provability in the some models, so although it is possible to prove "A does not halt or Pvbl($\Phi)$" in ZFC, it is not apparently possible to prove "A does not halt or $\Phi$" in ZFC. As I read it, the point of the question is to determine exactly where things go wrong if you try to actually formalize the proof in ZFC. That's what I addressed. Commented Sep 25, 2010 at 23:13
• @6005: If it's worth doing, it's worth doing right, \operatorname has the correct spacing whereas \mathrm{...} does not create the appropriate spacing. Commented Oct 24, 2017 at 15:50

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.

• You are correct, of course, but naively it seems that everything in my "proof" can be formalized inside ZFC. I can't put my finger on the "hard part" that cannot be formalized. Commented Sep 24, 2010 at 14:55
• I don't have an answer to this question but you definitely showed that this proof can't be formalized inside ZFC. We can actually simplify your problem a bit. Take a Turing machine A that enumerates proofs in ZFC and halts iff it finds a proof of "A doesn't halt". Obviously, A cannot halt if ZFC is consistent and therefore there can't be a proof in ZFC of "A doesn't halt" although it is true. That's actually a sketch proof of Gödel's first incompleteness theorem.
– user519
Commented Sep 24, 2010 at 15:25
• Note the difference - in "my" problem I give a proof for the claim "A does not halt or ZFC is inconsistent" - the only problem is that my proof is not phrases in formal terms and so maybe can't be formalized in ZFC. However, this is a simple proof, and usually such proofs are assumed to be possible to phrase in ZFC without question. Commented Sep 24, 2010 at 15:32
• @GadiA ZFC can't prove many things about itself. It can't even prove many things about Turing machines that talk about ZFC. Commented Jul 12, 2017 at 16:16

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)$.

Here's a simplified form of your original argument:

Construct a Turing machine A which sequentially runs on all proofs in ZFC and checks if the claim "A does not halt" is proved. If such a proof is found, A halts.

Note that A can know its encoding - see Kleene's recursion theorem - and even if it can't this "obstacle" can be overcome. So it seems to me such A is constructible.

Now, if A halts then it is because it has found a proof for "A does not halt". This is impossible, since A halted.

Now we have just proved the claim "A does not halt", so such a proof exists in ZFC. So A must halt on this proof - a contradiction.

(Hopefully this version makes the error more clear. The proof that "A does not halt" assumes the consistency of ZFC, and is therefore a proof in ZFC + Con(ZFC), not ZFC. In fact, the above argument is essentially a proof that Con(ZFC) is not provable in ZFC.)

• Assuming you're working in ZFC (not assuming Con(ZFC)), it's not actually contradictory for A to find a "coded proof" that A halts. If A halts, all we know is there is a (maybe nonstandard) number that codes a proof of "A does not halt". This does not actually contradict A halting (which just means some $\Sigma^0_1$ formula is satisfied). I do think that you have shown that any model in which A halts has an inconsistent provability predicate (meaning Pvbl($\theta$) holds for all $\theta$). But Pvbl($\theta \land \lnot \theta$) is not a contradiction, and doesn't imply anything about $\theta$. Commented Sep 26, 2010 at 11:53
• Could you please explain a bit further? I will use $P$ for "A halts" and $\square$ for "it is provable". We have $ZFC\vdash P \leftrightarrow \square(\neg P)$. Now if $ZFC\vdash P$ then $ZFC\vdash \square P$ and $ZFC\vdash \square(\neg P)$. This one is not a direct contradiction I suppose (comment above). If $ZFC\vdash \neg P$ then $ZFC \vdash \square (\neg P)$, which implies $ZFC\vdash P$. This is a contradiction, so if ZFC is consistent then $ZFC \not\vdash\neg P$. Is this correct reasoning?
– sas
Commented Nov 11, 2023 at 2:17

You might find Scott Aaronson's lecture on this useful. Search for the phrase "Talk to the axioms!"

In summary, suppose ZFC is consistent. I'll work with Alex's simplification, where $A$ searches for a ZFC proof of "A does not halt." Then there is a model $M$ of ZFC+"$A$ halts". In $M$, there is a set $S$ which satisfies the whatever sentence of ZFC you have cooked up to encode "a halting sequence of states for $A$". There is a set $P$ which satisfies the first order sentence you have cooked up to encode "a ZFC proof that $A$ does not halt."

From the perspective of the model $M$, there is no contradiction. The model sees that $P$ encodes a ZFC proof that $A$ doesn't halt, the model sees that $A$ does halt, so the model believes that ZFC is inconsistent. Since Con(ZFC) is not an axiom of ZFC, the model sees nothing wrong with this.

From an outside perspective, $S$ does not actually look like a sequence of states for the Turing machine $A$, and $P$ does not look like a proof. They are just objects of the model which the model thinks have those features, because it has some strange interpretation of set theory. Even if you could construct $M$ (and I think there are obstacles to $M$ being computable in any reasonable way), you could not convert $P$ into an actual ZFC proof that $A$ does not halt, nor could you convert $S$ into a halting sequence for $A$. Any attempt to convert them into an actual proof or actual halting sequence will run into the same difficulty Scott describes in trying to extract a proof of NOT(Con(PA)) from a model of PA+NOT(Con(PA))