What's the exact consistency strength of this axiom system for classes and sets?

Question

Notation: Let $\phi$ be any formula in $\mathsf{FOL}({=},{\in}, W)$; let $\varphi$ be any formula in $\mathsf{FOL}({=},{\in})$ having $x$ free, and whose parameters are among $x_1,\dotsc,x_n$.

Note: “$W$” is a primitive constant symbol.

$\DeclareMathOperator\elm{elm}$Define: $\elm(y)\iff \exists z (y \in z)$, where “$\elm$” is short for “… is an element”.

Axioms:

1. Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$.

2. Class Comprehension: $\exists x \forall y (y \in x \leftrightarrow \elm(y) \land\phi(y))$; where $x$ doesn't occur in formula $\phi(y)$.

3. Set Comprehension: $x_1,\dotsc,x_n \in W \to \\ [ \forall x (\varphi(x) \to x \subseteq W) \leftrightarrow \forall x (\varphi(x) \to x \in W)]$.

4. Foundation: $x \neq \emptyset \to \exists y \in x (y \cap x = \emptyset)$.

5. Choice over all classes.

The basic two axioms of this theory are the two comprehension schemes, all the rest of axioms are indeed interpretable from them. $W$ stands for the class of all sets, that's why the predicate $\elm$ is used here instead of the usual denotation of it as $\operatorname{set}$ in Morse–Kelley class theory.

In my opinion, this kind of axiomatization is ideal, I think it's one of the most elegant ones. There is no substantial dispute over axioms 1 and 4. Schema 2 is the most natural principle about classes. Schema 3 technically sums up all of what's in standard set theory in a neat manner. Axiom 5 is a stretch of choice to all classes, which is done in versions of Morse–Kelley and NBG, so it's encountered in systems that are considered fairly standard about classes and sets. All axioms are clean and fairly natural.

Question: What's the exact consistency strength of this theory?

Answer 1

In regards to your comments, if you have two infinite theories $T$ and $T'$, if $T'$ consists of $T$ plus the schema $M\vDash T$ for some constant $M$, without alternate assumptions (Such as the existence of a truth predicate) $T'\nvdash Con(T)$. This is why $ZFC+V_\kappa\prec V\nvdash V_\kappa\vDash ZFC$.

As for your actual theory, if $M\vDash ZFC$, then there is some $(N,V_\kappa^N)$ such that $V_\kappa^N\prec N$. I claim for any formula $\phi(x_0...x_n)\leftrightarrow\phi^{N_0}(x_0...x_n)$, where $N_0=\text{def}(N)$, if $\{(x_0...x_n)|\phi(x_0...x_n)\}\subseteq V_\kappa^N$, then $\{(x_0...x_n)|\phi(x_0...x_n)\}\in V_\kappa^N$ and $\{(x_0...x_n)|\phi(x_0...x_n)\}$ is definable in $V_\kappa^N$, the only tricky case being the existential quantifier.

Note that $\{(x_0...x_n)|\exists x(\phi(x,x_0...x_n))\}=\text{ran}(\{(x,x_0...x_n)|\phi(x,x_0...x_n)\})$. Now if $\{(x,x_0...x_n)|\phi(x,x_0...x_n)\})$ is definable in $V_\kappa^N$, then $\text{ran}(\{(x,x_0...x_n)|\phi(x,x_0...x_n)\})\in V_\kappa^N$. Furthermore, $\{(x_0...x_n)|\exists x(\phi(x,x_0...x_n))\}$ is definable as $\text{ran}\{(x_0...x_n)|\phi(x,x_0...x_n)\}$. The rest is trivial.

Answer 2

I tried to check that, for each axiom of ZFC, your theory proves that the set $W$ with the relation $\in$ satisfies each axiom of ZFC. This implies the consistency strength of your theory is at least the consistency strength of ZFC.

I succeeded for every axiom, but failed for the axiom of replacement. My successful arguments should be helpful for attempts to lower bound the consistency strength, and my failed one might be helpful for attempts to upper bound it.

---

First lets prove some lemmas:

A. $ (x \in W) \rightarrow (x \subseteq W)$. This follows from axiom 3, taking $\varphi$ to be $(x=x_1)$, getting $(x \in W) \implies ( (x \subseteq W) \leftrightarrow (x\in W))$ which is equivalent.

B. $((x_1 \in W) \land (x \subseteq x_1)) \rightarrow (x_1 \in W)$. This follows from axiom 3, taking $\varphi$ to be $(x_1 \subseteq x)$.

Now using axiom 1 and lemma A, $(W, \in)$ satisfies the axiom of extensionality.

Using axiom 4 and lemma A, $(W, \in)$ satisfies the axiom of foundation.

Now the axiom schema of specification, axiom of pairing, axiom of union, and axiom of power set we prove by essentially the same strategy. They all imply that a set satisfying some conditions (depending on some free variables) must exist. To prove these, we must first use axiom 2 to show that the class exists, then axiom 3 to prove it is an element of $W$. In particular, we can use axiom 3 in the form that if the predicate $\varphi$ defines a unique $x$, then that $x$ is a subset of $W$ if and only if it is an element of $W$.

For the axiom scheme of specification, in the first step we use that elements of a fixed set $z$ must be elements, and the second step we use lemma B.

For the axiom of pairing, we use that if $x_1$ and $x_2$ are in $W$, then $x_1$ and $x_2$ are elements, so $\{x_1,x_2\}$ is class, and then $\{x_1,x_2\} \in W$ by applying axiom 3 to the predicate $x =\{x_1,x_2\}$.

For the axiom of union, we use that if $w \in y$ and $y \in \mathcal x_1$ then $w$ is an element, so $\{ w | \exists y : w \in y \land y\in x_1\}$ is class. Then we apply axiom 3 to the predicate $x =\{ w | \exists y : w \in y \land y\in x_1\}$, using two applications of lemma A to verify the hypothesis.

For the axiom of power set, we use lemma B to verify that every subset of $x_1$ is an element of $W$ and hence is an element, so the power set of $x_1$ is a class, and then lemma A to verify that this is a subset of $W$ and thus to be able to apply axiom 3.

For the axiom of infinity, following Noah Schweber's suggestion, we first observe that the empty set is contained in $W$ and, for all $y$ in $W$, the successor of $y$ is in $W$, by applying axiom 3. We then note that the set of $z$ such that $z$ is contained in all classes containing the empty set and closed under succession exists by property 2, since all such $z$ are elements. Finally this set is contained in $W$, because it is uniquely defined and only a subset of $W$.

The argument for the axiom of choice is similar, except that given a set $x_1$ of sets, we must use axiom 5 to construct a choice function, and then apply axiom 3 to the predicate `` $x$ is a choice function of $x_1$" which from lemma A and the axiom of pairing (to construct ordered pairs) satisfies the hypothesis.

---

For the axiom scheme of replacement, we start with a predicate $\phi$ and assume we have a set $A \in W$ such that for all $x \in A$, there is a unique $y \in W$ satisfying $\phi$. We can then define the class consisting of all $y \in W$ that satisfy $\phi$ for some $x \in A$, using class comprehension. However, this definition requires the symbol $W$ - if we drop it, $\phi$ might no longer be a function, and the image of $\phi$ might contain elements that don't lie in $W$ - so I don't see how to get the axiom of replacement.

However, there should be no problem with using the axiom of replacement to construct ordinals, as we can always take a function that produces the smallest ordinal satisfying some condition, so maybe there is a way around this.