If we add to the language of ZFC class symbols, denoted using letter style $“\mathcal X, \mathcal Q, \mathcal R, \mathcal P, \mathcal L,.."$, call it class style, then add the axiom schema of class comprehension: $$\exists \mathcal X \forall \mathcal Y \ [\mathcal Y \in \mathcal X \leftrightarrow \exists y=\mathcal Y :\phi(y)]$$,
Where $\phi(y)$ is any formula in which $y$ only occur free and in which $\mathcal X$ doesn't occur.
Add all axioms of ZFC written in non-class style.
Add the axiom of sorting: $$\forall x \exists \mathcal Y (x= \mathcal Y)$$
Add the axiom of membership: $$\forall x \forall \mathcal Y (\mathcal Y \in x \to \exists y (y=\mathcal Y))$$
Call the resulting theory "ZFC + classes".
Notice that ZFC + classes is different from NBG\MK where every member of a class is a set, here only members of sets are sets, so you can have proper classes (i.e. non-sets) that are members of proper classes.
Is ZFC + classes equi-interpretable with MK?
If instead of adding ZFC axioms in non-class style only, we add all homogeneously written axioms of ZFC.
Where in a homogeneous expression either all terms are written in non-class style or all terms are written in class style.
Call the resulting theory ZFC+$classes_2$
Is ZFC+$classes_2$ consistent?
If consistent, then what's its consistency strength?
To be noticed is that if ZFC+$classes_2$ is not stronger than ZFC, then it would be a candidate theory for foundation of mathematics according to Muller's criteria!
Best Answer
ZFC+𝑐𝑙𝑎𝑠𝑠𝑒𝑠2 is equiconsistent with ZFC. Let LZFC be the theory obtained from ZFC by adding a constant symbol 𝛼, an axiom asserting that 𝛼 is an ordinal, and for every formula F of ZF with parameters from 𝑉𝛼 an axiom asserting that F holds in 𝑉𝛼 iff F holds. By reflection one can see that LZFC is a conservative extension of ZFC. If we interpret set as an element of 𝑉𝛼, and everything as a class, then all the axioms of ZFC+𝑐𝑙𝑎𝑠𝑠𝑒𝑠2 hold.