*In construction.*
$\text{ZFC}$, the usual first-order axiomatic set theory, can only
manipulate sets, and cannot formalize the notion of a proper class (e.g.
the class of all sets, $V$), so when one needs to manipulate proper
class objects, it is tempting to switch to a second-order logic form of
$\text{ZFC}$. However, because many useful theorems such as Gödel's
Completeness Theorem does not apply to second-order logic theories, it
is more convenient to use first-order two-sorted axiomatic theories with
two types of variables, one for sets and one for classes. Two such
"false" second-order theories, $\text{NBG}$ and $\text{MK}$, are the
most widely used extensions of $\text{ZFC}$.
Throughout this article, "*first-order (set theory) formula*" means a
formula in the language of $\text{ZFC}$, eventually with class
parameters, but only set quantifiers. "*second-order (set theory)
formula*" means a formula in the language of $\text{NBC}$ and
$\text{MK}$, i.e. it can contain class quantifiers.
**Von Neumann-Bernays-Gödel set theory** (commonly abbreviated as
*$\text{NBG}$* or *$\text{GCB}$*) is a conservative extension of
$\text{ZFC}$ - that is, it proves the same first-order sentences as
$\text{ZFC}$. It is equiconsistent with $\text{ZFC}$. However, unlike
$\text{ZFC}$ and $\text{MK}$, it is possible to finitely axiomatize
$\text{NBG}$. It was named after John von Neumann, Paul Bernays and
Kurt Gödel.
**Morse-Kelley set theory** (commonly abbreviated as *$\text{MK}$* or
*$\text{KM}$*) is an extension of $\text{NBG}$ which is stronger than
$\text{ZFC}$ and $\text{NBG}$ in consistency strength. It was named
after John L. Kelley and Anthony Morse. It only differs from
$\text{NBG}$ by a single axiom-schema. It is not finitely
axiomatizable.
It is possible to turn both theories into first-order axiomatic set
theories with only class variables, a class $X$ is called a set
(abbreviated $\text{M}X$) iff $\exists Y(X\in Y)$. One can also
define $\text{M}X\equiv X\in V$ with $V$ a symbol of the language
representing the universal class containing all sets. That is, a set is
a class member of another class.
## Axioms of $\text{NBG}$ and $\text{MK}$
We will be using capital letters to denote classes and lowercase letters
to denote sets. The following axioms are common to both $\text{NBG}$
and $\text{MK}$:
- **Extensionality:** two classes are equal iff they have the same
elements: $\forall X\forall Y(X=Y\iff\forall z(z\in X\iff
z\in Y))$.
- **Regularity:** every class is disjoint from one of its elements:
$\forall X(\exists a(a\in X)\implies\exists x(x\in
X\land\forall y(y\in x\implies y\not\in X)))$.
- **Infinity:** there exists an infinite set. For example, $\exists
x(\exists a(a\in x)\land\forall y(y\in x\implies\exists
z(y\in z\land z\in x))$.
- **Union:** the union of the elements of a set is a set : $\forall
x\exists y\forall z(z\in y\iff\exists w(z\in w\land w\in
x))$.
- **Pairing:** the pair of two sets is itself a set: $\forall
x\forall y\exists z\forall w(w\in z\iff(w=x\lor w=y))$.
- **Powerset:** the powerset of a set is a set: $\forall x\exists
y\forall z(z\in y\iff\forall w(w\in z\implies w\in x))$.
- **Limitation of Size:** a class $X$ is proper if and only if there
is bijection between $X$ and the universal class $V$.
The axiom of limitation of size implies the axiom of global choice
("there is a well-ordering of the universe") and $\text{ZFC}