Morse–Kelley set theory

In the foundations of mathematics, Morse–Kelley set theory (MK), Kelley–Morse set theory (KM), Morse–Tarski set theory (MT), Quine–Morse set theory (QM) or the system of Quine and Morse is a first-order axiomatic set theory that is closely related to von Neumann–Bernays–Gödel set theory (NBG). While von Neumann–Bernays–Gödel set theory restricts the bound variables in the schematic formula appearing in the axiom schema of Class Comprehension to range over sets alone, Morse–Kelley set theory allows these bound variables to range over proper classes as well as sets, as first suggested by Quine in 1940 for his system ML.

Morse–Kelley set theory is named after mathematicians John L. Kelley and Anthony Morse and was first set out by and later in an appendix to Kelley's textbook ''General Topology'' (1955), a graduate level introduction to topology. Kelley said the system in his book was a variant of the systems due to Thoralf Skolem and Morse. Morse's own version appeared later in his book ''A Theory of Sets'' (1965).

While von Neumann–Bernays–Gödel set theory is a conservative extension of Zermelo–Fraenkel set theory (ZFC, the canonical set theory) in the sense that a statement in the language of ZFC is provable in NBG if and only if it is provable in ZFC, Morse–Kelley set theory is a proper extension of ZFC. Unlike von Neumann–Bernays–Gödel set theory, where the axiom schema of Class Comprehension can be replaced with finitely many of its instances, Morse–Kelley set theory cannot be finitely axiomatized.

MK axioms and ontology

NBG and MK share a common ontology. The universe of discourse consists of classes. Classes that are members of other classes are called sets. A class that is not a set is a proper class. The primitive atomic sentences involve membership or equality.

With the exception of Class Comprehension, the following axioms are the same as those for NBG, inessential details aside. The symbolic versions of the axioms employ the following notational devices:
* The upper case letters other than ''M'', appearing in Extensionality, Class Comprehension, and Foundation, denote variables ranging over classes. A lower case letter denotes a variable that cannot be a proper class, because it appears to the left of an ∈. As MK is a one-sorted theory, this notational convention is only mnemonic.
* The monadic predicate $Mx,$ whose intended reading is "the class ''x'' is a set", abbreviates $\exists W(x \in W).$
* The empty set $\varnothing$ is defined by $\forall x (x \not \in \varnothing).$
* The class ''V'', the universal class having all possible sets as members, is defined by $\forall x (Mx \to x \in V).$ ''V'' is also the von Neumann universe.

Extensionality: Classes having the same members are the same class.
:$\forall X \, \forall Y \, ( \forall z \, (z \in X \leftrightarrow z \in Y) \rightarrow X = Y).$
A set and a class having the same extension are identical. Hence MK is not a two-sorted theory, appearances to the contrary notwithstanding.

Foundation: Each nonempty class ''A'' is disjoint from at least one of its members.
:\forall A \not = \varnothing \rightarrow \exists b (b \in A \land \forall c (c \in b \rightarrow c \not\in A))

Class Comprehension: Let φ(''x'') be any formula in the language of MK in which ''x'' is a free variable and ''Y'' is not free. φ(''x'') may contain parameters that are either sets or proper classes. More consequentially, the quantified variables in φ(''x'') may range over all classes and not just over all sets; ''this is the only way MK differs from NBG''. Then there exists a class $Y=\$ whose members are exactly those sets ''x'' such that $\phi(x)$ comes out true. Formally, if ''Y'' is not free in φ:
:\forall W_1 ... W_n \exists Y \forall x \in Y \leftrightarrow (\phi(x, W_1, ... W_n) \land Mx)

Pairing: For any sets ''x'' and ''y'', there exists a set $z=\$ whose members are exactly ''x'' and ''y''.
:\forall x \, \forall y \, (Mx \land My) \rightarrow \exists z \, (Mz \land \forall s \, [ s \in z \leftrightarrow (s = x \, \lor \, s = y)">s \in z \leftrightarrow (s = x \, \lor \, s = y)">(Mx \land My) \rightarrow \exists z \, (Mz \land \forall s \, [ s \in z \leftrightarrow (s = x \, \lor \, s = y)

Pairing licenses the unordered pair in terms of which the ordered pair, $\langle x,y \rangle$, may be defined in the usual way, as $\ \$. With ordered pairs in hand, Class Comprehension enables defining relations and function (set theory), functions on sets as sets of ordered pairs, making possible the next axiom:

Axiom of limitation of size, Limitation of Size: ''C'' is a proper class if and only if '' V'' can be mapped one-to-one into ''C''.
:\begin
\forall C lnot MC \leftrightarrow \exists F ( \forall x [Mx \rightarrow \exists s (s \in C \land \langle x, s \rangle \in F)\land \\
\qquad \forall x \forall y \forall s [(\langle x, s \rangle \in F \land \langle y, s \rangle \in F) \rightarrow x = y])].
\end

The formal version of this axiom resembles the axiom schema of replacement, and embodies the class function ''F''. The next section explains how Limitation of Size is stronger than the usual forms of the axiom of choice.

Power set: Let ''p'' be a class whose members are all possible subsets of the set ''a''. Then ''p'' is a set.
:\forall a \, \forall p \, Ma \land \forall x \, \in p \leftrightarrow \forall y \, (y \in x \rightarrow y \in a)">Ma \land \forall x \, Union: Let $s=\bigcup a$ be the sum class of the set ''a'', namely the union of all members of ''a''. Then ''s'' is a set.
:$\forall a \, \forall s \, [(Ma \land \forall x \, [x \in s \leftrightarrow \exists y \, (x \in y \land y \in a)">union (set theory)">union$ of all members of ''a''. Then ''s'' is a set.
:\forall a \, \forall s \, Ma \land \forall x \, [x \in s \leftrightarrow \exists y \, (x \in y \land y \in a) \rightarrow Ms

axiom of infinity">Infinity