Comment by Kranar

The issue is that it's impossible to formally and uniquely define the actual natural numbers, and hence it's impossible to require as part of the formal definition of some mathematical object like BB(n) to equal an actual natural number.

Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up with a formal definition of natural numbers that includes the actual natural numbers but will also include other number systems that contain mathematical objects that are infinitely big and hence are not actual natural numbers. Hence our formal definition of natural numbers will not uniquely define a single set of numbers {0, 1, 2, 3, ...}, there will be other sets of numbers such as {0, 1, 2, 3, ..., Q - 1, Q, Q + 1, ...} for some infinitely large object Q that satisfy the formal definition of natural numbers. Between you and me, we both know Q isn't an actual natural number, but what we don't know is what formal rule we need to add to our formal definition of natural numbers in order to get rid of Q. In fact, it's worse than that; we know that even if we add a rule that gets rid of Q, there will always be some other number system {0, 1, 2, 3, ..., Q* - 1, Q*, Q* + 1, ...} to take its place. No formal definition can ever uniquely define the natural numbers (unless that formal system is inconsistent).

It's also true that a model where BB(748) = Q is not the actual BB, it's some other function. The problem is that this model satisfies all of the rules of ZFC and all of the properties that ZFC says natural numbers must satisfy and hence it satisfies the formal definition of BB even though it isn't the actual BB. Remember it is impossible for the formal definition of BB to include the property that BB(n) = an actual natural number, because there is no formal definition that uniquely singles out what the actual natural numbers are. Since there exists one such model that satisfies all of the rules about BB but isn't actually the real BB then we can't use ZFC to formally prove what the value of BB(748) actually is.

What we can do is add new rules to ZFC get rid of this model, but that will only push the issue down to BB(749) or BB(750) or maybe if pick a really powerful rule we push the issue down to BB(800)... but the point stands that adding new rules only pushes the problem further down the road, it never eliminates the problem entirely.