Morse–Kelley set theory is named after mathematicians John L. Kelley and Anthony Morse and was first set out by Wang (1949) and later in an appendix to Kelley's textbook General Topology (1955), a graduate level introduction to topology.
Morse's own version appeared later in his book A Theory of Sets (1965).
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.
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.
Hence MK is not a two-sorted theory, appearances to the contrary notwithstanding.
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.
With ordered pairs in hand, Class Comprehension enables defining relations and functions on sets as sets of ordered pairs, making possible the next axiom: Limitation of Size: C is a proper class if and only if V can be mapped one-to-one into C. 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.
Note that p and s in Power Set and Union are universally, not existentially, quantified, as Class Comprehension suffices to establish the existence of p and s. Power Set and Union only serve to establish that p and s cannot be proper classes.
The above axioms are shared with other set theories as follows: Monk (1980) and Rubin (1967) are set theory texts built around MK; Rubin's ontology includes urelements.
These authors and Mendelson (1997: 287) submit that MK does what is expected of a set theory while being less cumbersome than ZFC and NBG.
MK is strictly stronger than ZFC and its conservative extension NBG, the other well-known set theory with proper classes.
That means that if MK's axioms hold, one can define a True predicate and show that all the ZFC and NBG axioms are true—hence every other statement formulated in ZFC or NBG is true, because truth is preserved by logic.
The NBG axiom schema of Class Comprehension can be replaced with finitely many of its instances; this is not possible in MK.
MK is consistent relative to ZFC augmented by an axiom asserting the existence of strongly inaccessible cardinals.
Instead, these authors invoke a usual form of the local axiom of choice, and an "axiom of replacement,"[2] asserting that if the domain of a class function is a set, its range is also a set.
The language of second-order ZFC is similar to that of MK (although a set and a class having the same extension can no longer be identified), and their syntactical resources for practical proof are almost identical (and are identical if MK includes the strong form of Limitation of Size).
Let the inaccessible cardinal κ be a member of V. Also let Def(X) denote the Δ0 definable subsets of X (see constructible universe).
Then: MK was first set out in Wang (1949) and popularized in an appendix to J. L. Kelley's (1955) General Topology, using the axioms given in the next section.
The system of Anthony Morse's (1965) A Theory of Sets is equivalent to Kelley's, but formulated in an idiosyncratic formal language rather than, as is done here, in standard first-order logic.
The first set theory to include impredicative class comprehension was Quine's ML, that built on New Foundations rather than on ZFC.
The axioms and definitions in this section are, but for a few inessential details, taken from the Appendix to Kelley (1955).
The Appendix states 181 theorems and definitions, and warrants careful reading as an abbreviated exposition of axiomatic set theory by a working mathematician of the first rank.
Peculiarities of Kelley's notation include: Definition: x is a set (and hence not a proper class) if, for some y,
I would be identical to the axiom of extensionality in ZFC, except that the scope of I includes proper classes as well as sets.
[4] Develop: Cartesian product, injection, surjection, bijection, order theory.
Up to this point, everything that has been proved to exist is a class, and Kelley's discussion of sets was entirely hypothetical.
IX is very similar to the axiom of global choice derivable from Limitation of Size above.
As is the case with ZFC, the development of the cardinal numbers requires some form of choice.
Hence the Kelley treatment of MK makes very clear that all that distinguishes MK from ZFC are variables ranging over proper classes as well as sets, and the Classification schema.