 Morse–Kelley set theory

In the foundation of mathematics, Morse–Kelley set theory (MK) or Kelley–Morse set theory (KM) 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.
Morse–Kelley set theory is named after mathematicians John L. Kelley and Anthony Morse and was first set out in an appendix to Kelley's text book General Topology (1955), a graduate level introduction to topology. Kelley himself referred to it as Skolem–Morse set theory, after Thoralf Skolem. 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.
Contents
MK axioms and ontology
NBG and MK share a common ontology. The universe of discourse consists of classes. Classes which are members of other classes are called sets. A class which 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 onesorted theory, this notational convention is only mnemonic;
 The monadic predicate whose intended reading is "'the class x is a set," abbreviates
 The empty set is defined by
 The class V, the universal class having all possible sets as members, is defined by V is also the Von Neumann universe.
Extensionality: Classes having the same members are the same class.
 Note that a set and a class having the same extension are identical. Hence MK is not a twosorted theory, appearances to the contrary notwithstanding.
Foundation: Each nonempty class A is disjoint from at least one of its members.
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 which 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 whose members are exactly those sets x such that ϕ(x) comes out true. Formally, if Y is not free in φ:
Pairing: For any sets x and y, there exists a set z = {x,y} whose members are exactly x and y.
 Pairing licenses the unordered pair in terms of which the ordered pair, , may be defined in the usual way, as . 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 onetoone 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.
Power set: Let p be a class whose members are all possible subsets of the set a. Then p is a set.
Union: Let be the sum class of the set a, namely the union of all members of a. Then s is a set.
Infinity: There exists an inductive set y, meaning that (i) the empty set is a member of y; (ii) if x is a member of y, then so is .
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:
 ZFC and NBG: Pairing, Power Set, Union, Infinity;
 NBG (and ZFC, if quantified variables were restricted to sets): Extensionality, Foundation;
 NBG: Limitation of Size;
 ML: Extensionality, Class Comprehension (in NF, comprehension is restricted to stratified formulas).
Discussion
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 we expect 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 wellknown set theory with proper classes. In fact, NBG—and hence ZFC—can be proved consistent if MK is. MK's strength stems from its axiom schema of Class Comprehension being impredicative, meaning that φ(x) may contain quantified variables ranging over classes. The quantified variables in NBG's axiom schema of Class Comprehension are restricted to sets; hence Class Comprehension in NBG must be predicative. (Separation with respect to sets is still impredicative in NBG, because the quantifiers in φ(x) may range over all sets.) 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 ordinals.
The only advantage of the axiom of limitation of size is that it implies the axiom of global choice. Limitation of Size does not appear in Rubin (1967), Monk (1980), or Mendelson (1997). Instead, these authors invoke a usual form of the local axiom of choice, and an "axiom of replacement,"^{[1]} asserting that if the domain of a class function is a set, its range is also a set. Replacement can prove everything that Limitation of Size proves, except prove some form of the axiom of choice.
Limitation of Size plus I being a set (hence the universe is nonempty) renders provable the sethood of the empty set; hence no need for an axiom of empty set. Such an axiom could be added, of course, and minor perturbations of the above axioms would necessitate this addition. The set I is not identified with the limit ordinal ω, as I could be a set larger than ω. In this case, the existence of ω would follow from either form of Limitation of Size.
The class of von Neumann ordinals can be wellordered. It cannot be a set (under pain of paradox); hence that class is a proper class, and all proper classes have the same size as V. Hence V too can be wellordered.
MK can be confused with secondorder ZFC, ZFC with secondorder logic (representing secondorder objects in set rather than predicate language) as its background logic. The language of secondorder 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). But the semantics of secondorder ZFC are quite different from those of MK. For example, if MK is consistent then it has a countable firstorder model, while secondorder ZFC has no countable models.
Model theory
ZFC, NBG, and MK each have models describable in terms of V, the standard model of ZFC and the von Neumann universe. Let the inaccessible cardinal κ be a member of V. Also let Def(X) denote the Δ_{0} definable subsets of X (see constructible universe). Then:
 V_{κ} is an intended model of ZFC;
 Def(V_{κ}) is an intended model of NBG;
 V_{κ+1}, the power set of V_{κ}, is an intended model of MK.
History
MK was first set out 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.^{[2]} Impredicative class comprehension was also proposed in Mostowski (1951) and Lewis (1991).
The axioms in Kelley's General topology
The axioms and definitions in this section are, but for a few inessential details, taken from the appendix to Kelley (1955). The explanatory remarks below are not his. 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. Kelley introduced his axioms gradually, as needed to develop the topics listed after each instance of Develop below.
Notations appearing below and now wellknown are not defined. Peculiarities of Kelley's notation include:
 He did not distinguish variables ranging over classes from those ranging over sets;
 domain f and range f denote the domain and range of the function f; this peculiarity has been carefully respected below;
 His primitive logical language includes class abstracts of the form "the class of all sets x satisfying A(x)."
Definition: x is a set [and hence not a proper class] if, for some y, .
I. Extent: For each x and each y, x=y if and only if for each z, when and only whenI is a variant of the axiom of extensionality, except that its scope includes proper classes as well as sets.
II. Classification (schema): An axiom results if in
 For each β, if and only if β is a set and B,
'α' and 'β' are replaced by variables, ' A ' by a formula Æ, and ' B ' by the formula obtained from Æ by replacing each occurrence of the variable which replaced α by the variable which replaced β.
Develop: Algebra of sets. Existence of the null class and the universal class V.
III. Subsets: If x is a set, there exists a set y such that for each z, if , thenDevelop: V is not a set. Existence of singletons. Separation provable. Proof sketch of Power Set: for any class z which is a subclass of the set x, the class z is a member of the set y whose existence III asserts. Hence z is a set.
IV. Union: If x and y are both sets, then is a set.The import of IV is that of Pairing above, whose proof sketch goes as follows. The singleton {x} of a set x is a set because it is a subclass of the power set of x (by two applications of III). Then IV implies that {x,y} is a set if x and y are sets.
Develop: Unordered and ordered pairs, relations, functions, domain, range, function composition.
V. Substitution: If f is a [class] function and domain f is a set, then range f is a set.The import of V is that of the "axiom of replacement" appearing in textbook treatments of NBG and MK.
VI. Amalgamation: If x is a set, then is a set.
The import of VI is that of Union above. V and VI may be combined into one axiom.^{[3]}
Develop: Cartesian product, injection, surjection, bijection, order theory.
VII. Regularity: If there is a member y of x such that
The import of VII is that of Foundation above.
Develop: Ordinal numbers, transfinite induction.
VIII. Infinity: There exists a set y, such that and whenever
VIII asserts the unconditional existence of two sets, the infinite inductive set y, and the null set is a set simply because it is a member of y. Up to this point, evertyhing that has been proved to exist is a class, and Kelley's discussion of sets was entirely hypothetical.
Develop: Natural numbers, N is a set, Peano axioms, integers, rational numbers, real numbers.
Definition: c is a choice function if c is a function and for each member x of domain c.IX. Choice: There exists a choice function c whose domain is .
IX is very similar to the axiom of global choice derivable from Limitation of Size.
Develop: Equivalents of the axiom of choice. As is the case with ZFC, the cardinal numbers require some form of this axiom.
Notes
 ^ See, e.g., Mendelson (1997), p. 239, axiom R.
 ^ The locus citandum for ML is the 1951 ed. of Quine's Mathematical Logic. However, the summary of ML given in Mendelson (1997), p. 296, is easier to follow. Mendelson's axiom schema ML2 is identical to the above axiom schema of Class Comprehension.
 ^ Kelley (1955), p. 261, fn †.
References
 John L. Kelley 1975 (1955) General Topology. Springer. Earlier ed., Van Nostrand. Appendix, "Elementary Set Theory."
 Lemmon, E. J. (1986) Introduction to Axiomatic Set Theory. Routledge & Kegan Paul.
 David K. Lewis (1991) Parts of Classes. Oxford: Basil Blackwell.
 Mendelson, Elliott (1997). Introduction to Mathematical Logic. Chapman & Hall. ISBN 0534066240. The definitive treatment of the closely related set theory NBG, followed by a page on MK. Harder than Monk or Rubin.
 Monk, J. Donald (1980) Introduction to Set Theory. Krieger. Easier and less thorough than Rubin.
 Morse, A. P., (1965) A Theory of Sets. Academic Press.
 Mostowski, Andrzej (1950) "Some impredicative definitions in the axiomatic set theory," Fundamenta Mathematicae 37: 11124.
 Rubin, Jean E. (1967) Set Theory for the Mathematician. San Francisco: Holden Day. More thorough than Monk; the ontology includes urelements.
External links
From Foundations of Mathematics (FOM) discussion group:
Categories: Systems of set theory
Wikimedia Foundation. 2010.