Language: First order logic with identity and extra-logical primitives of membership $``\in"$, and $``W"$, the last is a constant symbol.
Axioms: ID axioms +
1.Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$
Define: $set(y) \iff \exists x (y \in x)$
2.Class comprehension: if $\varphi$ is a formula in which $x$ is not free, then all closures of:
$$\exists x \forall y (y \in x \leftrightarrow \varphi \wedge set(y))$$; are axioms.
3.Reflection: for n=0,1,2,3,...; if $\varphi$ is a formula in the pure language of set theory (i.e., doesn't use the symbol $``W"$), that has all of its free variables among symbols $``y,x_1,..,x_n"$; then:
$x_1,..,x_n \in W \to [\forall y (\varphi \to y \subseteq W) \to \forall y (\varphi \to y \in W)]$,
is an axiom.
4.Transitivity: $x \in W \to x \subset W$
/ Theory definition finished.
This axiomatic system is amongst the simplest ones proposed for set theory. It look even simpler than the axioms for ZFC.
Yet I think this theory is much stronger than ZFC.
What's the exact consistency strength of this system?
It would be tempting to add the following axiom:
- Limitation of size: $x \subset W \wedge |x| < |W| \to x \in W$.
I think this would further increase the strength of this theory.
Also a further note about this theory is that I think it doesn't really need Extensionality, i.e. this theory minus Extensionality can interpret it with Extensionality. Moreover, I think also that axiom of Transitivity, can be dispensed with, since we can interpret it over the class of all sets that are hereditarily elements of $W$. So what is really needed is only Class Comprehension and Reflection.