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:
-
Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$.
-
Class Comprehension: $\exists x \forall y (y \in x \leftrightarrow \elm(y) \land\phi(y))$; where $x$ doesn't occur in formula $\phi(y)$.
-
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)]$. -
Foundation: $x \neq \emptyset \to \exists y \in x (y \cap x = \emptyset)$.
-
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?
Best Answer
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(ZFC)$. 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.