Fast-growing hierarchy and Turing machines Is it possible to get an estimate of the size of a Turing machine computing $f_\alpha(n)$, for a given $\alpha$ (I am especialy interested in moderately large $\alpha$ like the ordinal of Fefferman-Schütte, or the small Veblen ordinal)? The idea is to get an idea of the size of the BusyBeaver function $BB(n)$ for moderate values of $n$, as the litterature usually only mention the exact known values (for $n\le 6$) and the fact that such values will probably never be known for $n=10$, say.
 A: Consider Gödel's speed-up theorem which discusses sentences like "this sentence is unprovable in theory T with less than $\phi$ symbols" where $\phi$ is some computable formula like TREE(3), and T is some consistent, effective theory like PA or ZFC with large cardinals (assuming those are consistent).  Call the above sentence S.
Per the speed-up theorem, S is both true and provable (see the wiki article).  The provability means that for reasonable theories, there is a relatively small $n$ such that an $n$-state Turing machine will eventually (by unbounded search) find the proof and halt, but that the running time will be (much) longer than $\phi$.  Of course BB(n) has to be even bigger than that.  With a suitable encoding, n=15 might be enough.  So BB(n) quickly dominates any computable formula that can be written down.
"BB(15) is uncomputable" could be interpreted something like: there is a 15-state TM that halts if and only if your favorite strong arithmetic theory T is inconsistent.  So if you believe that T really is consistent, that means you'll never be able to know what BB(15) is.
