Von Neumann–Bernays–Gödel set theory
528491
216838381
2008-06-03T13:22:58Z
RussBot
279219
Robot-assisted fix [[WP:DPL|links to disambiguation page]] Function
In the [[foundations of mathematics]], '''Von Neumann–Bernays–Gödel set theory''' ('''NBG''') is an [[axiomatic set theory]] that is a [[conservative extension]] of the canonical axiomatic set theory [[ZFC]]. A statement in the language of ZFC is provable in NBG [[if and only if]] it is provable in ZFC. The [[ontology]] of NBG includes [[proper class]]es, objects having members but that cannot be members. NBG's principle of class comprehension is [[impredicative|predicative]]; [[quantifier|quantified]] variables in the defining [[first order logic|formula]] can range only over sets. Allowing [[impredicative]] comprehension turns NBG into [[Morse-Kelley set theory]], MK. NGB, unlike ZFC and MK, can be [[finite set|finite]]ly axiomatized.
==Ontology==
The defining aspect of NBG is the distinction between [[proper class]] and [[set]]. Let ''a'' and ''s'' be two individuals. Then the [[atomic sentence]] <math>a \in s</math> is defined if ''a'' is a [[set]] and ''s'' is a [[class (set theory)|class]]. In other words, <math>a \in s</math> is defined unless ''a'' is a proper class. A proper class is very large; NBG even admits of "the class of all sets", the universal class called ''V''. However, NBG does not admit "the class of all classes" or "the set of all sets".
By NBG's axiom schema of Class Comprehension, all objects satisfying any given formula in the [[first order logic|first order language]] of NBG form a class; if the class would not be a set in [[ZFC]], it is an NBG proper class.
The development of classes mirrors the development of [[naive set theory]]. The principle of abstraction is given, and thus classes can be formed out of all individuals satisfying any statement of [[first order logic]] whose [[atomic sentence]]s all involve either the membership relation or predicates definable from membership. Equality, pairing, subclass, and such, are all definable and so need not be axiomatized — their definitions denote a particular [[abstraction]] of a [[formula]].
Sets are developed in a manner very similarly to ZF. Let ''Rp''(''A,a''), meaning "the set ''a'' represents the class ''A''," denote a [[binary relation]] defined as follows:
:<math>\mathrm{Rp}(A,a) := \forall x(x \in A \leftrightarrow x \in a).</math>
That is, ''a'' "represents" ''A'' if every element of ''a'' is an element of ''A'', and conversely. Classes lacking representations, such as the class of all sets that do not contain themselves (the class invoked by the [[Russell paradox]]), are the [[proper class]]es.
===History===
The first variant of NBG, by [[John von Neumann]] in the [[1920s]], took [[Function (mathematics)|functions]] and not sets, as primitive. In a series of articles published 1937-54, [[Paul Bernays]] modified Von Neumann's theory so as to make sets and set membership primitive. [[Kurt Gödel|Gödel]] (1940), while investigating the independence of the [[Continuum hypothesis]], further simplified the theory and discovered that it could be finitely axiomatized. [[Richard Montague|Montague]] (1961) showed that ZFC cannot be finitely axiomatized.
== Axiomatizating NBG ==
NBG is presented here as a two-sorted theory, with lower case letters denoting variables ranging over sets, and upper case letters denoting variables ranging over classes. Hence <math>x \in y</math> should be read "set ''x'' is a member of set ''y''," and <math>x \in Y</math> as "set ''x'' is a member of class ''Y''." Statements of equality may take the form
<math>x=y</math> or <math>X=Y</math>. ''a=A'' stands for <math>\forall x (x \in a \leftrightarrow x \in A)</math> and is an [[abuse of notation]]. NBG can also be presented as a one-sorted theory of classes, with sets being those classes that are members of at least one other class.
We first axiomatize NBG using the axiom schema of Class Comprehension. This schema is provably equivalent<ref>Mendelson (1997), p. 232, Prop. 4.4, proves Class Comprehension equivalent to the axioms '''B1-B7''' shown on p. 230 and described below.</ref> to 9 of its finite instances, stated in the following section. Hence these 9 finite axioms can replace Class Comprehension. This is the precise sense in which NGB can be finitely axiomatized.
=== With Class Comprehension schema ===
The following five axioms are identical to their [[ZFC]] counterparts:
*'''[[axiom of extension|extensionality]]:''' <math>\forall x (x \in a \leftrightarrow x \in b)\rightarrow a=b.</math>: Sets with the same elements are the same set.
*'''[[axiom of pairing|pairing]]:''' <math>\forall x \forall y \exist z \forall w [w \in z \leftrightarrow (w = x \or w = y)].</math> For any sets ''x'' and ''y'', there is a set, <math>\{x,y\}</math>, whose elements are exactly ''x'' and ''y''.
:''pairing'' implies that for any set ''x'', the set {''x''} (the [[singleton set]]) exists. Also, given any two sets ''x'' and ''y'' and the usual set-theoretic definition of the [[ordered pair]], the ordered pair (''x,y'') exists and is a set. By Class Comprehension, all relations on sets are classes. Moreover, certain kinds class relations are one or more of functions, injections, and bijections from one class to another. ''pairing'' is an axiom in [[Z|Zermelo set theory]] and a theorem in [[ZFC]].
*'''[[axiom of union|union]]:''' For any set ''x'', there is a set which contains exactly the elements of elements of ''x''.
*'''[[axiom of power set|power set]]:''' For any set ''x'', there is a set which contains exactly the subsets of ''x''.
*'''[[axiom of infinity|infinity]]:''' There exists an [[inductive set]], namely a set ''x'' whose members are (i) the [[empty set]]; (ii) for every member ''y'' of ''x'', <math>y \cup \{y\}</math> is also a member of ''x''.
:''infinity'' can be formulated so as to imply the existence of the [[null set]].<ref>Mendelson (1997), p. 239, Ex. 4.22(b).</ref>
The remaining axioms have capitalized names because they are primarily concerned with classes rather than sets. The next two axioms differ from their [[ZFC]] counterparts only in that their quantified variables range over classes, not sets:
*'''Extensionality:''' <math>\forall x (x \in A \leftrightarrow x \in B)\rightarrow A=B.</math>: Classes with the same elements are the same class.
*'''Foundation (Regularity):''' Each nonempty class is disjoint from one of its elements.
The last two axioms are peculiar to NBG:
*'''[[axiom of limitation of size|Limitation of Size]]:''' For any class ''C'', a set ''x'' such that ''x=C'' exists if and only if there is no [[bijection]] between ''C'' and the class ''V'' of all sets.
:From this axiom, due to [[Von Neumann]], [[axiom schema of separation|Subsets]], [[axiom schema of replacement|Replacement]], and [[axiom of global choice|Global Choice]] can all be derived. This axiom implies the [[axiom of global choice]] because the class of [[ordinal number|ordinals]] is not a set; hence there exists a [[bijection]] between the ordinals and the [[universe]]. If Limitation of Size were weakened to "If the domain of a class function is a subset of some set, then the range of that function is likewise as set," then no form of the [[axiom of choice]] is an NBG theorem. In this case, any of the usual local forms of Choice may be taken as an added axiom, if desired.
:Limitation of Size cannot be found in Mendelson (1997) NGB. In its place, we find the usual [[axiom of choice]] for sets, and the following form of the [[axiom schema of replacement]]: if the class ''F'' is a [[function (set theory)|function]] whose [[domain (mathematics)|domain]] is a set, the [[range (mathematics)|range]] of ''F'' is also a set .<ref>Mendelson (1997), p. 239, axiom R.</ref>
*'''Class Comprehension schema:''' For any formula <math>\phi</math> containing no quantifiers over classes (it may contain class and set parameters), there is a class ''A'' such that <math>\forall x (x \in A \leftrightarrow \phi(x)).</math>
:This axiom asserts that invoking the principle of [[axiom schema of specification|unrestricted comprehension]] of [[naive set theory]] yields a class rather than a set, thereby banishing the [[paradoxes of set theory]].
:Class Comprehension is the only axiom schema of NBG. In the next section, we show how this schema can be replaced by a number of its own instances. Hence NBG can be finitely axiomatized. If the quantified variables in φ(''x'') range over classes instead of sets, the result is [[Morse-Kelley set theory]], a [[proper extension]] of ZFC which cannot be finitely axiomatized.
=== Replacing Class Comprehension with finite instances thereof ===
An appealing but somewhat mysterious feature of NBG is that its axiom schema of Class Comprehension is equivalent to the conjunction of a finite number of its instances. The axioms of this section may replace the Axiom of Class Comprehension in the preceding section. The finite axiomatization presented below does not necessarily resemble exactly any NBG axiomatization in print.
We develop our axiomatization by considering the structure of formulas.
*'''Sets:''' For any set ''x'', there is a class ''X'' such that ''x=X''.
This axiom, in combination with the set existence axioms from the previous axiomatization, assures the existence of classes from the outset, and enables formulas with class parameters.
Let <math>A=\{x \mid \phi\}</math> and <math>B=\{x \mid \psi\}.</math> Then <math>\{x \mid \neg\phi\} = V-A</math> and <math>\{x \mid \phi\wedge \psi\} = A \cap B</math> suffice for handling all [[sentential connective]]s, because ∧ and ¬ are a [[functional completeness|functionally complete]] set of connectives.
*'''Complement:''' For any class ''A'', the [[complement]] <math>V-A = \{x \mid x \not\in A\}</math> is a class.
*'''Intersection:''' For any classes ''A'' and ''B'', the [[intersection]] <math>A \cap B = \{x \mid x \in A \wedge x \in B\}</math> is a class.
We now turn to quantification. In order to handle multiple variables, we need the ability to represent [[relation]]s. Define the [[ordered pair]] <math>(a,b)</math> as <math>\{\{a\},\{a,b\}\},</math> as usual. Note that two applications of '''pairing''' to ''a'' and ''b'' assure that (''a'',''b'') is indeed a set.
*'''Products:''' For any classes ''A'' and ''B'', the class <math>A \times B = \{(a,b) \mid a \in A \wedge b \in B\}</math> is a class. (In practice, only <math>V \times A</math> is needed.)
*'''Converses:''' For any class ''R'', the classes:
: <math>Conv1(R) = \{(b,a)\mid (a,b)\in R\}</math> and
: <math>Conv2(R) = \{(b,(a,c)) \mid (a,(b,c)) \in R\}</math> exist.
*'''Association:''' For any class ''R'', the classes:
: <math>Assoc1(R) = \{((a,b),c) \mid (a,(b,c)) \in R\}</math> and
: <math>Assoc2(R) = \{(d,(a,(b,c))) \mid (d,((a,b),c)) \in R\}</math> exist.
These axioms license adding dummy arguments, and rearranging the order of arguments, in relations of any [[arity]]. The peculiar form of ''Association'' is designed exactly to make it possible to bring any term in a list of arguments to the front (with the help of ''Converses''). We represent the argument list <math>(x_1,x_2,\ldots,x_n)</math> as <math>(x_1,(x_2,\ldots,x_n))</math> (it is a pair with the first argument as its first projection and the "tail" of the argument list as the second projection). The idea is to apply ''Assoc1'' until the argument to be brought to the front is second, then apply ''Conv1'' or ''Conv2'' as appropriate to bring the second argument to the front, then apply ''Assoc2'' until the effects of the original applications of ''Assoc1'' (which are now behind the moved argument) are corrected.
If <math>\{(x,y)\mid \phi(x,y)\}</math> exists, then the set <math>\{y \mid \exists x[\phi(x,y)]\}</math> is simply the [[range]] of the first set, considered as a relation. The [[universal quantifier]] can be defined in terms of the [[existential quantifier]] and [[negation]].
*'''Ranges:''' For any class ''R'', the class <math>Rng(R) = \{y \mid \exists x[(x,y)\in R]\}</math> exists.
The above axioms can reorder the arguments of any relation so as to bring any desired argument to the front of the argument list, where it can be quantified.
Finally, each [[atomic formula]] implies the existence of a corresponding class relation:
*'''Membership:''' The class <math>[\in] = \{(x,y) \mid x\in y\}</math> exists.
*'''Diagonal:''' The class <math>[=] = \{(x,y) \mid \,x=y\}</math> exists.
''Diagonal'', together with addition of dummy arguments and rearrangement of arguments, can build a relation asserting the equality of any two of its arguments; thus repeated variables can be handled.
====Mendelson's variant====
Mendelson (1997: 230) refers to his axioms '''B1-B7''' of class comprehension as "axioms of class existence." Four of these identical to axioms already stated above: '''B1''' is Membership; '''B2''', Intersection; '''B3''', Complement; '''B5''', Product. '''B4''' is Ranges modified to assert the existence of the domain of ''R'' (by existentially quantifying ''y'' instead of ''x''). The last two axioms are:
:'''B6:''' <math> \forall X \exist Y \forall uvw[(u,v,w) \in Z \leftrightarrow (v,w,u) \in X].</math>
:'''B7:''' <math> \forall X \exist Y \forall uvw[(u,v,w) \in Z \leftrightarrow (u,w,v) \in X].</math>
'''B6''' and '''B7''' enable what Converses and Association enable: given any class ''X'' of ordered triples, there exists another class ''Y'' whose members are the members of ''X'' each reordered in the same way.
==Discussion==
For a discussion of some [[ontology|ontological]] and other philosophical issues posed by NBG, especially when contrasted with [[ZFC]] and [[MK]], see Appendix C of Potter (2004).
Even though NBG is a [[conservative extension]] of ZFC, a theorem may have a shorter and more elegant proof in NBG than in ZFC (or vice versa). For a survey of known results of this nature, see Pudlak (1998).
===Model theory===
ZFC, NBG, and MK have models describable in terms of ''V'', the [[inner model|standard model]] of [[ZFC]] and the [[von Neumann universe]]. Now let the members of ''V'' include the [[inaccessible cardinal]] κ. Also let Def(''X'') denote the Δ<sub>0</sub> definable [[subset]]s of ''X'' (see [[constructible universe]]). Then:
*''V''<sub>κ</sub> is an intended model of [[ZFC]];
* Def(''V''<sub>κ</sub>) is an [[intended interpretation|intended model]] of NBG;
*''V''<sub>κ+1</sub> is an intended model of [[Morse–Kelley set theory|MK]].
===Category theory===
The ontology of NBG provides scaffolding for speaking about "large objects" without risking paradox. In some developments of [[category theory]], for instance, a "large category" is defined as one whose [[object (category theory)|object]]s make up a proper class, with the same being true of its [[morphism]]s. A "small category," on the other hand, is one whose objects and morphisms are members of some set. We can thus easily speak of the "[[category of all small categories]]" without risking paradox. That category is large, of course.
On whether an ontology including classes as well as sets is adequate for [[category theory]], see Muller (2001).
== See also ==
*[[Impredicativity|Predicativity]]
*[[Morse-Kelley set theory]]
*[[ZFC]]
== Notes ==
<references/>
== References ==
* {{cite book | author=Bernays, Paul | title=Axiomatic Set Theory | publisher=Dover Publications | year=1991 | id=ISBN 0-48-666637-9}}
* Mendelson, Elliott, 1997. ''An Introduction to Mathematical Logic'', 4th ed. London: Chapman & Hall. ISBN 0412808307. Pp. 225-86 contain the classic textbook treatment of NBG, showing how it does what we expect of set theory, by grounding [[relation (mathematics)|relations]], [[order theory]], [[ordinal number]]s, [[transfinite number]]s, etc.
* [[Richard Montague]], 1961, "Semantic Closure and Non-Finite Axiomatizability I," in ''Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics'', (Warsaw, 2-9 September 1959). Pergamon: 45-69.
*Muller, F. A., 2001, "Sets, classes, and categories," ''British Journal of the Philosophy of Science'' 52: 539-73.
*Potter, Michael, 2004. ''Set Theory and Its Philosophy''. Oxford Univ. Press.
*Pudlak, P., 1998, "The lengths of proofs" in Buss, S., ed., ''Handbook of Proof Theory''. North-Holland: 547-637.
* [[John von Neumann]], 1925, "An Axiomatization of Set Theory." English translation in [[Jean van Heijenoort]], ed., 1967. ''From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931''. Harvard University Press.
==External links==
*{{planetmathref|id=4395|title= von Neumann-Bernays-Gödel set theory}}
[[Category:Systems of set theory|Von Neumann-Bernays-Godel set theory]]
[[cs:Von Neumann-Bernays-Gödelova teorie množin]]
[[de:Neumann-Bernays-Gödel-Mengenlehre]]
[[fr:Théorie des ensembles de von Neumann–Bernays–Gödel]]
[[hu:Neumann–Bernays–Gödel-halmazelmélet]]
[[zh:冯诺伊曼-博内斯-哥德尔集合论]]