[Scarblac]

And also, if BB were computable, then it could be used to solve the halting problem: run the Turing machine of size n for BB(n) steps, and if it hasn't halted yet, it never will. So the BB function is clearly not computable.

But to me as a layman that seems true regardless of formal axioms chosen, but I guess I need to read that linked thesis.

[ajkjk]

That is the standard argument for why BB is uncomputable for general n, but it's not the same as why BB(n) would be independent of ZFC for fixed n.