I am slightly confused about the definition of the Rayo function and Rayo's number, and how it relates to the Busy Beaver function. I know that ZFC can't pin down the precise value of even $BB(7918)$. However, ZFC can define the Busy Beaver function itself, in less than, say, a billion symbols. So, we can form the number $BB(7918)$, and even $BB(BB(7918))$, using way less than a googol symbols of ZFC. But now here is where I am confused. Since ZFC can't determine the value of $BB(7918)$, is it even legitimate to give a lower bound for Rayo's number as $BB(7918)$? Do we only use descriptions of numbers that ZFC can prove define a number uniquely? I would be grateful if someone clarified this matter for me, and told me the exact definition of the Rayo function and whether it is a well-defined function at all.
A confusion regarding Rayo’s number and Busy Beaver function.
big numberslogic
Related Solutions
As some of the comments already mentioned, you misquoted the definition. The correct definiton (quoting Googology Wiki) is:
the smallest positive integer bigger than any finite positive integer named by an expression in the language of first order set theory with a googol symbols or less
So while there are only approximately $(10^{100})^{(10^{100})}$ possible expressions, and only a very small fraction of them actually name a number, Rayo's number can be very large.
We don't exactly know how large, but there are good heuristic arguments that the busy beaver function $\Sigma$ can be implemented in a few million symbols. Given that $\Sigma$ grows much faster then $\mathrm{TREE}$ and all other computable functions, Rayo's number is much larger than $(10^{100})^{(10^{100})}$ .
Your question is about what I view as the definable-in-set-theory analogue of the busy beaver problem. I had previously posted an answer on MathOverflow to the corresponding question concerning what I view as the definable-in-arithmetic analogue of the busy-beaver function. The main conclusion there was that this function has a growth rate exceeding any arithmetically definable function, and furthermore, that the function is not itself arithmetically definable.
A similar analysis works for your function.
The first thing to notice is that what you call the Rayo function is not definable in the first-order language of set theory. Basically, you haven't actually defined a function, because the concept of which numbers are definable or not is not expressible in the same language.
But in second-order set theory, or at least in the set theory having a proper class truth predicate, then we can define the Rayo function, by reference to that truth predicate. Such a predicate, for example, is provable in Kelley-Morse set theory, as I explain in my blog post Kelley-Morse implies con(ZFC) and much more.
So let us work in the theory GBC + Tr is a satisfaction class or truth predicate for first-order set-theoretic truth. With this class, the Rayo function $R(n)$ is definable, since we can refer to the truth predicate to find out which functions are definable.
Theorem. The function $R(n)$ eventually dominates every set-theoretically definable function.
Proof. Suppose that $f:\mathbb{N}\to\mathbb{N}$ is a set-theoretically definable function, so that the relation $f(x)=y$ is definable in the language of set theory by some formula $\varphi(x,y)$.
Notice that with the powers of two, we can easily define large numbers with comparatively small formulas. For example, $2^n$ is definable by a formula of size $n+c$ for some constant $c$. Put differently, and by iterating this, for any sufficiently large $k$ we can define a number $k^+$ larger than $k$ with a formula smaller than $\log(\log(k))$.
Therefore, if $k$ is very large with respect to these constants and the size of the definition of $f$, then we can define $\max_{x\leq k^+}f(x)$ using a formula of size less than $k$. Thus, $f(k)\leq R(k)$, as desired. QED
Corollary. It is not possible to provide a first-order set-theoretic definition of the Rayo function.
Proof. If you could define it, then add one, and this would be a definable function not dominated by the Rayo function, contrary to the previous theorem. QED
In particular, we cannot define this function in ZFC set theory, and I don't find it meaningful to talk about the Rayo function in a general mathematical context without further specifying the foundational context, such as whether there is a truth predicate available or not.
For example, the formal definition that you provided from the link involves a second-order quantifier $\forall R$, but it will not work in all models of second-order set theory GBC, since it presumes that there is a truth function. But it will work in Kelley-Morse set theory or in GBC + Truth predicate. One can improve the definition somewhat by asking for $R$ to be only a partial satisfaction class, defined on all formulas of complexity less than $n$, and then you'll get a definition that works in GBC, but it will not be provably total, although it will be defined on the standard finite numbers. But GBC is not strong enough with separation for the function to exist as a set, since it is being defined with a second-order quantifier.
Meanwhile, however, your actual question is about small values of $n$, and in this case, if one is referring only to a bounded part of the Rayo function, then the question is perfectly sensible, since for every particular finite $n$, we have a $\Sigma_n$ truth predicate and a way of referring to truth defined by formulas of size at most $n$. And so one can still hope to prove lower bounds for $R(n)$ for various small values of $n$.
In particular, for the Rayo number itself, which takes $n$ as a googol symbols, the function is definable.
But let me point out further that once $n$ gets to have sufficient size, then the values of $R(n)$ will become independent of ZFC. For example, in set theory, we can define a number $k$ to be the smallest such that $2^\omega$ has size $\aleph_k$, if there is such a finite number $k$, and otherwise $0$. The point now is that this defines a definite number in set theory, but ZFC does not settle what the value is or provide any upper bound in the natural numbers. For this reason, after a few steps, the nature of the function $R(n)$ becomes completely wrapped up in the meta-mathematical foundational issues I have alluded to earlier.
In particular, since I believe that the definition I provided can be made formally in fewer than a googol symbols, the particular value of Rayo's number, R(googol), is independent of ZFC, and no upper bound can be proved in ZFC for it.
Best Answer
Short version: Rayo's function doesn't relate at all to the Busy Beaver function. (Or rather there is an obvious relation - Rayo is way way way way WAY bigger than the Beaver - but the Busy Beaver just isn't relevant to Rayo.) Rayo is fundamentally about truth rather than provability, and so the relevant "logical obstacle" is Tarski's undefinability theorem rather than the incomputability of the halting problem.
In more detail:
Rayo's function $R$ has nothing to do with provability, in $\mathsf{ZFC}$ or otherwise. Simply stated, $R(n)$ is $1$ + the supremum of the natural numbers which are definable in set theory by formulas of length $<1$. Here, we say that a natural number $a$ is defined by a formula $\varphi$ iff $a$ is the unique object satisfying $\varphi$ in the sense of $V$, that is, the unique thing such that $V\models\varphi(a)$. The question of whether $\varphi(a)$ is provable in some theory or other doesn't arise. So $BB(7918)$ is indeed a lower bound for Rayo's number $R(10^{100})$.
However, this does mean that we run into Tarski's theorem: Rayo's function cannot itself be defined within $V$ (and in particular it doesn't even make sense to ask what $\mathsf{ZFC}$ does or does not prove about it). Rather, to talk about $R$ we need to work in a context rich enough to define "truth in $V$" - such as some appropriate class theory. So it does make sense to ask, for example, whether $\mathsf{NBG}$ proves that $R(10^{100})>BB(7918)$ (which it indeed does, quite easily).
It may help to first consider the "arithmetic Rayo function" - this is the map $R_{arith}$ sending $n$ to $1$ + the supremum of the natural numbers which are definable by formulas of length $<n$ in the structure $\mathfrak{N}=(\mathbb{N};+,\times)$. The function $R_{arith}$ is (again, per Tarski) not definable in $\mathfrak{N}$ itself; however, it is easily definable in set theory, and so it makes sense to ask what $\mathsf{ZFC}$ proves about $R_{arith}$.
It may also help to contrast $R$ with the "provability analogue" of the Busy Beaver function: let $P_{\mathsf{ZFC}}$ be the function sending $n$ to $1$ + the supremum of the natural numbers $k$ such that there is a formula $\varphi$ in set theory of length $<n$ such that $\mathsf{ZFC}$ proves that $\varphi$ holds of $k$ and only $k$. The function $P_{\mathsf{ZFC}}$ may superficially seem like Rayo's function, but it's really just a Busy Beaver variant (and in particular is easily definable in set theory).
Finally, there is a "local version" of the Rayo function: for $n\in\omega$ and $M$ (for simplicity) a transitive model of $\mathsf{KP}$, let $R_{loc}(n,M)$ be $1$ + the supremum of the natural numbers $k$ such that there is some formula $\varphi$ with $\{x\in M: M\models\varphi(x)\}=\{k\}$. The function $R_{loc}$ is definable in set theory again, since we're only ever asking about truth in set-sized structures, but for each appropriate $M$ the function $n\mapsto R_{loc}(n,M)$ is not definable in $M$.
Now you may ask: why have I defined $R$ and $P_{arith}$ in terms of suprema above, rather than maxima? Well, thinking set-theoretically it becomes quite natural to consider a "super-Rayo function" $S$ which applies to arbitrary ordinals: for an ordinal $\alpha$ let $S(\alpha)$ be the supremum of the ordinals $\beta$ such that there is some $\mathcal{L}_{\infty,\infty}$-formula of length $<\alpha$ which defines $\beta$.
I don't know offhand of a particular application of $S$, but to me it actually seems a bit more interesting than $R$. For example, consider the "ultra-Rayo" function $U$, defined as $S$ but using $\mathcal{L}_{\infty,\omega}$ instead of $\mathcal{L}_{\infty,\infty}$. This gives a slower-growing function than $S$ which is still pretty fast-growing, and at a glance it seems like there might be some nontrivial comparisons to be drawn. And these are merely two of the many extensions of first-order logic which let us talk about arbitrarily large ordinals. So I'm happy to use "supremum" rather than "maximum" even in the finite case, in order to smooth the way for these variants.
Wait, what is the "length" of an infinitary formula? Well, we'll define it recursively, similarly to quantifier rank or similar complexity notions. For example, we should probably set $$len("\bigvee_{\alpha<\theta}\varphi_\alpha")=(\sum_{\alpha<\theta}len(\varphi_\alpha))+1$$ or something similar. The point is that it's not hard to extend the notion of length to infinitary formulas, even if it's not immediately clear which extension is the "right" one, and as soon as we do we get the ultra- and super-Rayo functions emerging as natural objects of study.