Comment by codeflo
11 years ago
Here's a philosophical question that's been bothering me for a while. For large enough n, we can construct an n-state Turing machine that attempts to prove a contradiction in our current most powerful axiomatic system (let's say ZFC). We must assume that this machine loops forever, but Gödel's incompleteness theorem implies that we can't prove that.
What does this construction imply about BB(n)? In what sense is the BB sequence even well-defined if we can prove that it can't be determined?
(Edited for clarity.)
> 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
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.
> 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.
4 replies →
I think this[0] is a good formalization of what I'm trying to say.
[0] http://math.stackexchange.com/a/614017/215039
Everything rests on the consistency of ZFC, which we can't prove. In some sense even results like 2+2=4 are provisional, because if ZFC were inconsistent (and we can't prove that it isn't) then it might also be true that 2+2=3 and 2+2=5.
(Well, strictly we can prove that 2+2=4 in Presburger arithmetic which is provably complete and consistent. But any result that we prove by contradiction and that uses the higher axioms (e.g. Hilbert's basis theorem) is implicitly assuming the (unprovable) consistency of ZFC).
Mostly this doesn't bother working mathematicians - ZFC seems reasonable, corresponds to the models that we do have, so we just take it on trust. People who care explicitly about these issues might work in a "higher" axiom system to prove "metamathematical" facts (e.g. ZFC + weakly inaccessible large cardinal, under which we can prove that ZFC is consistent and also that this particular Turing machine doesn't halt).
((Of course the whole point of Gödel's incompleteness theorems is that there's no sharp line between mathematical and metamathematical; any unproven proposition might turn out to be an unprovable landmine. But this doesn't tend to bother people. After all, the proposition might just as easily turn out to simply be very difficult to prove, and the practical impact would be much the same))
This kind of thing happens in math a lot. Any time you use the axiom of choice to prove something exists, it's non-constructive. It exists, but you can't get your hands on it.
I wrote a comment down below about how one could in principle determine a number which is probably BB(n), but you could never be sure. But I just had the crazy thought that if a human brain is really just an N-state Turing machine for some giant N, then any human would either wait forever or give up before finding the true BB(n) for some n. Time for bed!
>We must assume that this machine loops forever
We must assume this machine would loop forever, it it operated on only the rules of ZFC, because we assume ZFC is consistent. A real machine cannot loop forever, and it would be unreasonable to assume that it does. Real machines are not known to operate based solely on the rules of ZFC. ZFC is only an approximation.
that's a good question. I think the answer is that if we could prove BB(n) = K, then we just have to run this turing machine for K iterations, and either it finds a contradiction, or it doesn't. In the latter case, we have proven that ZFC has no contradiction, and so by Godel's theorem, it has a contradiction.
From this it follows (by proof by contradiction!) that BB(n) is undecidable/uncomputable (getting a bit hazy on these definitions). In any case, we cannot prove that BB(n) = K for any K.
Is it a problem that for all K we cannot prove that BB(n) = K? I don't think so, this is just another incompleteness result.
> For large enough n, we can construct a Turing machine that attempts to prove a contradiction in our current most powerful axiomatic system (let's say ZFC).
What is n in this construction?
I'm sorry, n was supposed to be the number of states of the Turing machine. I've clarified the original post.
The article does mention that "no Turing machine can list the Busy Beaver numbers".
That's clear. My point is that mathematics can't list the Busy Beaver machines.
> In what sense is the BB sequence even well-defined if we can prove that it can't be determined?
Every BB number can be determined. However, each one must require zillions of special cases which require their own reasoning---this is the only way to prevent the BB numbers from being computable.
So, if you consider, for example, the proof of the four-color theorem (which amounts to checking many special cases), as mathematics, then mathematics surely can determine BB(n). It's just extremely hard---as hard as doing all of mathematics (in the sense that if you could easily get BB(n) you could then take a logical proposition you are interested in proving in some axiomatic system and construct a TM to derive the statement using those axioms. Then, count how many states that TM has, and start running it. If it runs for more than BB(# states), there is no proof from your system of your proposition).
3 replies →