# Succinctly naming big numbers: ZFC versus Busy-Beaver

Years ago, I wrote an essay called Who Can Name the Bigger Number?, which posed the following challenge:

You have fifteen seconds. Using standard math notation, English words, or both, name a single whole number---not an infinity---on a blank index card. Be precise enough for any reasonable modern mathematician to determine exactly what number you’ve named, by consulting only your card and, if necessary, the published literature.

The essay went on to discuss systems for naming increasingly huge numbers concisely---including the Ackermann function, the Busy Beaver function, and super-recursive generalizations of Busy Beaver.

Recently (via Eliezer Yudkowsky), the claim has come to my attention that there are ways to concisely define vastly bigger numbers than even the super-recursive Busy Beaver numbers, using set theory. (See for example this page by Agustín Rayo, which proposes a definition based on second-order set theory.) However, whether these definitions work or not seems to hinge on some very delicate issues about definability in set theory.

So, I have a specific question about fast-growing integer sequences that are "well-defined," as I understand the term. But first, let me be clear about some ground rules: I'm certainly fine with integer sequences whose values are unprovable from (say) the axioms of ZFC, as sufficiently large Busy Beaver numbers are. Crucially, though, the values of the sequence must not depend on any controversial beliefs about transfinite sets. So for example, the "definition"

n := 1 if CH is true, 2 if CH is false

makes sense in the language of ZFC, but it wouldn't be acceptable for my purposes. Even a formalist---someone who sees CH, AC, large-cardinal axioms, etc. as having no definite truth-values---should be able to agree that we've picked out a specific positive integer.

Let me now describe the biggest numbers I know how to name, consistent with the above rules, and then maybe you can blow my numbers out of the water.

Given a Turing machine M, let S(M) be the number of steps made by M on an initially blank tape, or 0 if M runs forever. Then recall that BB(n), or the nth Busy Beaver number, is defined as the maximum of S(M) over all n-state Turing machines M. BB(n) is easily seen to grow faster than any computable function. But for our purposes, BB(n) is puny! So let's define $BB_1(n)$ to be the analogue of BB(n), for Turing machines equipped with an oracle that computes $BB_0(n):=BB(n)$. Likewise, for all positive integers k, let $BB_k$ be the Busy Beaver function for Turing machines that are equipped with an oracle for $BB_{k-1}$. It's not hard to see that $BB_k$ grows faster than any function computable with a $BB_{k-1}$ oracle.

But we can go further: let $BB_{\omega}$ be the Busy Beaver function for Turing machines equipped with an oracle that computes $BB_k(n)$ given (k,n) as input. Then let $BB_{\omega+1}$ be the Busy Beaver function for Turing machines with an oracle for $BB_{\omega}$, and so on. It's clear that we can continue in this way through all the computable ordinals --- i.e. those countable ordinals $\alpha$ for which there exists a way to describe any $\beta < \alpha$ using a finite number of symbols, together with a Turing machine that decides whether $\beta < \beta'$ given the descriptions of each.

Next, let $\alpha(n)$ be the largest computable ordinal that can defined (in the sense above) by a Turing machine with at most n states. Then we can define

$f(n) := BB_{\alpha(n)}(n),$

which grows faster than $BB_{\alpha}$ for any fixed computable ordinal $\alpha$.

A different way to define huge numbers is the following. Given a predicate $\phi$ in the language of ZFC, with one free variable, say that $\phi$ "defines" a positive integer m if m is the unique positive integer that satisfies $\phi$, and the value of $m$ is the same in all models of ZFC.

Then let z(n) be the largest number defined by any predicate with n symbols or fewer.

One question that immediately arises is the relationship between f(n) and z(n). I don't think it's hard to show that there exists a constant c such that $f(n) < z(n+c)$ for all n (please correct me if I'm wrong!) But what about the other direction? Does z(n) grow faster than any function definable in terms of Turing machines, or can we find a function similar to f(n) that dominates z(n)? And are there other ways of specifying big numbers that dominate them both?

Update (8/5): After reading the first few comments, it occurred to me that the motivation for this question might not make sense to you, if you don't recognize a distinction between those mathematical questions that are "ultimately about finite processes" (for example: whether a given Turing machine halts or doesn't halt; the values of the super-recursive Busy Beaver numbers; most other mathematical questions), and those that aren't (for example: CH, AC, the existence of large cardinals). The former I regard as having a definite answer, independently of the answer's provability in any formal system such as ZFC. (If you doubt that there's a fact of the matter about whether a given Turing machine halts or runs forever, then you might as well also doubt that there's a fact of the matter about whether a given statement is or isn't provable in ZFC!) For questions like CH and AC, by contrast, one can debate whether it even means anything to discuss their truth independently of their provability in some formal system.

In this question, I'm asking about integer sequences that are "ultimately definable in terms of finite processes," and which one can therefore regard as taking definite values, independently of one's beliefs about set-theoretic questions. Of course, "ultimately definable in terms of finite processes" is a vague term. But one can list many statements that certainly satisfy the criterion (for example: anything expressible in terms of Turing machines and whether they halt), and others that certainly don't (for example: CH and AC). A large part of what I'm asking here is just how far the boundaries of the "definable in terms of finite processes" extend!

Yes, it's possible that my question could degenerate into philosophical disagreements. But a priori, it's also possible that someone can give a sequence that everyone agrees is "definable in terms of finite processes," and that blows my f(n) and z(n) out of the water. The latter would constitute a completely satisfying answer to the question.

Update (8/6): It's now been demonstrated to my satisfaction that z (as I defined it) is blown out of the water by f. The reason is that z is defined by quantifying over all models of ZFC. But by the Completeness Theorem, this means that z can also be defined "syntactically," in terms of provability in ZFC. In particular, we can compute z using an oracle for the $BB_1$ function (or possibly even the BB function?), by defining a Turing machine that enumerates all positive integers m as well as all ZFC-proofs that the predicate $\phi$ picks out m.

So thanks -- I didn't want to prejudice things, but this is actually the answer I was hoping for! If it wasn't clear already, I'm interested in big numbers not so much for their own sake, but as a concrete way of comparing the expressive power of different notational systems. And I have a strong intuition that Turing machines are a "maximally expressive" notational system, at least for those numbers that meet my criterion of being "ultimately defined in terms of finite processes" (so in particular, independent of the truth or falsehood of statements like CH). If one could use ZFC to define integer sequences that blew my sequence f(n) out of the water (and that did so in a model-independent way), that would be a serious challenge to my intuition.

So let me refocus the question: is my intuition correct, or is there some more clever way to use ZFC to define an integer sequence that blows f(n) out of the water?

Actually, a proposal for using ZFC to at least match the growth rate of f now occurs to me. Recall that we defined the sequence z by maximizing over all models M of ZFC. However, this definition ran into problems, related to the "self-hating models" that contain nonstandard integers encoding proofs of Not(Con(ZFC)). So instead, given a model M of ZFC and a positive integer k, let's call M "k-true" if every $\Pi_k$ arithmetical sentence S is true in M if and only if S is semantically true (i.e., true for the standard integers). (Here a $\Pi_k$ arithmetical sentence means a sentence with k alternating quantifiers, all of which range only over integers.)

Now, let's define the function

$z_k(n)$

exactly the same way as z(n), except that now we only take the maximum over those models M of ZFC that are k-true.

This remains to be proved, but my guess is that $z_k(n)$ should grow more-or-less like $BB_{k+c}(n)$, for some constant c. Then, to get faster-growing sequences, one could strengthen the k-truth requirement, to require the models of ZFC being maximized over to agree with what's semantically true, even for sentences about integers that are defined using various computable ordinals. But by these sorts of devices, it seems clear that one can match f but not blow it out of the water---and indeed, it seems simpler just to forget ZFC and talk directly about Turing machines.

-
Possible duplicate question: mathoverflow.net/questions/32891/… –  Joel David Hamkins Aug 6 '10 at 1:36
The largest number I can define in 1000 or fewer symbols can be defined as: "the largest number I can define in 1000 or fewer symbols". The number described before the colon is well defined if and only if the quoted phrase defines it. Slightly more seriously, this isn't a question with a well-defined answer, because "can be defined" is not at mathematically precise. I'm also sorry to say this is the third instance of this question on MO (cf. 8390, 34462). One way to save the question might be to ask about published notation systems for fast growing functions (growing faster than tetration). –  Carl Mummert Aug 6 '10 at 1:39
Joel and Carl: I apologize for the overlap! However, I did see 8390 and 34462 a while ago, and they didn't address what I'm asking about here. Yes, I'm well aware of the inherent ambiguity in asking for "the biggest number nameable with n symbols," so feel free to reinterpret the question as being about "some particular kinds of really big numbers nameable with n symbols." Specifically: can you construct a fast-growing sequence that blows the two particular sequences I mentioned (f(n) and z(n)) out of the water? And what can you say about the relation of f(n) and z(n) to each other? –  Scott Aaronson Aug 6 '10 at 1:57
I think this question is good, although it seems to ask a different question at the beginning than the end. Namely, at the beginning OP asks for us to play the "largest integer" game, which is not a great MO question, but at the end asks a very particular question relating two different functions. I recommend that the latter question be fronted, as it seems that that's really what Scott wants to know. –  Theo Johnson-Freyd Aug 6 '10 at 3:12
I am sorry that you feel I haven't engaged your question, since I did spend some effort writing what I thought to be a careful answer, trying to explain some of the problems that arise with a naive treatment of definability. My comment about you retreating into the meta-theory was in reference to your comment to my answer, where you seem explicitly to do this. Incidently, how does your definition of $z_2(100)$ work, if there are no $2$-correct models of ZFC? (As far as we know, this hypothesis is consistent with ZFC and could be the true state of affairs.) –  Joel David Hamkins Aug 6 '10 at 18:50

I think your question is not as precise as you portray it.

First, let me point out that you have not actually defined a function $z$, in the sense of giving a first order definition of it in set theory, and you provably cannot do so, because of Tarski's theorem on the non-definability of truth. We simply have no way to express the relation x is definable in the usual first-order language of set theory. More specifically:

Theorem. If ZFC is consistent, then there are models of ZFC in which the collection of definable natural numbers is not a set or even a class.

Proof. If V is a model of ZFC, then let $M$ be an internal ultrapower of $V$ by a nonprincipal ultrafilter on $\omega$. Thus, the natural numbers of $M$ are nonstandard relative to $V$. The definable elements of $M$ are all contained within the range of the ultrapower map, which in the natural numbers is a bounded part of the natural numbers of $M$. Thus, $M$ cannot have this collection of objects as a set or class, since it would reveal to $M$ that its natural numbers are ill-founded, contradicting that $M$ satisfies ZFC. QED

In such a model, your definition of $z$ is not first order. It could make sense to treat your function $z$, however, in a model as an externally defined function, defined outside the model (as via second-order logic). In this case, $z(n)$ only involves standard or meta-theoretic definitions, and other problems arise.

Theorem. If ZFC is consistent, then there is a model of ZFC in which $z(n)$ is bounded by a constant function.

Proof. If ZFC is consistent, then so is $ZFC+\neg Con(ZFC)$. Let $V$ be any model of this theory, so that there are no models of ZFC there, and the second part of the definition of $z$ becomes vacuous, so it reduces to its definable-in-$V$ first part. Let $M$ be an internal ultrapower of $V$ by an ultrafilter on $\omega$. Thus, $M$ is nonstandard relative to $V$. But the function $z$, defined externally, uses only standard definitions, and the definable elements of $M$ all lie in the range of the ultrapower map. If $N$ is any $V$-nonstandard element of $M$, then every definable element of $M$ is below $N$, and so $z(n)\lt N$ for every $n$ in $M$. QED

Theorem. If ZFC is consistent, then there is a model of ZFC in which $f(n)\lt z(10000)$ for every natural number n in the meta-theory.

Proof. If ZFC is consistent, then so is $ZFC+\neg Con(ZFC)+GCH$. Let $V$ be a countable model of $ZFC+\neg Con(ZFC)+GCH$. Since $V$ has no models of ZFC, again the second part of your definition is vacuous, and it reduces just to the definability-in-$V$ part. Let $M$ again be an internal ultrapower of $V$ by an ultrafilter on $\omega$, and let $N$ be a $V$-nonstandard natural number of $M$. Every definable element of $M$ is in the range of the ultrapower map, and therefore below $N$. In particular, for every meta-theoretic natural number $n$, we have $f(n)\lt N$ in $M$, since $f(n)$ is definable. Now, let $M[G]$ be a forcing extension in which the continuum has size $\aleph_N^M$. Thus, $N$ is definable in $M[G]$ by a relatively short formula; let's say 10000 symbols (but I didn't count). Since the forcing does not affect the existence of ZFC models or Turing computations between $M$ and $M[G]$, it follows that $f(n)\lt z(10000)$ in $M[G]$ for any natural number of $V$. QED

Theorem. If ZFC is consistent, then there is a model of ZFC with a natural number constant $c$ in which $z(n)\lt f(c)$ for all meta-theoretic natural numbers $n$.

Proof. Use the model $M$ (or $M[G]$) as above. This time, let $c$ be any $V$-nonstandard natural number of $M$. Since the definable elements of $M$ all lie in the range of the ultrapower map, it follows that every z(n), for meta-theoretic $n$, is included in the $V$-standard elements of $M$, which are all less than $c$. But $M$ easily has $c\leq f(c)$, and so $z(n)\lt f(c)$ for all these $n$. QED

-
I think we're still talking past each other: your 2nd two theorems both define models of ZFC containing non-standard integers, then consider z and f relative to those models. But I'm only interested in the functions' behavior on standard integers, and in the definition of z, m should be understood as ranging over standard integers only. As for your first theorem, and your argument about z running afoul of Tarski's indefinability theorem: I don't understand what you mean by "definable natural number." EVERY standard natural number is definable! The only question is how many symbols we need. –  Scott Aaronson Aug 6 '10 at 5:40
The main point of the first theorem is that we don't have a first-order expressible concept of definibility. Please see Tarski's theorem on the non-definibility of truth http:\\en.wikipedia.org/wiki/Tarski's_undefinability_theorem. –  Joel David Hamkins Aug 6 '10 at 5:55
I know Tarski's theorem, and I don't see that it's relevant here. Nothing that I said required a first-order predicate for definability. (As a possibly-related point, my notion of a predicate phi "defining" a positive integer m is meta-theoretic: the positive integers m that I'm talking about are the standard ones, not those in some particular model of ZFC.) –  Scott Aaronson Aug 6 '10 at 12:14
An issue is that the definitions of natural numbers in set theory may involve quantifiers not only over natural numbers, but over all sets. And the definition of z quantifies not only over all sets, but over all models of set theory. The background metatheory that you use has a significant impact on what sorts of models of set theory exist. –  Carl Mummert Aug 6 '10 at 13:10
Scott, the "standard natural numbers" cannot be defined in ZFC or any other first-order theory. If your notion of "definable" is not "first-order definable", then you need to be very precise about what notion of definability you're using. You'll also need to convince us that your non-first-order notion of definability has a sound and complete provability relation if you want to treat "having models" and "being provable" as the same concept. –  Adam Aug 8 '10 at 3:24

This is basically a comment but it's too long for that. I'm hoping that maybe I can help explain to Scott why there's an issue with his "definition" of "$\phi$ defines $m$."

The fundamental problem is that it's not clear what it means for $m$ to "satisfy $\phi$". We can certainly take the formula $\phi$ and syntactically insert $m$ to produce a formula $\phi(m)$. But merely producing $\phi(m)$ does not determine whether "$m$ satisfies $\phi$." Whether $m$ satisfies $\phi$ hinges on whether $\phi(m)$ is true. And it's not clear what this means.

When I say that it's not clear what it means, I'm not saying that we don't know any algorithm for determining truth. If that were the only issue then there would be nothing for a classical mathematician to complain about. The problem is worse than that. We don't know what the word "true" even means here. This is where Tarski's theorem comes in. We can't even define the word "true" using ordinary mathematical means. If we could, then we would be able to formalize that definition in ZFC, just like we can formalize all ordinary mathematical discourse, and that's just not possible.

Perhaps a concrete example will help. Let $\phi(x)$ be "$x=1$ and there is a cardinal strictly between $\aleph_0$ and $2^{\aleph_0}$." Does 1 satisfy $\phi$?

Now this problem isn't insurmountable. There are ways you can try to define truth. But it's a subtle business and you need to be explicit and careful. Without that, we don't have a clear definition of what it means for $m$ to satisfy $\phi$ and hence we don't have a clear definition of what it means for $\phi$ to define $m$.

-

This isn't an answer, but it's too long for a comment.

I don't think the computable ordinals are well enough defined for the function $f(n)$ to work. Suppose you give me a system mapping {$0,1$}$^*$ into the computable ordinals. I'll give you a system, which is your system together with a new symbol, $2$, which stands for the smallest ordinal you can't define in your system. I can then map the numbers {$0,1,2$}$^*$ back into {$0,1$}$^*$; my system reaches a computable ordinal that's not defined in your system, and it even defines it with length 2.

So the computable ordinals are a concept that makes sense, but it is impossible to have a single encoding that gives you all of them. Thus, I don't see how your function $f$, which is defined using the phrase

Next, let $\alpha(n)$ be the largest computable ordinal that can defined (in the sense above) by a Turing machine with at most $n$ states.

works. You should be able to get a Turing machine with an oracle that corresponds to any computable ordinal, but that's where it stops.

-
Thanks, Peter! But I didn't claim to have a single encoding that gives all the computable ordinals. It's clear that, as you go to larger and larger computable ordinals, your encoding scheme will have to change. The function f was defined by maximizing the ordinal over all encoding schemes that are defined by a Turing machine with <=n states. (Of course, this maximum won't be computable or even first-order definable, but its meaning nevertheless seems sufficiently clear!) –  Scott Aaronson Aug 6 '10 at 14:26
Hi Scott, Given that there's a universal Turing machine with a fixed number of states, how does increasing the number of states make your Turing machine more expressive? –  Peter Shor Aug 6 '10 at 14:34
Peter: Because I'm not assuming the ability to feed the Turing machine some "side-program," of unbounded length, that tells it what to do. –  Scott Aaronson Aug 6 '10 at 14:48
More formally: given a Turing machine M, let's say that M defines the computable ordinal alpha if the following holds. First, the function M(x,y) defines a total ordering on binary strings: M(x,y)=1 and M(y,z)=1 imply M(x,z)=1, and M(x,y)=M(y,x)=1 iff x=y, and either M(x,y)=1 or M(y,x)=1. Second, the total ordering so defined is a well-ordering. And third, the well-ordering has order type alpha. Then do you agree that, the more states M has, the larger the ordinal alpha we can define? –  Scott Aaronson Aug 6 '10 at 14:53
That makes everything clear ... I hadn't understood the connection between Turing machines and computable ordinals. –  Peter Shor Aug 6 '10 at 17:06

I have another question which is too long to fit into a comment: how do you even know that $f(n)$ is increasing?

If you have two Turing Machines $M$ and $M'$ that realize the same ordinal $\alpha$, there is no guarantee (as far as I can see) that $BB_\alpha^M(n) = BB_\alpha^{M'}(n)$, because (if $\alpha > \omega$) the Turing machine that computes $BB_\alpha^M$ needs to use the encoding defined by $M$ to index into ordinals less than $\alpha$. With $M$ and $M'$, there may not even be a computable map from the index generated by $M$ to the index generated by $M'$. You might be able to compute this map using $BB_\alpha^M$, but I don't even see how to do that. Thus, $BB_\alpha(n)$ doesn't seem well-defined; you need to specify the encoding into ordinals less than $\alpha$ for it to be well-defined. So even if $\alpha > \beta$, it's not clear that $BB^M_\alpha(n)$ grows faster than $BB^{M'}_\beta(n)$. It's possible that there are some computable ordinals where the index function is so complicated that you can't use it to compute anything useful.

You should be able to fix this by defining $f(n)$ to be $BB_\alpha^M(n)$ for the Turing machine $M$ with $n$ states so that $BB_\alpha^M(n)$ takes the maximum value over all such Turing machines.

UPDATE: and now I have what may be an answer to Scott's question. Is there any reason you have to have the Turing machine $M$ that defines the oracle for $\alpha$ be a vanilla Turing machine. Couldn't you let it have access to an oracle for BB, as well. This way, you can define classes using machines like $T_\alpha^{M_\beta^{M'}}$. Now, just let $f(n)$ be the maximum value for $BB_\alpha^M(n)$ where $M$ is a machine defined in this recursive manner using $n$ symbols.

Question: can you define ordinals that are strictly larger than any computable ordinal in this way? Or does this just define the same class of ordinals in much more complicated ways?

-
Thanks! Yeah, I was just thinking before about this encoding-dependence issue. Fortunately, there are a number of straightforward solutions, including the one you suggested, of maximizing BB over all n-state "base TMs" M as well as all n-state TMs that define an ordinal encoding for M's oracle. The proof that f is increasing (to say the least) will then be that, for every fixed Turing machine O defining a computable ordinal, f(n) dominates BB_O(n) for all n beyond some finite point. –  Scott Aaronson Aug 7 '10 at 17:54
Peter: No, certainly there's no reason for the Turing machine defining the ordinal to be a plain vanilla one! Given any collection of ideas for defining big numbers, you can always simply combine them to get a still bigger number. What I was looking for with this question was something a bit more ... dramatic. –  Scott Aaronson Aug 8 '10 at 14:57

I could be wrong, but I seem to have shown that $f$ is much faster growing than $z$. The intuition is that $f$ is a property of this beast with recursively growing Turing-degrees, while $z$ is defining numbers that TMs with low Turing degrees can figure out and outdo.

For any predicate $s$ in the language of ZFC with one free variable (call it "$x$"), let $M_s$ be a TM with an oracle for the halting problem that runs this algorithm given an integer $a$ as input:

   1  i := a
2  REPEAT:
*3      IF s(i->x) is a theorem of ZFC THEN:
4          HALT AND RETURN i
5      ELSE:
6          i := i + 1

* Denotes a step that depends on the halting oracle


Now in the space of all TMs with an oracle for $BB_1$, for any $n$ you'll find some $T_n$ that runs the following algorithm when given a blank tape:

   1  biggest := 0
2  FOR EACH n-or-fewer-character string s:
3      IF s is a predicate in the language of ZFC with one free var "x" THEN:
**4          IF M_s(1) halts THEN:
*5              b := M_s(1)
**6              IF M_s(b+1) loops forever THEN
7                  // Now we know s defines b
8                  IF b > biggest THEN:
9                      biggest := b
10  IDLE FOR biggest STEPS
11  HALT

*Denotes a step that depends on the BB_1 oracle by way of the halting oracle
**Denotes a step that depends on the BB_1 oracle
`

For all $n$, $T_n$ runs for a little longer than $z(n)$ steps when run on a blank tape. And there's no reason why the state count $S(T_n)$ of the most compact choice of $T_n$ should grow faster than $n$. Therefore $BB_2$(n) dominates $z(n)$.

-
Your algorithm is only using the second clause of the OPs notion of definability, where all ZFC models agree, since you search for proofs, but not the first part, where the definition must define $m$ in the universe. So you aren't really computing $z$ here. For example, your proof doesn't work in a model of $ZFC+\neg Con(ZFC)$, since you will be finding all kinds of meaningless proofs there. –  Joel David Hamkins Aug 6 '10 at 11:02
The issue is with proof vs. definability. The (standard part of the) oracle for the halting problem is different in different models of ZFC. For example, consider the program that searches for a proof of "0=1" from ZFC; this has a standard index $e$. In the standard model, $e$ is not in the halting set, but in some nonstandard models $e$ is in the halting set. So, when you formalize the algorithms above as formulas of ZFC, they may give different answers in different models. But your definition of $z$ quantifies over formulas that give the same answer in all models of ZFC. –  Carl Mummert Aug 6 '10 at 13:50
(continued) On the other hand, if you interpret everything above in the standard model of set theory, the issue is that there are plenty of formulas $s$ such that $M_s$ never halts, because $ZFC$ doesn't prove $s$, but $s$ is still true in the standard model. So in this case the second algorithm is not going to find the largest definable number, only the largest provably definable number. If you could test for truth in the first algorithm, that would solve this problem in the setting of the standard model, but Tarski's theorem prevents that. –  Carl Mummert Aug 6 '10 at 13:54
OK, thanks, I think I made my peace with this "paradox" over breakfast. The BB function has a definite meaning, independent of any formal system. And BB is also definable within ZFC (even though its values aren't provable beyond some finite point). The trouble is that BB as defined within ZFC need not coincide with the semantic BB function: whether it does or not will depend on the model. –  Scott Aaronson Aug 6 '10 at 14:31
(continued) And that's why it can be the case that, as Liron pointed out, the function z grows much slower f. So then, can anyone come up with a better ZFC-based integer sequence that avoids these problems and matches or (better yet) exceeds the growth rate of f, while not being dependent on a particular model of ZFC? Alternatively, maybe you can give a general argument that no such sequence exists? –  Scott Aaronson Aug 6 '10 at 14:37

It seems that the philosophical position you're taking for granted is close to the position called "predicativism" advocated by mathematicians such as Poincarè and Weyl, and whose boundaries have been delineated more precisely by Solomon Feferman. Roughly, Feferman's position is that the notion of an "arbitrary set" is not well-defined enough for statements like AC and CH to take on definite values. So instead we should restrict our attention to the natural numbers and any questions which are "implicit" in our concept of the natural numbers; for example, talking within Peano Arithmetic (PA) makes sense, but so does talking about the truth of PA-strings, and talking about the truth of strings which talk about the truth of PA-strings, and so on. In his system, questions about the Busy Beaver functions $BB_\alpha$ have definite values whenever $\alpha$ is an ordinal less than $\Gamma_0$, where $\Gamma_0$ is the Feferman-Schutte ordinal.

It might be possible to extend predicativity to some ordinals greater than $\Gamma_0$ without losing "truth-definiteness"; for example, this is argued by Nik Weaver. But I think extending to the first non-recursive ordinal (i.e. the Church-Kleene ordinal), which is implicit in the function $f(n) = BB_{\alpha(n)}(n)$ defined in the OP, is problematic. This is because the notion of "ordinalhood" is not a notion which is "ultimately definable in terms of finite processes", in your terms. To be more specific, let's recall that a computable ordinal is a computable ordering of $\mathbb N$ with the property that every nonempty subset of $\mathbb N$ has a least element with respect to this ordering. The notion of a computable ordering is certainly well-defined, but the ordinalhood property depends on universal quantification over the realm of subsets of the integers. According to Feferman, such quantification is ill-defined because "the concept of the totality of arbitrary subsets of $\mathbb N$ is essentially underdetermined or vague" -- because sets are introduced by definitions, and no formal system for describing how we define things can capture all of the different ways in which we can define things.

Now, you may disagree with Feferman on this point, perhaps being skeptical only of definite totalities consisting of all subsets of $\mathbb R$ or higher types. In which case I think that would be a new philosophical position, and it would be worth expanding on what exactly the boundaries of this system are, and what the motivation for those boundaries are.

On the other hand, without accepting the notion of a totality of subsets of $\mathbb N$, one can philosophically accept the notion of ordinalhood as somehow describing the "well-definedness" of concepts -- that is, an ordering of the integers is said to be an ordinal if any recursive definition (in a particular formal language) of a function $f:\mathbb N\to\mathbb N$ of the form $$f(n) = F(f\upharpoonleft \{m : m < n\})$$ determines a well-defined total function $f:\mathbb N\to\mathbb N$. But this raises issues of whether the concept of "well-definedness" is really a well-defined concept. Certainly, a diagonal argument may cause problems if we intend to mean the same thing by the two uses of the phrase "well-defined" in the previous sentence. Also, the dependence of this concept on the formal language used for the universal quantification over $F$ may also be problematic. (You can't quantify over all formal languages for the same reason you can't quantify over all sets.) But perhaps these philosophical issues are not too troublesome, in which case the question of whether or not a given ordering of the natural numbers is a well-ordering always has a definite truth value.

But in any case, it seems to me that if one accepts the notion of "well-definedness" described above, then one is no longer talking about those things which are "ultimately definable in terms of finite processes" -- instead, one has introduced new notions and is now talking about them.

So in conclusion, I don't think that the entry $f(n) = BB_{\alpha(n)}(n)$ given in the original post satisfies the rules for the contest laid down in the original post.

........

I've also spent some time thinking about the main question of this post, that is, what is the best strategy for winning a largest-number contest? After looking at a number of case studies (which I hope to write up at some point), I concluded that there are only three types of largest-number contests:

1. Those in which whoever has the (slightly) bigger paper to write on wins.
2. Those in which whoever has the most faith in (true) large cardinal axioms wins.
3. Those which are not well-defined as mathematical contests, but instead ask philosophical questions.

The first kind of contest can usually be judged on a reasonable timescale, while the second kind of contest can often be judged on an unreasonable timescale. The third kind can't really be judged at all.

The simplest example is the Busy Beaver Contest: Given a (reasonably large) $n$, the challenge is to write a Turing machine on $n$ symbols, and the winner is whoever has the longest runtime (and is thus the best approximation to $BB(n)$). The optimal strategy is this:

1. Pick a large cardinal axiom $\kappa$ that you think is $\omega$-consistent.
2. Enter the following program into the contest:

For every $\sigma\leq 3\uparrow\uparrow\uparrow 3$(

For every Turing machine $m$ of Gödel number $\leq 3\uparrow\uparrow\uparrow 3$(

If $\sigma$ is the Gödel number of a proof in $ZFC+\kappa$ that $m$ halts(

Run $m$)))

Essentially, what this strategy does is "run all of the strategies that your opponent might be using that you can prove halt". If your opponent is honest enough that he won't submit any entry that he doesn't believe will halt, and he doesn't believe any mathematical statement that can't be proven in a formal system of consistency strength $\leq ZFC+\kappa$, then you will win. So this is a contest of type 2.

An obvious modification to this contest would be to only allow entries which provably halt within some formal system, e.g. $\Sigma = PA$. (The proof of halting must be submitted with the entry, as otherwise the requirement is trivial since every program which halts, halts provably in PA.) Then the best strategy is to fix a large $n$ consider the formal system $\Sigma(n)$ which is the same as PA except that only statements of with $\leq n$ nested quantifiers are allowed in the proofs of theorems. Then $\Sigma(n)$ is provably $\omega$-consistent in PA, although the length of the proof of $\omega$-consistency increases as $n\to\infty$. So then you just replace $ZFC+\kappa$ by $\Sigma(n)$ in the previous strategy; now that strategy provably halts within PA. So as long as your $n$ is greater than your opponent's $n$, then you win. So this is a contest of type 1.

The original posting seems to be a largest-number contest of type 3...

-

Scott, I am trying to understand the difference between the two. Could you please explain the reason for BB being OK? It seems to me that the usual argument for existence of the values for BB should be provable in a very weak set theory. We form the set of halting TM with n states, prove that it is finite, and take the maximum of steps before halting for each of them. The reason we can not compute the values is the logical complexity of the formula defining BB, we could compute it if it was $\Sigma_1$, but it is not. Am I correct?

I guess that the distinction is about the complexity of the formula defining the function. It seems that you are OK with arbitrary quantifiers over natural numbers but not over sets of them. For example, what would you say if we use GC in place of CH?

So you are asking about arithmetical functions. What about BB for Turing machines with oracles in the arithmetical hierarchy?

Is using higher order quantifiers over natural numbers OK? What if I define it to be the BB for functions defined by such formulas?

I think the relation with truth predicate is that since you are OK with arithmetical formulas, you think they have definite truth values, but it seems that you don't think that formulas outside this hierarchy, e.g. those with set quantifiers over natural number necessary have definite truth values.

-
Kaveh, to start with the easy "yes or no" questions: yes, your understanding is correct that I'm fine with arbitrary quantification over natural numbers, and even more that that (e.g., the computable ordinals). However, when you start quantifying over sets of natural numbers, or sets of sets, I start to be skeptical that your question necessarily has a "Platonic answer" independent of the formal system. BB for Turing machines with oracles in the arithmetical hierarchy is fine -- in fact, it's essentially equivalent to the BB_k functions that I defined in the OP. –  Scott Aaronson Aug 7 '10 at 13:21
The essential distinction, for me, is between those mathematical questions that are ultimately about some "computable" process, and those that aren't. I see the former questions as always having "Platonic" right answers, even when independent of ZFC -- because that belief seems to me like a prerequisite for doing mathematics. (As I said before: if you deny there's an objective fact about whether a given Turing machine halts or doesn't halt, then why not also deny there's an objective fact about whether Theorem X is or isn't provable from Axioms Y? But that leads to infinite regress.) –  Scott Aaronson Aug 7 '10 at 13:32
(Amusingly, when I explained this 'debate' to other TCS folks, the distinction I'm making---between those questions that are ultimately phrasable in terms of Turing machines and those that aren't---was so self-evident that I had trouble convincing them that mathematicians tend to think in a completely different way! :) ) –  Scott Aaronson Aug 7 '10 at 13:38
I think that the problem is that TCS folks see algorithms as one of their basic building blocks, while logicians see algorithms as a concept which can only be defined by using other building blocks. If algorithms must be defined using other building blocks, they you have to worry about the definitions being interpreted in non-standard ways. –  Peter Shor Aug 8 '10 at 13:50
Peter: I agree! My argument boils down to the idea that, while you don't have to take algorithms as a basic building block of mathematics, you might as well do so. For, if you don't already know what an algorithm operating on natural numbers means, then neither PA, nor ZFC, nor second-order logic, nor any other formal system is going to clarify it for you. Understanding how to derive one ZFC statement from another one already presupposes that you understand computation. –  Scott Aaronson Aug 8 '10 at 14:32

This picks up Scott's further question

can anyone come up with a better ZFC-based integer sequence that avoids these problems and matches or (better yet) exceeds the growth rate of f, while not being dependent on a particular model of ZFC?

I can't see anything in the Turing machine style definition that can't be encoded with ZFC. Translate any TM-style definition of $f$ into a ZFC-style definition, using standard machinery such as treating the TM state transition table as a binary relation, letting an integer encode the current state of a tape, and collecting together the right objects into oracle sets. Then let $z$ be the ZFC-style definition of $f$.

In your definition of $f$ you are using a description which is more compact than ZFC, in the sense that your parameterize it with $n$ states in each of the two TMs you compose, instead of $n$ symbols which is all you allow for $z$.

What am I missing: what specific feature does the TM style definition bring that is not already in ZFC? I would agree that the TM style definition allows expressing larger numbers than an equivalent length ZFC description. But this seems to be a feature of what is being counted, not necessarily that TMs are more expressive, let alone "maximally" expressive.

-
Here's the problem. If you write "x = BB(n)" as a proposition in the language of ZFC with x as its free variable, then the ZFC axioms aren't sufficient to pin down a single value that x must have. So "the value of x defined in ZFC by 'x = BB(n)'" isn't a well-defined entry for Scott's contest. But if we just talk about Turing machines as their own meta-level thing, then "BB(n)" is a well-defined integer for Scott's contest. –  Liron Aug 8 '10 at 6:16
Then it seems Scott's further question is ill-posed, and that his original question also is ill-posed. It seems unfair to pose a contest between a formal system which is required to obey rigid rules, and a Platonic notion on which one doesn't impose such rules. If one drops the $z$ part of Scott's discussion, then I do not follow why we are supposed to believe that the notion of a TM is somehow maximally expressive. This is an intriguing notion, but I don't see how this discussion supports the claim. I'd love to see more about it, though! –  András Salamon Aug 9 '10 at 9:31
I think I agree, although I'm certainly no expert. It seems like the Turing machines get metatheoretic gifts (the oracles) that ZFC does not, and the latter has no way of gaining the same (if it even could) due to the restrictions. To be comparable, shouldn't we consider $ZFC_0$ to be the usual ZFC axioms, and then talk about the metatheoretic $g_0(n)$ being defined similar to $z(n)$ above? Then we can talk about $ZFC_1$ being $ZFC_0$ augmented with $g_0(n)$, which is allowed to be used in the formulas we will use to define $g_1(n)$. And so on, with ordinals and whatnot. –  Dan Doel Aug 14 '10 at 8:27