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

  • 7
    $\begingroup$ A PA-degree computes a Henkin completion of ZFC, i.e., a model of ZFC along with its satifaction predicate. So, it computes all definable relations in the model, which also implies it computes any (multi)function definable in the model. This includes all the listed properties. $\endgroup$ – Emil Jeřábek Jul 16 '17 at 21:48
  • 5
    $\begingroup$ Although Emil has answered the question, I'm wondering about one aspect of the question, namely the idea that replacement is somehow easier than specification. "Hard coding constants" looks reasonable for the axiom of infinity, since it asserts the existence of a single set with some properties, but I don't see how it would work for replacement (and not for specification). $\endgroup$ – Andreas Blass Jul 16 '17 at 21:54
  • $\begingroup$ @AndreasBlass each individual axiom of replacement asserts the existence of only one set. Each set has a specific code, so each individual axiom is computable. (Oh wait, nvm, it quantifies over the domain, I'll fix that later.) $\endgroup$ – PyRulez Jul 17 '17 at 2:31
  • 2
    $\begingroup$ I'm not sure it can compute the BB function as such, but it can compute the function that the model thinks is the BB function. (Note that the model has nonstandard integers.) $\endgroup$ – Emil Jeřábek Jul 17 '17 at 12:56
  • 1
    $\begingroup$ @EmilJeřábek It definitely can't compute BB as such, since BB is equivalent to $0'$ and there are PA degrees not computing $0'$ (e.g. low PA degrees). $\endgroup$ – Noah Schweber Sep 6 '17 at 13:18

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.


Your Answer

