“Proof” that ZFC is inconsistent using Turing machines

Question

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?

Answer 1

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

Answer 2

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.

Answer 3

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

Answer 4

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

Answer 5

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

Answer 6

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

Answer 7

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.