First, some context. Ever since I was a high schooler, I have been fascinated with large numbers. As I have grown in mathematical maturity, I have become both disappointed and fascinated to see that the process of naming larger and larger numbers requires a sort of philosophical tradeoff.


For example, an ultrafinitist might reject $10^{10^{100}}$ as being a valid representation of a number. A finitist might reject numbers defined using ordinal collapsing functions with large cardinals. A person who believes only in the constructible universe might reject the same ordinal collapsing functions if cardinals incompatible with $V=L$ are used. In general, the more you are willing to accept philosophically, the "larger" a number you can name concisely.


The interesting thing about these tradeoffs is that some of these philosophical stances have concrete impacts on the "real" world. For example, there is a number $n$ for which new axioms in addition to those of ZFC would be needed to prove the value of $BB(n)$. So in a way, this "real world" value changes depending on our philosophical stance.


My question then is: what sorts of axioms might we accept to strengthen as much as possible the values of $BB(n)$ which we can prove? And more generally, is there a way we can evaluate whether certain statements independent of ZFC are "true" based on their implications for the "real world" value of $BB(n)$ (if there is even a "true" value for this number).


EDIT: useful reading for those not familiar with the phenomenon of independence of $BB(n)$ from ZFC:


* Adam Yedidia, Scott Aaronson, *A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory*, Complex Systems **25**(4) (2016), [journal](https://www.complex-systems.com/abstracts/v25_i04_a04/), arXiv:[1605.04343](https://arxiv.org/abs/1605.04343)


EDIT: As requested, an example of a "real world" consequence of a set theoretical axiom would be how Con(ZFC) would prove the Turing machine in the above paper doesn’t halt, whereas the negation of Con(ZFC) proves it halts in finite time.



What sorts of extra axioms might we add to ZFC to compute higher Busy Beaver numbers?
There's a certain confusion underlying your question, which Andreas Blass's answer is trying to point out. Let me see if I can explain it in different words.


You say, “the negation of Con(ZFC) proves it halts in finite time” and you are trying to use this fact to argue about which axioms beyond ZFC to accept. The best sense I can make out of your comment is that ZFC + $\neg$Con(ZFC) has no $\omega$-model (i.e., no model in which the natural numbers are standard) and you treat this fact as an argument against accepting $\neg$Con(ZFC) as an axiom. So your question sounds like, do any of the standard strengthenings of ZFC have the property that they have no $\omega$-model? As Andreas Blass explained, the answer is no. So under this interpretation of your question, the answer is that none of the standard large cardinal axioms can be rejected on such grounds.


But I suspect that this is not your real question. I am guessing that when you refer to the “real world” you mean the standard integers, not the integers in some model of ZFC. Let me see if I can state what I think is your intended question.


Suppose for the sake of argument that BB(3) = 17 but that this fact is unprovable in ZFC. (Of course, this is absurd; but to write down realistic numbers in place of 3 and 17 would be, shall we say, inconvenient, and it does not matter for what I am going to say what the actual numbers are.) What is it about this statement that is unprovable? Well, BB(3) $\ge$ 17 is actually provable in ZFC, and in fact in a much weaker system, because you can just write down a specific size 3 Turing machine and verify that it halts in 17 steps. The troublesome part is proving that all those other size 3 Turing machines that take at least 18 steps *never halt at all*. For some of these machines, ZFC is unable to prove that they do not halt.


So what about stronger axioms? It certainly can be the case that adding a large cardinal axiom to ZFC will allow us to prove that some of those non-halting size 3 Turing machines do not halt. For example, adding large cardinal axioms yields new consistency statements, and consistency statements can be cast as statements about certain Turing machines (those that search for contradictions) not halting. So if this is what you mean, then the answer is yes, in principle, we can partially evaluate large cardinal axioms on the basis of their “real-world” consequences. However, I do not think that the BB function is particularly helpful in this regard. The trouble is that we do not know of any “reasonable” axiom that would let us prove that BB(3) = 17. And even if we did, how would that help us evaluate the axiom? Presumably, we would try to accumulate empirical evidence by enumerating size 3 Turing machines that run for at least 18 steps, and watching to see if they ever halt. The longer they run, the more confident we become that they will indeed never halt, so the happier we are that the predictions of our new axiom are being validated. The trouble is that 18 is so ridiculously large that we will never reach it, let alone sit around waiting even longer to see if the machine halts. So we have no practical way of accumulating the relevant empirical evidence.


