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.