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

Note: $``W"$ is a primitive constant symbol.

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,..,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 $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?

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?

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

Note: $``W"$ is a primitive constant symbol.

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))$

3.Set Comprehension: $x_1,..,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 $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?

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

Note: $``W"$ is a primitive constant symbol.

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,..,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 $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?

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

Note: $``W"$ is a primitive constant symbol.

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(x))$

3.Set Comprehension: $x_1,..,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 $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?

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

Note: $``W"$ is a primitive constant symbol.

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))$

3.Set Comprehension: $x_1,..,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 $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?