Why is there no computable function that grows faster than the sequence of Busy Beaver numbers? I understand that if f


*

*Grows faster than BB

*Is computable

*Can be proven to have the first property


we can use it as an oracle to solve the halting problem. But let's say f is computable, grows faster than BB but cannot be proven to grow faster than BB. That won't let us answer the halting problem.
Is such a function known not to exist?
 A: The argument showing that a computable function growing faster than $BB$ permits computation of the halting problem does not depend on the provability, unless you want to be able to prove that your solution is a solution to the halting problem. Here's the idea: we can take any computable function $f$ we like and use it to "pretend" to solve the halting problem, by declaring that any Turing machine of length $N$ that doesn't halt within $f(N)$ stages must not halt at all. If $f$ doesn't grow faster than $BB$, the resulting "guess" at the halting problem won't be terribly interesting; but if it does, then our guess will be correct. If $f$ grows faster than $BB$ but we can't prove it, then our guess at the answer to the halting problem will be correct even though we can't prove it.
Now, the halting problem is noncomputable irrespective of proof - i.e., getting a solution to the halting problem that is provably a solution to the halting problem isn't the issue, getting a solution to the halting problem at all is. Since a solution to the halting problem (regardless of provability) can't be computable, no computable function can bound $BB$ (regardless of provability).
