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.

(Turning my misinterpretation into a comment): Note that if $W$ were arelationsymbol, 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$ – Noah Schweber Jun 17 '19 at 20:1917more comments