A confusion regarding Rayo's number and Busy Beaver function.

Question

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.

Answer 1

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

• Note that $S(n)$ is generally much greater than $R(n)$ even when $n$ is finite - e.g. $\omega$ is pretty easily definable in the language of set theory by a finite-length formula.

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.