2
$\begingroup$

Lately I learned that Adam Yedidia and Scott Aaronson showed a Turing Machine that would only stop if ZFC is consistent (Scott Aaronson blog), therefore proving that for this Turing Machine it is unprovable under ZFC whether it would stop.

I don't understand how is that possible, that we would have a concrete example of a program for which we can't say if it will stop in finite time. We surely can run this program. If it would stop after N steps, we would know it does stop and it wouldn't be undecidable. So it can't stop after N steps, for any natural N. But then it wouldn't ever stop and again, it wouldn't be undecidable.

Can you point me, where I'm wrong?

$\endgroup$
  • $\begingroup$ I think you must be misunderstanding the blog post; I cannot find where it speaks about "a Turing Machine that would only stop if ZFC is consistent" -- if that means a machine that will stop if and only if ZFC is consistent (and ZFC can prove this fact), then ZFC would, if consistent, be able to prove its own consistency simply by exhibiting a terminating run of that machine, which contradicts a well-known result of Gödel and Rosser. $\endgroup$ – Henning Makholm Feb 6 '17 at 23:11
  • 1
    $\begingroup$ The blog is quite clear. What is announced is a TM that can be proved to halt in an extension of ZFC, but can't be proved to halt in ZFC is ZFC is consistent. Your argument that we can run the TM and see what happens is invalid: you can't run a test to show that a computation does not terminate. $\endgroup$ – Rob Arthan Feb 6 '17 at 23:30
  • 1
    $\begingroup$ As explained in the article, suppose a program that enumerates all possible consequences of the ZFC axioms and halts if it finds a contradiction. You can definitely run this program. But if you're reasoning in ZFC, you cannot pose the question "Will it stop after $N$ steps?" and get an answer for arbitrary $N$. You can fix $N$ to a value and probably get an answer "No", and then try with a bigger $N$ and get again a "No" and so on, but this doesn't guarantee that you'll get a "No" for any $N$. $\endgroup$ – frabala Feb 7 '17 at 0:29
2
$\begingroup$

You are missing a key assumption - that ZFC is an appropriately nice theory. In particular, the statement

therefore proving that for this Turing Machine it is unprovable under ZFC whether it would stop

is incorrect: all we can conclude is that if ZFC is consistent then ZFC can't prove that it doesn't halt, and if ZFC is arithmetically sound (see below) then ZFC can't prove that it does halt. But the point is, we need assumptions on ZFC in order to conclude anything about the behavior of the machine.


In more detail:

Essentially, what the machine in question does is the following: search through all possible proofs of "$0=1$" from the ZFC axioms, and halt when, and only when, it finds one. Thus:

  • If ZFC is consistent, the machine never halts (it never finds a proof of $0=1$, since there isn't one).

  • If ZFC is consistent, then - by Goedel's Second Incompleteness Theorem - ZFC can't prove that ZFC is consistent, so - while for each $N$, ZFC can prove "The machine doesn't halt in $N$ steps" - it can't prove "The machine never halts."

  • So this proves: "If ZFC is consistent, then - while the machine never halts - ZFC can't prove that the machine never halts." If, in addition, we assume ZFC is arithmetically sound (that is, doesn't prove any false statements about arithmetic - this is actually vastly more than we need, but oh well), then ZFC can't prove "The machine does halt", since that would (under these assumptions) be a false statement. (Note that there are, in fact, consistent theories which prove themselves to be inconsistent!)

  • So to recap, we can prove (in ZFC, or indeed much less):

    • If ZFC is consistent, then ZFC doesn't prove "The machine doesn't halt," even though the machine truly doesn'thalt.

    • If ZFC is arithmetically sound (a stronger condition than mere consistency), then ZFC doesn't decide the question "Does the machine halt?" either way.

Now the key point is that in each case we have an important assumption about ZFC: consistency, or arithmetic soundness. In general, the argument

If it would stop after N steps, we would know it does stop and it wouldn't be undecidable. So it can't stop after N steps, for any natural N.

isn't right: ZFC doesn't know that the question is undecidable, it just knows that it's undecidable if ZFC itself has a nice property. Think about the similar issue of consistency: if ZFC were inconsistent, then we would know that, so the inconsistency of ZFC would be provable in ZFC. But this isn't a contradiction, since we never proved "ZFC doesn't decide its own consistency," we just proved "If ZFC is arithmetically sound then ZFC doesn't prove its own consistency."

$\endgroup$
  • $\begingroup$ Note that arithmetic soundness implies consistency: any inconsistent theory proves "$0=1$", which is false, hence any inconsistent theory is not arithmetically sound. $\endgroup$ – Noah Schweber Feb 7 '17 at 1:13
  • $\begingroup$ while for each N, ZFC can prove "The machine doesn't halt in N steps" - it can't prove "The machine never halts." How are these statements different? Isn't "For every N, the machine doesn't halt in N steps" the definition of "The machine never halts"? $\endgroup$ – Jan Rzymkowski Feb 7 '17 at 11:03
  • $\begingroup$ @JanRzymkowski Yes, but the statements "$\forall n, ZFC\vdash \varphi(n)$" and "$ZFC\vdash\forall n\varphi(n)$" are not. Just because ZFC can prove each instance of $\varphi$, doesn't mean ZFC can prove that $\varphi$ always holds. This is weird, but true. The standard example of this is consistency: if ZFC is consistent, then for each $n$ ZFC proves "There is no proof of contradiction in ZFC of length $\le n$"; but by Goedel's Second Incompleteness Theorem, ZFC (being consistent) can't prove "For all $n$, there is no proof of contradiction in ZFC of length $\le n$" (cont'd) $\endgroup$ – Noah Schweber Feb 7 '17 at 13:21
  • $\begingroup$ since that's exactly the statement "ZFC is consistent"! This can be very counterintuitive at first glance, but it is nonetheless true. $\endgroup$ – Noah Schweber Feb 7 '17 at 13:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.