Morse–Kelley set theory 2693655 215275442 2008-05-27T14:00:42Z Michael Hardy 4626 Changed to \varnothing. To me \emptyset looks like a character that you use because your typewrite has the zero and the slash and no special characters. In the [[foundation of mathematics]], '''Kelley–Morse (KM)''' or '''Morse–Kelley (MK) set theory''' is a [[first order logic|first order]] [[axiomatic set theory]] that is closely related to [[Von Neumann–Bernays–Gödel set theory]] (NBG). MK allows the [[bound variable]]s in the schematic formula appearing in the axiom schema of Class Comprehension to range over [[proper class]]es as well as sets. [[Von Neumann–Bernays–Gödel set theory|NBG]] restricts these bound variables to sets alone. MK is a [[proper extension]] of the canonical set theory [[Zermelo–Fraenkel set theory|ZFC]] and cannot be finitely axiomatized. NBG is a [[conservative extension]] of ZFC, and can be finitely axiomatized. == MK axioms and ontology == [[Von Neumann–Bernays–Gödel set theory|NBG]] and MK share a common [[ontology]]. The [[universe of discourse]] consists of [[proper class|classes]]. Classes which are members of other classes are called [[set]]s. A class which is not a set is a [[proper class]]. The primitive [[atomic sentence]]s involve membership or equality. With the exception of Class Comprehension, the following axioms are the same as those for [[Von Neumann–Bernays–Gödel set theory|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 &isin;. As MK is a one-sorted theory, this notational convention is only [[mnemonic]]; *The [[relation (mathematics)|monadic predicate]] <math>\ Mx,</math> whose intended reading is "'the class ''x'' is a set," abbreviates <math>\exist W(x \in W);</math> *The [[empty set]] <math>\varnothing</math> is defined by <math>\forall x (x \not \in \varnothing);</math> *The class ''V'', the [[universal class]] having all possible sets as members, is defined by <math>\forall x (x \in V).</math> ''V'' is also the [[Von Neumann universe]]. '''[[Axiom of extensionality|Extensionality]]:''' Classes having the same members are the same class. :<math>\forall X \, \forall Y \, ( \forall z \, (z \in X \leftrightarrow z \in Y) \rightarrow X = Y).</math> : Note that a set and a class having the same extension are identical. Hence MK is not a two-sorted theory, appearances to the contrary notwithstanding. '''[[Axiom of foundation|Foundation]]:''' Each nonempty class ''A'' is [[disjoint sets|disjoint]] from at least one of its members. :<math>\forall A [A \not = \varnothing \rightarrow \exist b (b \in A \and \forall c (c \in b \rightarrow c \not\in A))].</math> '''Class Comprehension:''' Let &phi;(''x'') be any formula in the language of MK in which ''x'' is a [[free variable]] and ''Y'' is not free. &phi;(''x'') may contain parameters which are either sets or proper classes. More consequentially, the quantified variables in &phi;(''x'') may range over all classes and not just over all sets; ''this is the only way MK differs from [[Von Neumann–Bernays–Gödel set theory|NBG]]''. Then there exists a '''class''' <math>Y=\{x \mid \phi(x)\}</math> whose members are exactly those '''sets''' ''x'' such that <math>\phi(x)</math> comes out true. Formally, if ''Y'' is not free in &phi;: :<math>\forall W_1 ... W_n \exist Y \forall x [x \in Y \leftrightarrow (\phi(x, W_1, ... W_n) \and Mx)].</math> '''[[Axiom of pairing|Pairing]]:''' For any sets ''x'' and ''y'', there exists a set <math>z=\{x,y\}</math> whose members are exactly ''x'' and ''y''. :<math>\forall x \, \forall y \, [ (Mx \and My) \rightarrow \exist z \, (Mz \and \forall s \, [ s \in z \leftrightarrow (s = x \, \or \, s = y)])].</math> :Pairing licenses the unordered pair in terms of which the [[ordered pair]], <math>\langle x,y \rangle</math>, may be defined in the usual way, as <math>\ \{\{x\},\{x,y\}\}</math>. With ordered pairs in hand, Class Comprehension enables defining [[relation (mathematics)|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 ''[[Von Neumann universe|V]]'' can be [[one-to-one mapping|mapped one-to-one]] into ''C''. :<math>\forall C [\lnot MC \leftrightarrow \exist F ( \forall x [Mx \rightarrow \exist s (s \in C \and \langle x, s \rangle \in F)] \and </math> ::<math>\forall x \forall y \forall s [(\langle x, s \rangle \in F \and \langle y, s \rangle \in F) \rightarrow x = y])].</math> :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]]. '''[[Axiom of power set|Power set]]:''' Let ''p'' be a class whose members are all possible [[subset]]s of the set ''a''. Then ''p'' is a set. :<math>\forall a \, \forall p \, [(Ma \and \forall x \, [x \in p \leftrightarrow \forall y \, (y \in x \rightarrow y \in a)]) \rightarrow Mp].</math> '''[[Axiom of union|Union]]:''' Let <math>s=\bigcup a</math> be the sum class of the set ''a'', namely the [[union (set theory)|union]] of all members of ''a''. Then ''s'' is a set. :<math>\forall a \, \forall s \, [(Ma \and \forall x \, [x \in s \leftrightarrow \exist y \, (x \in y \and y \in a)]) \rightarrow Ms].</math> '''[[axiom of infinity|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 <math>x \cup \{x\}.</math>. :<math>\exist y[My \and \varnothing \in y \and \forall z(z \in y \rightarrow \exist x [x \in y \and \forall w (w \in x \leftrightarrow [w = z \or w \in z])] )].</math> 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: * [[Zermelo–Fraenkel set theory|ZFC]] and [[Von Neumann–Bernays–Gödel set theory|NBG]]: Pairing, Power Set, Union, Infinity; * [[Von Neumann–Bernays–Gödel set theory|NBG]] (and ZFC, if quantified variables were restricted to sets): Extensionality, Foundation; * [[Von Neumann–Bernays–Gödel set theory|NBG]]: Limitation of Size; * [[New Foundations|ML]]: Extensionality, Class Comprehension (in [[New Foundations|NF]], comprehension is restricted to stratified formulas). <!-- The above axioms feature six [[existential quantifier]]s over sets and one over classes. By contrast, a nonredundant axiomatization of ZFC requires at least 11 existential quantifiers over sets. NBG with Class Comprehension calls into being two sets, one for each of Power Set and Union, in addition to the 6 MK calls into being. The finite axiomatization of NBG calls at least 7 classes into being. --> == Discussion == Monk (1980) and Rubin (1967) are set theory texts built around MK; Rubin's [[ontology]] includes [[urelement]]s. These authors and Mendelson (1997: 287) submit that MK does what we expect of a set theory while being less cumbersome than [[Zermelo–Fraenkel set theory|ZFC]] and [[Von Neumann–Bernays–Gödel set theory|NBG]]. MK is strictly stronger than ZFC and its [[conservative extension]] NBG, the other well-known set theory with [[proper class]]es. In fact, NGB—and hence ZFC—can be proved consistent if MK is. MK's strength stems from its axiom schema of Class Comprehension being [[impredicativity|impredicative]], meaning that &phi;(''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 [[impredicativity|predicative]]. (Separation with respect to sets is still impredicative in NBG, because the quantifiers in &phi;(''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 cardinal|inaccessible ordinal]]s. 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,"<ref>See, e.g., Mendelson (1997), p. 239, axiom R.</ref> asserting that if the domain of class function is a set, its range is also a set. Replacement can do prove everything that Limitation of Size proves, except prove some form of the [[axiom of choice]]. [[axiom of limitation of size|Limitation of Size]] plus [[axiom of infinity|''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]] <math>\omega,</math> as ''I'' could be a set larger than <math>\omega.</math> In this case, the existence of <math>\omega</math> would follow from either form of Limitation of Size. The class of [[von Neumann ordinal]]s can be [[well-order]]ed. 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 well-ordered. MK can be confused with second-order ZFC, ZFC with [[second-order logic]] (representing second-order objects in set rather than predicate language) as its background logic. 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 [[syntax|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 second-order ZFC are quite different from those of MK; whatever is true in all models of second-order ZFC in which the classes are '''all''' the collections of the sets, is also provable (because the logic is second-order). Hence second-order ZFC "decides" many classical conundrums, such as the [[continuum hypothesis]], although in a sense that is arguably not very practical. Second-order ZFC also uniquely determines the [[rank (set theory)|rank]], if any, of the [[cumulative hierarchy]] up to the first [[inaccessible cardinal]]. === Model theory === ZFC, NBG, and MK each have models describable in terms of ''V'', the [[inner model|standard model]] of [[Zermelo–Fraenkel set theory|ZFC]] and the [[von Neumann universe]]. Let the [[inaccessible cardinal]] κ be a member of ''V''. Also let Def(''X'') denote the Δ<sub>0</sub> definable [[subset]]s of ''X'' (see [[constructible universe]]). Then: *''V''<sub>κ</sub> is an [[intended interpretation|intended model]] of [[Zermelo–Fraenkel set theory|ZFC]]; * Def(''V''<sub>κ</sub>) is an intended model of [[Von Neumann–Bernays–Gödel set theory|NBG]]; *''V''<sub>κ+1</sub>, the [[power set]] of ''V''<sub>κ</sub>, 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 [[W. V. Quine|Quine's]] [[New Foundations|ML]], that built on [[New Foundations]] rather than on [[Zermelo–Fraenkel set theory|ZFC]].<ref>The ''locus citandum'' for ML is the 1951 ed. of [[W. V. O. Quine|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.</ref> [[Impredicative]] class comprehension was also proposed in [[Mostowski]] (1951) and [[David Kellogg Lewis|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 well-known 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 [[set builder notation|class abstract]]s of the form <math>\ \{x : A(x)\},</math> "the class of all sets ''x'' satisfying ''A''(''x'')." '''Definition:''' ''x'' is a ''set'' [and hence not a [[proper class]]] [[iff]] for some ''y'', <math>x \in y</math>. '''I. Extent:''' For each ''x'' and each ''y'', ''x=y'' [[iff]] for each ''z'', <math>z \in x</math> when and only when <math>z \in y.</math> '''I''' 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 <math> \beta</math>, <math>\beta \in \{\alpha:A\}</math> [[iff]] <math>\beta</math> is a set and <math>B,</math> '&alpha;' and '&beta;' are replaced by variables, ' ''A'' ' by a formula Æ, and ' ''B'' ' by the formula obtained from Æ by replacing each occurrence of the variable which replaced &alpha; by the variable which replaced &beta;. ''Develop'': [[Algebra of sets]]. Existence of the [[empty set|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 <math>z \subseteq x</math>, then <math>z \in y.</math> ''Develop'': ''V'' is not a set. Existence of [[singleton]]s. [[axiom of separation|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 <math>x \cup y</math> is a set. The import of '''IV''' is that of Pairing above, whose proof sketch goes as follows. The singleton <math>\{x\}</math> 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 <math>\{x,y\}</math> is a set if ''x'' and ''y'' are sets. ''Develop'': Unordered and [[ordered pair]]s, [[relation (mathematics)|relations]], [[function (set theory)|function]]s, [[domain (mathematics)|domain]], [[range (mathematics)|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 <math>\bigcup x</math> is a set. The import of '''VI''' is that of Union above. '''V''' and '''VI''' may be combined into one axiom.<ref>Kelley (1955), p. 261, fn †.</ref> ''Develop'': [[Cartesian product]], [[injection]], [[surjection]], [[bijection]], [[order theory]]. '''VII. Regularity:''' If <math>x \neq \varnothing</math> there is a member ''y'' of ''x'' such that <math>x \cap y = \varnothing.</math> The import of '''VII''' is that of Foundation above. ''Develop'': [[Ordinal number]]s, [[transfinite induction]]. '''VIII. Infinity:''' There exists a set ''y'', such that <math>\varnothing \in y</math> and <math>x \cup \{x\} \in y</math> whenever <math>x \in y.</math> '''VIII''' asserts the unconditional existence of two sets, the [[infinite set|infinite]] [[inductive set]] ''y'', and the null set <math>\varnothing.</math> <math>\varnothing</math> 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 number]]s, '''N''' is a set, [[Peano axioms]], [[integer]]s, [[rational number]]s, [[real number]]s. '''Definition:''' ''c'' is a ''choice function'' [[iff]] ''c'' is a function and <math>c(x) \in x</math> for each member ''x'' of ''domain c''. '''IX. Choice:''' There exists a choice function ''c'' whose domain is <math>V - \{\varnothing\}.</math>. '''IX''' is very similar to the [[axiom of global choice]] derivable from Limitation of Size. ''Develop'': [[axiom of choice#Equivalents|Equivalents]] of the [[axiom of choice]]. As is the case with [[Zermelo–Fraenkel set theory|ZFC]], the [[cardinal number]]s require some form of this axiom. Theorems of [[Cantor's theorem|Cantor]] and [[Schroeder-Bernstein theorem|Schroeder-Bernstein]]. ==Notes== <references/> == 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. * {{cite book | author=Mendelson, Elliott | title=Introduction to Mathematical Logic | publisher=Chapman & Hall | year=1997 | id=ISBN 0-534-06624-0}} The definitive treatment of the closely related set theory [[Von Neumann–Bernays–Gödel 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]], Andrejz (1951) "Some impredicative definitions in the axiomatic set theory," ''Fundamenta Matheticae'' 37: 111-24. *Rubin, Jean E. (1967) ''Set Theory for the Mathematician''. San Francisco: Holden Day. More thorough than Monk; the ontology includes [[urelement]]s. == External links == From Foundations of Mathematics (FOM) discussion group: *[http://www.cs.nyu.edu/pipermail/fom/2004-May/008208.html Allen Hazen on set theory with classes.] *[http://www.cs.nyu.edu/pipermail/fom/2000-February/003740.html Joseph Shoenfield's doubts about MK.] {{DEFAULTSORT:Morse-Kelly set theory}} [[Category:Systems of set theory]] [[cs:Kelley-Morseova teorie množin]]