What Turing degree would allow you to "compute" the axioms of ZFC in some countable model of ZFC?

Question

It is established in this post that you there is no computable model of ZFC, yet it can be computed in by a PA-degree oracle machine. Note that when we see "compute a model", we just mean that membership is decidable. My question is what Turing degree do you need if you want more than that?

In particular, we require the following:

• A computable set $S$, representing the sets.
• A decidable relation $\in_S$, such that $(S,\in_s)$ is a model for ZFC.
• That $=_s$ is computable (i.e. equality between sets in the model)
• Given a nonempty set $x$, we can compute a disjoint set $y$ such that $y \in_s x$ (axiom of regularity)
• For any formula $\phi(x)$ and given a set $x$, we may compute the set $\{x \in_s z : \phi(x)\}$ (axiom schema of specification)
• Given $x$ and $y$, we can compute $\{x,y\}$ (axiom of pairing)
• Given $x$, we can compute $\bigcup x$ (axiom of union)
• Given $x$, we can compute $P(x)$ (axiom of powerset)
• Given $x$, we can compute a well order for $x$ (Well-ordering theorem)

Note that we do need to worry about the axiom of infinity, or any of the axioms of replacement, since they assert that a certain set exists, and we can just "hard code" those constants as output.

Of course, this is based only just one axiomatization of ZFC. I could have asked about others, or I could just ask that for any provable statement $\exists x:\phi(x,y)$, given a $y$ we can compute a $x$ but this is just about getting a feel for what Turing degrees we will need for some axiomatization of ZFC.

What Turing degree is needed to compute all of the above. (My best guess is that any PA degree would be sufficient, since there is a PA degree computing a model of Morse-Kelly set theory, but I'm not sure.)

Answer 1

Any PA degree is still sufficient. (Emil answered this in the comments, I'm just expanding on how to do it.)

To see this, let's remember the characterization of PA degrees:

${\bf d}$ is PA iff for every computable theory $T$, ${\bf d}$ computes a model of $T$.

Now by "model," as you observe, I just mean the atomic diagram (e.g. for ZFC, the underlying set and the membership relation). However, the point is that I can improve this by appropriately changing the theory.

In this case, let's consider an expanded language. First, consider the language $$L^-=\{\in, c_{inf}, f_{reg}, f_{un}, f_{pow}, f_{wo}, g_{pair}\}$$ where $c_{inf}$ is a constant symbol, $f_{reg}, f_{un}, f_{pow},f_{wo}$ are each unary function symbols and $g_{pair}$ is a binary function symbol. Now the language $L$ we want consists of $L^-$ together with appropriate-arity function symbols $h_{sep}^\varphi$ and $h_{rep}^\varphi$ for each formula $\varphi$ in the usual language of set theory (you left Replacement out of your list of axioms, but I assume you want it there).

Now I'm going to build an $L$-theory, call it "ZFC'," which says (in addition to ZFC) that the additional function symbols we've added witness the corresponding ZFC axioms. This is basically partial Skolemization. E.g., amongst the axioms of ZFC', we'll have:

• $c_{inf}$ is $\omega$.

• $f_{pow}(a)$ is the powerset of $x$.

• $f_{wo}(a)$ is a well-ordering of $x$.

• $g_{pair}(a,b)=\{a,b\}$.

• For $\varphi(x, y, z)$ a formula of three variables, $h_{sep}^\varphi(a, b, c)=\{d\in a: \varphi(d, b, c)\}$.

And so on. Note that each of these is in fact expressible as an $L'$-sentence; in particular, since $\omega$ has a definition in the language $L$, we can use it as an abbreviation for that definition here.

Now the key facts are:

• ZFC' is computable.

• If $M\models$ ZFC,' then we can turn it into a model of ZFC of the kind you want (that is, "annotated" appropriately).

And now we're done, by invoking the PA degree.

---

Note that this trick is far more general than just applying to ZFC. In fact, for any computable theory $T$ and any PA degree ${\bf d}$, from ${\bf d}$ we can compute a model of $T$ together with its complete theory and all of its Skolem functions. The one change we need to make is that now we don't know what sentences we want to be true, so we need to use conditional Skolemization: e.g. for each formula $\psi(x, y)$ we add a function symbol $f_\psi$ and an axiom stating $$\forall x(\exists y(\psi(x, y))\implies \psi(x, f_\psi(x))).$$ We didn't need to do this in the ZFC case since the formulas we wanted to Skolemize were ones we wanted to hold everywhere.