The first few values of Rayo's function?

Rayo's function defined in English:

"$\operatorname{Rayo}(n)$ is the smallest positive integer bigger than any finite positive integer named by an expression in the language of first order set theory with $n$ symbols or less."

More formally, we make use of the following second-order formula (Sat):

∀R {
{for any (coded) formula [ψ] and any variable assignment t
(R( [ψ],t) ↔
( ([ψ] = `x_i ∈ x_j' ∧ t(x_1) ∈ t(x_j)) ∨
([ψ] = `x_i = x_j' ∧ t(x_1) = t(x_j)) ∨
([ψ] = `(∼θ)' ∧ ∼R([θ],t)) ∨
([ψ] = `(θ∧ξ)' ∧ R([θ],t) ∧ R([ξ],t)) ∨
([ψ] = `∃x_i (θ)' and, for some an xi-variant t' of t, R([θ],t'))
)} →
R([φ],s)}

where [φ] is a Gödel-coded formula and s is a variable assignment.

We then define $\operatorname{Rayo}(n)$ as:

The smallest number bigger than every finite number m with the following property: there is a formula φ(x) in the language of first-order set-theory (as presented in the definition of `Sat') with less than or equal to $n$ symbols and x as its only free variable such that: (a) there is a variable assignment s assigning m to x such that Sat([φ(x)],s), and (b) for any variable assignment t, if Sat([φ(x)],t), then t assigns m to x.

I do wonder, how many values of this function are explicitly known or have good bounds? For example, for $0\le n<10$, I speculate that $\operatorname{Rayo}(n)=0$, since it takes, I believe, ten symbols to write zero. Once we write zero, we get $\operatorname{Rayo}(10)=1$, and so on. So how many values can we reach?

I have not seen any good references for this.

Related: Is Rayo's number really that big?

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.