27
$\begingroup$

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.

$\endgroup$
20
  • 3
    $\begingroup$ "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 $\operatorname{BB}(n)$": is this a suspicion, or a theorem? (And what does it mean to "prove the value" of something?) $\endgroup$
    – LSpice
    Jan 11 at 21:08
  • 2
    $\begingroup$ @LSpice I asked myself the same question, and wikipedia led me to this article: arxiv.org/abs/1605.04343 $\endgroup$ Jan 11 at 21:10
  • 4
    $\begingroup$ Thanks! The name of the article @user2520938 referenced: Yedidia and Aaronson - A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory. $\endgroup$
    – LSpice
    Jan 11 at 21:11
  • 3
    $\begingroup$ @Sam Hopkins For example, if we assume Con(ZFC) then the Turing machine referenced in Yedidia and Aaronson doesn’t halt, and assuming the negation of Con(ZFC) gives that this Turing machine does halt. $\endgroup$
    – exfret
    Jan 11 at 21:14
  • 7
    $\begingroup$ You could always add an axiom of the sort: $BB(5)=193894749339392$. This one is almost surely inconsistent (because I made up that large integer). With such an axiom, the value of $BB(5)$ is very easy to find. $\endgroup$ Jan 11 at 21:57
20
$\begingroup$

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.

$\endgroup$
10
  • 7
    $\begingroup$ "Of course, this is absurd" It's true for sufficiently large values of $3$ and $17$! $\endgroup$ Jan 12 at 5:17
  • 1
    $\begingroup$ Maybe this is getting too far away from the OP's question, but is there any work in the philosophy of math on treating Turing machines as physical objects which we can investigate empirically (in order to determine mathematical truths)? That seems to be a viewpoint certain "realistically" minded people want to take (see also this other MO question mathoverflow.net/questions/34710/…) $\endgroup$ Jan 12 at 5:35
  • $\begingroup$ An easier question (perhaps?) .... let the bounding number of PA be the smallest value $n$ such that there exists some machine of size $n$ for which PA can't prove its halting. Now bounding number of PA is $\leq$ to set theory. For some standard agreed upon computation model (such as in question), is it known that bounding number of PA is strictly smaller than set theory? In fact while we are at it, what is known about relation between bounding numbers of HA and PA (for example) or other theories? $\endgroup$
    – SSequence
    Jan 12 at 8:07
  • $\begingroup$ I meant "can't prove its non-halting" in last comment. $\endgroup$
    – SSequence
    Jan 12 at 8:53
  • 3
    $\begingroup$ @exfret : SSequence is correct. The technical way to say "any Turing machine whose non-haltingness is provable in ZFC does not halt" is "ZFC is $\Sigma_1$-sound" or "ZFC is 1-consistent." This is a stronger assumption than "ZFC is consistent." (It is also weaker than "ZFC is arithmetically sound" which would mean that any arithmetic statement provable in ZFC is true of the standard integers). So you could demand that any proposed new axiom A have the property that not only is ZFC + A consistent, but it is also $\Sigma_1$-sound. Almost everyone would agree with you, I think. $\endgroup$ Jan 12 at 13:34
18
$\begingroup$

$\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.)

$\endgroup$
11
  • $\begingroup$ $\DeclareMathOperator\BB{BB}$I don't really understand this answer. Why would the definition of $\BB$ in such a model allow the Turing machine to run for a non-standard number of steps? $\endgroup$ Jan 11 at 21:55
  • 3
    $\begingroup$ @user2520938 The definition of BB allows Turing machines to run for any natural number of steps. In worlds with nonstandard natural numbers, they're included in "any natural number". $\endgroup$ Jan 11 at 22:05
  • $\begingroup$ Hm I see. I'm not sure that your answer answers the question though. The question is not about changing the values of BB, but about making it possible to prove the exact values of BB. $\endgroup$ Jan 11 at 22:08
  • $\begingroup$ @user2520938 True, but the question also mentions that "in a way, this “real world” value changes depending on our philosophical stance." $\endgroup$ Jan 11 at 22:13
  • 1
    $\begingroup$ @Andreas: I think that other than the heartbreak, most of the problems belong to the people of my generation and those that follow. Especially those without a permanent job... :-P $\endgroup$
    – Asaf Karagila
    Jan 12 at 19:16
8
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.