If Rayo number construction is not limited to first order set theory, will we be able to build much larger Rayo number? Rayo number is named by an expression in the language of first order set-theory. I wonder if we extend this definition to any higher order logics, will the result significantly change? (because for most (useful) models in higher logic we can still find expression in first order logic)
I am not professional in set theory/proof theory. But I will try to understand professional answers. Thank you!
 A: Yes. In general, given any logic $\mathcal{L}$ with a notion of "length of formula" according to which every formula is finite and only finitely many formulas have a given length (not all logics have such length notions!) and any "ambient structure" $\mathfrak{A}$ containing the naturals, the Rayo function for $\mathcal{L}$ in $\mathfrak{A}$ makes sense. This is the function sending $n$ to the smallest number greater than every $k$ such that $k$ is definable in $\mathfrak{A}$ by an $\mathcal{L}$-formula of length $\le n$. See here for a summary of definability in the context of first-order logic; the basics remain unchanged when we replace first-order logic with some other logic, and an element is definable iff (by definition) the singleton containing it is definable.
Rayo's function as usually defined takes $\mathfrak{A}$ to be the whole set-theoretic universe $V$. This isn't properly speaking a structure, since it's too big, and this is what saves us from the apparent paradox. Similarly, in order to make sense of the Rayo function for $\mathcal{L}$ in $V$ we'll need to cheat and work in some "even larger" mathematical system. But ignoring this issue for the moment, the answer to your question is definitely yes: changing the logic can dramatically change the corresponding function.
Here's one easy observation: since in any "reasonable" structure $\mathfrak{A}$, first-order truth is second-order definable, the Rayo function for $\mathsf{SOL}$ (= second-order logic) in $\mathfrak{A}$ will eventually dominate the Rayo function for first-order logic in $\mathfrak{A}$. In fact more is true: the latter won't even be $O$-of-the-former.
