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.)