Comment by fbastiat

After looking more closely at your linked post by Terence Tao, are you by chance basing your statements such as "it does not halt" in what he calls the informal platonic reasoning system (which presumably assumes ZFC as well as its consistency)?

If so, I think I understand what you mean and I agree with you.

My thoughts were a bit confused on these topics so my posts probably contain some reasoning errors, but in the end I think what matters is we agree on the answer to OP's question, i.e.

For any given theory T at least as strong as ZFC (and maybe even some weaker ones) then

- BB as function is well defined in T - However there is some number n_T after which T can't prove any upper bound for BB(n) for any n > n_T

I think this is a very interesting result because the fact that any axiomatic system will be powerless to describe this function's growth after only a small number of steps expresses pretty well how mind numbingly fast it grows.