# How can Busy beaver($10 \uparrow \uparrow 10$) have no provable upper bound?

This wikipedia article claims that the number of steps for a $10 \uparrow \uparrow 10$ state (halting) Turing Machine to halt has no provable upper bound:

"... in the context of ordinary mathematics, neither the value nor any upper-bound of $\Sigma(10\uparrow\uparrow10)$ can be proven..."

How is this possible? In principle, wouldn't listing the computations of all the (finitely many) halting Turing machines of that size, and individual proofs of non-halting for all the non-halting ones (again, finitely many) create a proof?

I'm assuming that the "ordinary mathematics" mentioned has no formal meaning.

-
Yes, that would work. But why do you think it's possible to prove the non-halting of all those machines? – Chris Eagle Oct 21 '12 at 17:00
@ChrisEagle But then that would imply that there is some specific Turing machine which does not halt, but its non-halting is unprovable. Are you claiming that such a thing exists? If so, is there an easy way to see the existence? – ronno Oct 21 '12 at 17:08
If none such existed, you could solve the halting problem: given a Turing machine $M$, enumerate all possible proofs (of all statements) until you come to either a proof that $M$ halts or that $M$ does not halt. – Chris Eagle Oct 21 '12 at 17:14
@ChrisEagle But... but... if it is not provable, then the negation of the statement would also be true in some model, right? What does that mean? Is whether or not a given Turing machine halts not determined by the laws of arithmetic? – ronno Oct 21 '12 at 17:19
It means there's a model in which it halts after some nonstandard number of steps. – Chris Eagle Oct 21 '12 at 17:22

The Wikipedia article explains exactly what it means. Here is an elaboration.

Define the complexity of a number $n$ to be the smallest number of states for a Turing machine that returns $n$ when run with $0$ as an input. Certainly every number has a complexity. Now let $T$ be any effective formal theory whose language includes statements of the form "$n$ has complexity greater than $k$" for each $n$ and $k$. Some of these sentences may be provable in the theory, and some may not. Say that the theory is complexity sound if each statement "$n$ has complexity greater than $k$" that is provable in the theory is correct. Both PA and ZFC are effective, complexity sound theories.

Theorem. For any effective, complexity sound theory $T$, there is some $k$ such that the theory does not prove that any number $n$ has complexity greater than to $k$.

Proof by contradiction. Assume $T$ is complexity sound and proves statements of the form "$n$ has complexity greater than $k$" for arbitrarily large $k$. Consider a program $P$ that does the following when run with $0$ as an input. First, $P$ computes its own source code (like a Quine; formally, the proof uses Kleene's recursion theorem). Then $P$ counts the number of states $s$ in this source code. Next $P$ enumerates all statements of the form "$n$ has complexity greater than $k$" that are provable from $T$, until it finds one with $k > s$. It will find one by assumption. Finally, $P$ returns $n$. Because $T$ is an effective theory, $P$ can do all this computably. But then the number $n$ returned is by $P$, which has $s$ states, but $T$ proves "$n$ has complexity greater than $k$" for some $k > s$, so $T$ is not complexity sound, which is a contradiction. That completes the proof.

Thus there is a bound on the largest $k$ such that $T$ proves "$n$ has complexity greater than $k$" for any $n$. In fact, we can actually write down $P$ explicitly, and thus $k$ is no more than the number of states of the version of $P$ we write down. For any reasonable theory, like PA or ZFC, this $k$ will be huge but not anywhere near $10\uparrow\uparrow 10$.

If a sufficiently strong theory cannot prove any $n$ has complexity larger than $k$, then it also cannot prove any statement of the form "$m$ is an upper bound on $\Sigma(k)$", because if it could prove that it would also prove "$m+1$ has complexity greater than $k$". So in particular neither PA nor ZFC can prove an upper bound on $\Sigma(k)$ when $k$ is sufficiently large.

Just as the Wikipedia article says, the theorem above is just a recasting of Chaitin's incompleteness theorem in which the length of the program is replaced with the number of states.

-
This makes sense, thanks. But I'm still a bit mystified about why $10\uparrow\uparrow 10$ was chosen as the stated bound -- you seem to agree that it is much larger than you would actually need. Is it just a case of being extremely conservative? (Is this worth asking in a separate question?) – Chris Pressey Dec 9 '12 at 13:14
Yes, I think they are just being conservative. It would be sufficiently irritating that nobody is likely to actually write down the Turing machine to see how large it is, even though the actual process for writing down that Turing machine does not require any creativity, just patience. – Carl Mummert Dec 9 '12 at 18:35

While what has been discussed in the comments is relevant (there exist individual Turing machines which have undecidable Halting problems), I doubt this is what the statement in the Wikipedia article is referring to, mainly because there's absolutely no need to mention a bound as high as $10 \uparrow \uparrow 10$ to find a Busy Beaver with an undecidable Halting problem.

Any universal Turing machine has an undecidable Halting problem, for if it didn't, you would be able to solve the Halting problem for any machine it simulates. There are universal Turing machines with only a handful of states (see e.g. this paper of Neary and Woods.) The restriction that a Busy Beaver starts with a blank tape isn't of consequence, because the machine can just write a machine description onto the tape, and then proceed to simulate it.

I suspect the phrase "ordinary mathematics" is an oblique reference to first-order Peano Arithmetic or similar, and the statement is referring to some proof that any proof of a bound for TM's with $10 \uparrow \uparrow 10$ states must use transfinite methods, even if the TM is total (like the Hydra rewriting game, or something in a similar vein.) But this is just a guess.

("Ordinary mathematics" normally suggests ZFC to me, but a proof that this result is independent of ZFC would be somewhat too astonishing to me, for me to take that interpretation here.)

-
As I have attempted to explain in my answer, ZFC has the same problem; it is an incompleteness phenomenon endemic to effective sound theories. – Carl Mummert Dec 8 '12 at 0:21

Here's a simpler argument that doesn't depend on explicit diagonalization. On the other hand, in contrast to Carl Mummert's answer it only works for first-order theories or another axiomatic framework where something like Gödel's completeness theorem holds. But that's enough to cover the usual suspects for "ordinary mathematics", i.e. PA and ZFC.

First, of course, fix a particular first-order theory $T$ that you want to prove the claim about. We assume it is effectively axiomatized and doesn't prove arithmetic falsehoods (in particular it is consistent).

Let $M$ be a Turing machine that loops through the natural numbers until it finds one that is the Gödel number of a proof of $T\vdash 0\ne0$, and then stops. Since "is the Gödel number of a proof of $T\vdash0\ne0$" is (primitive) recursive, there's certainly a Turing machine that does this, and it will have much fewer than $10\mathop{\uparrow\uparrow}10$ states. (The huge bound of $10\mathop{\uparrow\uparrow}10$ must be in order to cater for really wasteful ways to implement p.r. functions as Turing machines).

Now $M$ cannot ever halt, since we're assuming that our theory proves no falsehoods.

On the other hand, if $T$ proves that $M$ doesn't halt, then effectively it will have proved that it is itself consistent, and that is impossible according to the second Gödel-Rosser incompleteness theorem.

Since $M$ doesn't halt in any standard number of steps, and it can't be proved that it never halts, there must be a model of $T$ in which $M$ halts in a nonstandard number of steps. Therefore no standard upper bound for $\Sigma(|M|)$ is true in that model, and therefore $T$ can prove no such bound.

-