Would an oracle for Rayo's function let you compute a model of $(V, \in)$?

Question

Working in Kelly-morse set theory, let $R$ be an oracle that can compute Rayo's function. Can $R$ compute a countable model $M = (\mathbb N,\in_M)$ that is elementary equivalent to $(V, \in)$?

Answer 1

This is an excellent question!

Here are some steps in the positive direction. I claim that the Rayo function can compute the theory of true arithmetic. Indeed, I claim more, that we can push this into the hyperarithmetic hierarchy.

To see this, let's consider just true arithmetic first. Let $R$ be the Rayo function; so $R(n)$ is the smallest number not first-order definable in $V$ in the language of set theory by an expression of size at most $n$. [This definition is made relative to a fixed truth predicate, and it is not sensible to speak of the Rayo function in contexts where there isn't such a truth predicate. For example, we cannot refer to the Rayo function in ZFC, but it is fine in GBC+ETR or KM.]

Now, I claim that we can compute recursively whether a given statement $\sigma$ in the language of arithmetic is true or not in the standard model $\langle\mathbb{N},+,\cdot,0,1,<\rangle$. The same idea appears in my solution to the question, The set of largest numbers definable by formulas in different lengths.

The algorithm is this: we can compute atomic assertions directly, and we can reduce via Boolean combinations. The only difficult case is to check quantifiers $\exists m\ \varphi(m)$. But for this, I claim that it is sufficient to check whether $\varphi(k)$ holds for any $k$ up to $R(n)$, where $n$ is large enough to express the definition, "m is the least natural number for which $\varphi(m)$ holds in $\mathbb{N}$.'' The point is that if $\exists m\ \varphi(m)$ is true, then the least such $m$ will be definable and therefore will be smaller than $R(n)$ for that value of $n$. So we can use the Rayo function to reduce the infinite process of an existential quantifier into finitely many cases, since if none of those numbers works then we can be sure that there is no witness.

So the Rayo function $R$ computes $0^{(\omega)}$.

But actually, we can now push this further into the hyperarithmetic hierarchy. For example, we can compute $0^{(\omega+\omega)}$, which is the theory of the structure $\langle\mathbb{N},+,\cdot,0,1,<,0^{(\omega)}\rangle$. We just described how to compute atomic assertions in this structure, and now we can do the same trick again to get the theory of this structure, by using $R$ to bound the existential witnesses.

It seems to me that we can push this method much further, well into the hyperarithmetic hierarchy. But I'm not sure exactly how far. You want to push it all the way to $\text{Th}(V,\in)$, which is quite a bit farther indeed.