# “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"? – Arturo Magidin Sep 24 '10 at 14:36
Yes, thank you. – Gadi A Sep 24 '10 at 14:37

1
Surely ZFC is consistent, and is rather not complete? – Noldorin Sep 24 '10 at 19:49
@Noldorin: Hence the question. – ShreevatsaR Sep 25 '10 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 – Carl Mummert Sep 25 '10 at 11:46
show 2 more comments

## 7 Answers

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 ~Con(ZFC) but this is not material. Let $\mathrm{Pvbl}(b)$ be the standard 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 \mathrm{Pvbl}((A\uparrow) \lor \Phi)$$

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

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

Now: what we have obtained is: "A does not halt or 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.

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

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

-

1
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? – Gadi A Sep 25 '10 at 8:33

3
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. – Carl Mummert Sep 25 '10 at 11:40

1
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 Sep 25 '10 at 13:54

1
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. – Carl Mummert Sep 25 '10 at 23:13

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.

-

2
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. – Gadi A Sep 24 '10 at 14:55

1
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 Sep 24 '10 at 15:25

1
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. – Gadi A Sep 24 '10 at 15:32

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

-

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

-

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$. – Carl Mummert Sep 26 '10 at 11:53

The problem is that if the machine manages to prove it - it halts. and therefore ZFC inconsistent.

-

3
I don't see how this addresses the question. – Carl Mummert Sep 24 '10 at 18:49

Why not replace "ZFC is inconsistent" by false? Namely you can prove anything this way.

But this argument is not a proof because it has an extra assumption that A halts iff there is a proof that A does not halt. You mean A is constructible.
What does consistent mean? Someone defines consistent as ~provable(0 = 1), but this only implies the axioms are not against our intuition. But we could have 0 = 1 as an axiom.

-

The theory {A does not halt} proves A does not halt, no matter A halts or not. So it's all about whether we accept the axioms of the theory. If we accept them as true, the proof implies truth. Another question is what if we choose the theory as the empty set of axioms, then certainly proof implies truth. – Zirui Wang Dec 24 '10 at 5:16
What's Kleene's recursion theorem and how is it applied to the construction of A? How is it proved? – Zirui Wang Dec 24 '10 at 6:30
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 69, "mathjax_display_tex": 3, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": false, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9509453773498535, "perplexity_flag": "middle"}