zlacker

>>jeremy+(OP)
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.)

>>codefl+Ue
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.