Comment by swatow

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.