Comment by jbapple

11 years ago

> In what sense is the BB sequence even well-defined if we can prove that it can't be determined?

I think it may help you to understand how the BB sequence can be well-defined if you change your definition of "we can prove".

A proof is a sequence of logical deductions in an axiomatic system, so what "we can prove" depends a lot on which axiom system you're using. For some types of questions, it helps to make that explicit.

For instance, in weak axiom systems, we can't prove that every hydra game terminates. [0] In very strong axiom systems, ones so strong we call them inconsistent, we can prove everything! People argue over intermediate systems sometimes by pointing out things they can prove that are counter-intuitive. [1][2]

For any terminating Turing machine, there is a (possibly very long) proof in a very weak axiom system of that fact: the full trace of the execution. (For non-terminating machines, this is not true.) So, if ZFC, a rather strong axiom system, cannot prove a machine halts, it does not halt.

For another example of this kind of thing, see Terry Tao's discussion of the consequences of the independence of Goldbach's conjecture from ZFC on MathOverflow. [3]

[0] https://en.wikipedia.org/wiki/Goodstein%27s_theorem [1] https://en.wikipedia.org/wiki/Freiling%27s_axiom_of_symmetry [2] https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox [3] http://mathoverflow.net/a/27764

7 comments

jbapple

Reply
fbastiat  11 years ago

But if the machine that stops when it has proven ZFC is inconsistent does not halt, then surely it means there is no proof of the inconsistency of ZFC? Hence ZFC is consistent? Which is contradicted by Godel.

I would think instead ZFC can't prove or disprove that this machine halts, which just means it's undecidable wether it halts or not.

This also implies that for sufficiently large n, we won't be able to prove that BB(n) = N, or even BB(n) < N for any N using the ZFC axioms. Of course, although they can't compute or bound its value, they can still easily prove that BB(n) is finite.

  • jbapple  11 years ago

    > But if the machine that stops when it has proven ZFC is inconsistent does not halt, then surely it means there is no proof of the inconsistency of ZFC?

    I'm not sure what this question means. Are you referencing an earlier discussion of a machine that demonstrated a proof of "0=1" using the axioms of ZFC? If so, what is your concern?

    When thinking about undecidability/independence from a computational perspective, it's helpful to be cautious about the phrase "does not halt". How would you know a machine "does not halt"? You might run it for a long time and observe that it has not halted yet, but that's not the same.

    Instead, you can talk about "a proof in $AXIOM_SYSTEM that this machine does not halt".

    So, using that terminology, consider a machine that enumerates all valid proofs of ZFC and checks if their conclusion is "0 = 1". Certainly, if ZFC is inconsistent, this machine will find a proof and halt. However, if there is no such proof, then ZFC is consistent, the machine will not halt, but there will be no proof in ZFC that the machine will not halt.

    This ability to enumerate the proofs is related to semidecidability/recursive-enumerability.

    When you say "for sufficiently large n, we won't be able to prove that BB(n) = N", I agree. There is some n that is so large that there is a Turing machine of size n that does loop, but the fact that it loops will not be provable in ZFC.

    • fbastiat  11 years ago

      Well you said "if ZFC, a rather strong axiom system, cannot prove a machine halts, it does not halt.". This particular statement is what I was replying to. I agree that a non-halting Turing machine is not a very well defined concept in the general sense (hence my reply), but I would think the onus is on the one who used it first to define what they meant by it :-)

      3 replies →