Working in Kellymorse 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)$?

$\begingroup$ Related $\endgroup$ – PyRulez Jan 20 '18 at 8:57

2$\begingroup$ This is a great question! Note that computing a model like that is equivalent to computing the theory $\text{Th}(V)$, since from the theory we can compute a Henkin model by the effective completeness theorem. So the question is: does Rayo's function compute the firstorder theory of $V$? $\endgroup$ – Joel David Hamkins Jan 20 '18 at 14:17

2$\begingroup$ I strongly suspect this depends on the choice of V. First, every Rayo's function is Turing Complete, so they compute some common completion of KM. So for a model of that completion, yes. I'm not terribly familiar with KM, but in ZFC, it wouldn't be hard to show that most standard forcings preserve Rayo's function. So one would be able to get uncountably many theories with the same Rayo's function, indicating that one of them isn't computed from it. Does the same work for KM? $\endgroup$ – Dan Turetsky Jan 20 '18 at 16:47

1$\begingroup$ @DanTuretsky I had similar ideas early this morning, but it seems to me now that things are much more subtle than this. First, it doesn't make sense to refer to Rayo's function in ZFC, since you need a truth predicate to define it. But second, it isn't at all clear that most standard forcing notions preserve Rayo's function exactly. Although it often happens that forcing preserves the definable sets and preserves which ordinals are definable, the sizes of the definitions can definitely change, and this affects the values of $R$. $\endgroup$ – Joel David Hamkins Jan 20 '18 at 18:36

1$\begingroup$ @lyricallywicked That's why I specified that we are working in Kelleymorse set theory, in which you can prove that it is welldefined. So, even if you disagree about whether or not its welldefined, you can agree that KM at least proves as much, and that KM is probably at least a consistient set of axioms to work with in. $\endgroup$ – PyRulez Apr 6 '18 at 15:20
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 firstorder 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.

1$\begingroup$ For pushing it all the way up the hyperarithmetic hierarchy, there's a standard result that any function that dominates all hyperarithmetic functions computes all hyperarithmetic sets. For each $\Sigma^1_1$ set, the Rayo function should uniformly compute a function $f$ such that, if the set is the graph of a function $g$, then $f(n) > g(n)$ for all $n$. Then just taking a diagonal sum gets a dominating function. $\endgroup$ – Dan Turetsky Jan 20 '18 at 20:31

$\begingroup$ @DanTuretsky Could you give a reference for this "standard result"? $\endgroup$ – Wojowu Jan 20 '18 at 20:40

1$\begingroup$ @Wojowu Earliest reference I have is the proof of theorem 6.8 from Jockusch's Uniformly Introreducible Sets (JSL 1968). It shows that for every hyperarithmetic set $A$, there is a hyperarithmetic function $f$ such that $A$ is computable from every $g$ majorizing $f$. $\endgroup$ – Dan Turetsky Jan 20 '18 at 21:41