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


  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?

  • 1
    $\begingroup$ (Turning my misinterpretation into a comment): Note that if $W$ were a relation symbol, this theory would be quite weak - in particular, consistent relative to PA. Let $M$ be a nonstandard model of PA, $\alpha$ a nonstandard $Ackermann(M)$-ordinal, consider the the expansion of $(V_{\alpha+1})^{Ackermann(M)}$ by interpreting $W$ as the well-founded part of $Ackermann(M)$, and note that set comprehension follows from overspill. Having $W$ an actual object changes things: e.g. $W$ satisfies Infinity since it's the smallest adjunction-closed set. $\endgroup$ Jun 17, 2019 at 20:19
  • 2
    $\begingroup$ Have you proved that $W$ is a model of ZFC in your theory? Or do you believe you can prove this? $\endgroup$
    – Will Sawin
    Jun 17, 2019 at 20:53
  • 4
    $\begingroup$ If I'm not mistaken, you can construct a model of your theory from ZFC with an inaccessible. If $\kappa$ is inaccessible, you let the universe be $V_{\kappa+1}$ and let $W$ be $V_\alpha$ for $\alpha<\kappa$ such that any ordinal less than $\kappa$ definable in $V_{\kappa+1}$ with parameters from $V_\alpha$ is less than $\alpha$. (You can prove such an $\alpha$ exists using inaccessibility of $\kappa$.) $\endgroup$ Jun 17, 2019 at 22:24
  • 2
    $\begingroup$ These axioms are weird in that they imply the existence of many elements that are not sets (since $W$ needs to not be definable with parameters from $W$), but say very little about such elements. For instance, if you have any model and a class $C$ in the model which is not an element, it seems you can get a new model by just making $C$ an element: i.e., for every class $D$ that you had, add a new class $D\cup\{C\}$. (Although I suppose if $C$ is not definable with parameters from $W$, this might somehow mess up set comprehension.) $\endgroup$ Jun 18, 2019 at 2:54
  • 1
    $\begingroup$ @NajibIdrissi, to my trivial knowledge I've first presented here as a question. I don't know if it was on table before this attempt. I've presented before a similar axiomatization to FOM but with implication instead of the biconditional in set comprehension, and it was only the two schemas. $\endgroup$ Jun 18, 2019 at 14:15

2 Answers 2


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.


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.

  • 3
    $\begingroup$ This system interprets easily Ackermann's set theory, its easy to prove ackermann's reflection axiom. It is known that Ackermann interprets ZFC (Reinhardt). So it must interpret ZFC. $\endgroup$ Jun 18, 2019 at 14:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.