What sorts of extra axioms might we add to ZFC to compute higher Busy Beaver numbers?

Question

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, arXiv: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.

Answer 1

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.

Answer 2

$\DeclareMathOperator\BB{BB}$Philosophical issues, like acceptance (or non-acceptance) of large cardinals, won't affect $\BB(n)$, because the busy beaver function is defined arithmetically and so depends only on the natural numbers. Specifically, suppose I believe in some large cardinal, say supercompact. Then within my set-theoretic world, there is the submodel of Gödel's constructible sets, and within that there's an even smaller model containing only sets of rank below the first inaccessible cardinal. In this tiny sub-universe, there are no large cardinals, not even inaccessible ones, let alone measurable or bigger (like supercompact). But $\BB$ is exactly the same as it was in my original, rich universe. I could even cut down further to the minimal transitive model of ZF (or even of weaker theories) without changing $\BB$.

To change $\BB$, you need to move to non-standard models of arithmetic. So there will be infinite natural numbers in that new world. Then of course the domain of $BB$ will change (since it'll include all the integers) but, more importantly, the value $\BB(n)$ could change even for some standard $n$. Such a change could, however, only be of one sort: The new value of $\BB(n)$ is a non-standard integer. (Some Turing machine computation that never halted in the standard world now halts after a non-standard number of steps.)

Answer 3

Knowing the values of the Busy Beaver function is the same as knowing the truth values of $\Pi^0_1$-statements (ie statements of the form $\forall n \in \mathbb{N} \ P(n)$ for decidable properties $P$). Knowing a particular $\mathrm{BB}(m)$ means knowing all $\Pi^0_1$-statements of complexity $m$ (for a suitable complexity measure).

For any c.e. theory $T$, $\mathrm{Con}(T)$ is a $\Pi^0_1$-statement. Moreover, if $T$ is of the form "$\mathrm{ZFC}$ + some short axiom", the complexity of $\mathrm{Con}(T)$ (in the sense above) will not be much more than the complexity of $\mathrm{Con}(\mathrm{ZFC})$. Hence if we want to settle values of the Busy-Beaver function on "medium-sized" inputs, we would need to add axioms that settle a lot of consistency statements.

Proving that adding an axiom actually increases the range of provable Busy-Beaver values will be non-trivial. It does not suffice to show that it settles more $\Pi^0_1$-statements, but one needs to show that actually increases the least complexity of an undetermined $\Pi^0_1$-statement. Unfortunately, the complexity notion here is essentially Kolmogorov complexity -- which means that we cannot compute the complexity of a logical formula from that formula.