An analogue of Rayo's function for ordinals I have spent a little time, just for fun, wondering about how to construct larger and larger countable ordinals, and I finally tried to take a cue from Rayo's function by considering the following $\rho: \omega \rightarrow \text{On}$:
"$\rho(n)$ is the supremum of all ordinals arising as limits of ordinal notations that can be defined with at most $n$ symbols".
Actually, I'm not sure about how to formalize this, but I'm quite sure that it can be done in a reasonable way (just to give an idea: $\rho(n)$ shall be larger than $\Gamma_0$ if $n$ is large enough to define the sum between ordinals, the function $\varphi_0(x)=\omega^x$ and the inductive step that constructs each Veblen function $\varphi_{\alpha}$ in terms of the previous ones).
So, assuming that this $\rho$ is well defined, can we say that it is uncomputable in any sense (like the ordinary Rayo's function)?  And also, is it true that $\sup\limits_{n \in \omega} \rho(n)=\omega_1^{\text{CK}}$?
 A: Of course it's going to depend a lot on how you choose to formalize it. Let me examine, though, two reasonable approaches to consider.

*

*(Small ordinal Rayo) There is a formal notion of "notation for a computable ordinal" - namely, Kleene's $\mathcal{O}$. So you could just look at the function $r(n)=$ "The least $\alpha$ such that there is some notation $a\in\mathcal{O}$ with $\vert a\vert_\mathcal{O}=\alpha$ and $a$ can be defined in $<n$ symbols." In this case we immediately have $\sup_{n\in\omega}r(n)=\omega_1^{CK}$.


*(Big ordinal Rayo) We could also just lift the definition of Rayo's function verbatim: "$R(n)$ is the least ordinal not definable by a sentence with fewer than $n$ symbols." In general $R$ is much bigger than $r$. After all, $\omega_1^{CK}$ is itself definable so we have $\omega_1^{CK}<R(k)$ for some large-but-finite $k$.

Of course, each of the above approaches runs afoul of the usual issue: what exactly do we mean by "defined by?"
The small approach is surprisingly nice since we're bounding everything by $\omega_1^{CK}$ a priori; any reasonable notion of definability will lead to the same supremum, even if the specific values of the function change. However, the big approach goes about as poorly as you'd expect. After all, naively speaking the ordinal $\sup_{n\in\omega}R(n)$ is definable, isn't it?
Granted, this was an issue with the original Rayo's function itself as well. The solution was of course to recognize that Rayo's function is defined in a richer language than the definitions it considers, and that fix has to be employed here as well. But in fact the big approach throws this nuance into even sharper relief since there are models of $\mathsf{ZFC}$ in which every ordinal is definable! These are called Paris models. There are also models in which everything is definable - these are called pointwise-definable models.
