View source for Von Neumann–Bernays–Gödel set theory

{{Short description|System of mathematical set theory}}
{{Use dmy dates|date=October 2020}}
In the [[foundations of mathematics]], '''von Neumann–Bernays–Gödel set theory''' ('''NBG''') is an [[axiomatic set theory]] that is a [[conservative extension]] of [[Zermelo–Fraenkel set theory|Zermelo–Fraenkel–choice set theory]] (ZFC). NBG introduces the [[Primitive notion|notion]] of [[Class (set theory)|class]], which is a collection of [[Set (mathematics)|sets]] defined by a [[Formula (mathematical logic)|formula]] whose [[Quantifier (logic)|quantifiers]] range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all [[ordinal number|ordinals]]. [[Morse–Kelley set theory]] (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

A key theorem of NBG is the class existence theorem, which states that for every formula whose quantifiers range only over sets, there is a class consisting of the sets satisfying the formula. This class is built by mirroring the step-by-step construction of the formula with classes. Since all set-theoretic formulas are constructed from two kinds of [[atomic formula]]s ([[Membership (set theory)|membership]] and [[Equality (mathematics)|equality]]) and finitely many [[logical symbols]], only finitely many [[axiom]]s are needed to build the classes satisfying them. This is why NBG is finitely axiomatizable. Classes are also used for other constructions, for handling the [[Absolute infinite, well-ordering theorem, and paradoxes|set-theoretic paradoxes]], and for stating the [[axiom of global choice]], which is stronger than ZFC's [[axiom of choice]].

[[John von Neumann]] introduced classes into set theory in 1925. The [[primitive notion]]s of his theory were [[Function (set theory)|function]] and [[Argument of a function|argument]]. Using these notions, he defined class and set.<ref name=VN1925def>{{harvnb|von Neumann|1925|pp=221&ndash;224, 226, 229}}; English translation: {{Harvnb|van&nbsp;Heijenoort|2002b|pp=396&ndash;398, 400, 403}}.</ref> [[Paul Bernays]] reformulated von Neumann's theory by taking class and set as primitive notions.<ref name=Bernays1937def>{{harvnb|Bernays|1937}}, pp. 66&ndash;67.</ref> [[Kurt Gödel]] simplified Bernays' theory for his [[relative consistency]] proof of the [[axiom of choice]] and the [[generalized continuum hypothesis]].<ref name=Godel1940>{{harvnb|Gödel|1940}}.</ref>

== Classes in set theory ==
=== The uses of classes ===
Classes have several uses in NBG:
* They produce a finite axiomatization of set theory.<ref>{{harvnb|Gödel|1940|pp=3&ndash;7}}.</ref>
* They are used to state a "very strong form of the [[axiom of choice]]"<ref name=Godelp6>{{harvnb|Gödel|1940|p=6}}.</ref>—namely, the [[axiom of global choice]]: There exists a global choice function <math>G</math> defined on the class of all nonempty sets such that <math>G(x) \in x</math> for every nonempty set <math>x.</math> This is stronger than ZFC's axiom of choice: For every set <math>s</math> of nonempty sets, there exists a [[choice function]] <math>f</math> defined on <math>s</math> such that <math>f(x) \in x</math> for all <math>x \in s.</math>{{efn|[[#Axiom of global choice|Axiom of global choice]] explains why it is provably stronger.}}
* The [[Absolute infinite, well-ordering theorem, and paradoxes|set-theoretic paradoxes]] are handled by recognizing that some classes cannot be sets. For example, assume that the class <math>Ord</math> of all [[Ordinal number|ordinal]]s is a set. Then <math>Ord</math> is a [[Transitive (set theory)|transitive]] set [[well-order]]ed by <math>\in</math>. So, by definition, <math>Ord</math> is an ordinal. Hence, <math>Ord \in Ord</math>, which contradicts <math>\in</math> being a well-ordering of <math>Ord.</math> Therefore, <math>Ord</math> is not a set. A class that is not a set is called a [[proper class]]; <math>Ord</math> is a proper class.<ref>{{harvnb|Gödel|1940|p=25}}.</ref>
*{{Anchor|Gödel's function}} Proper classes are useful in constructions. In his proof of the relative consistency of the axiom of global choice and the [[generalized continuum hypothesis]], Gödel used proper classes to build the [[constructible universe]]. He constructed a function on the class of all ordinals that, for each ordinal, builds a constructible set by applying a set-building operation to previously constructed sets. The constructible universe is the [[Image (set theory)|image]] of this function.<ref>{{harvnb|Gödel|1940|pp=35&ndash;38}}.</ref>

=== Axiom schema versus class existence theorem ===
Once classes are added to the language of ZFC, it is easy to transform ZFC into a set theory with classes. First, the [[axiom schema]] of class comprehension is added. This axiom schema states: For every formula <math>\phi(x_1, \ldots, x_n)</math> that quantifies only over sets, there exists a class <math>A</math> consisting of the {{nowrap|<math>n</math>-[[tuple]]s}} satisfying the formula—that is, <math>\forall x_1 \cdots \,\forall x_n [(x_1, \ldots , x_n) \in A \iff \phi(x_1, \ldots, x_n)].</math> Then the [[axiom schema of replacement]] is replaced by a [[#NBG's axiom of replacement|single axiom]] that uses a class. Finally, ZFC's [[axiom of extensionality]] is modified to handle classes: If two classes have the same elements, then they are identical. The other axioms of ZFC are not modified.<ref name=Britannica_NBG>{{cite encyclopedia|url=https://www.britannica.com/science/set-theory/The-Neumann-Bernays-Godel-axioms|title=The Neumann-Bernays-Gödel axioms|encyclopedia=Encyclopædia Britannica|access-date=17 January 2019}}</ref>

This theory is not finitely axiomatized. ZFC's replacement schema has been replaced by a single axiom, but the axiom schema of class comprehension has been introduced.

To produce a theory with finitely many axioms, the axiom schema of class comprehension is first replaced with finitely many [[#class existence axioms|class existence axioms]]. Then these axioms are used to prove the class existence theorem, which implies every instance of the axiom schema.<ref name=Britannica_NBG /> The [[#CET|proof of this theorem]] requires only seven class existence axioms, which are used to convert the construction of a formula into the construction of a class satisfying the formula.

== Axiomatization of NBG ==
=== Classes and sets ===
NBG has two types of objects: classes and sets. Intuitively, every set is also a class. There are two ways to axiomatize this.{{npsn|date=November 2024}} Bernays used [[First-order logic#Many-sorted logic|many-sorted logic]] with two sorts: classes and sets.<ref name=Bernays1937def /> Gödel avoided sorts by introducing primitive predicates: <math>\mathfrak{Cls}(A)</math> for "<math>A</math> is a class" and <math>\mathfrak{M}(A)</math> for "<math>A</math> is a set" (in German, "set" is ''Menge''). He also introduced axioms stating that every set is a class and that if class <math>A</math> is a member of a class, then <math>A</math> is a set.<ref name=Godel1940p3>{{harvnb|Gödel|1940|p=3}}.</ref> Using predicates is the standard way to eliminate sorts. [[Elliott Mendelson]] modified Gödel's approach by having everything be a class and defining the set predicate <math>M(A)</math> as <math>\exists C(A \in C).</math><ref>{{harvnb|Mendelson|1997|pp=225&ndash;226}}.</ref> This modification eliminates Gödel's class predicate and his two axioms.

Bernays' two-sorted approach may appear more natural at first, but it creates a more complex theory.{{efn|The historical development suggests that the two-sorted approach does appear more natural at first. In introducing his theory, Bernays stated: "According to the leading idea of von Neumann set theory we have to deal with two kinds of individuals, which we may distinguish as ''sets'' and ''classes''."<ref>{{harvnb|Bernays|1937|p=66}}.</ref>}} In Bernays' theory, every set has two representations: one as a set and the other as a class. Also, there are two [[membership relation]]s: the first, denoted by "∈", is between two sets; the second, denoted by "η", is between a set and a class.<ref name=Bernays1937def /> This redundancy is required by many-sorted logic because variables of different sorts range over disjoint subdomains of the [[domain of discourse]].

The differences between these two approaches do not affect what can be proved, but they do affect how statements are written. In Gödel's approach, <math>A \in C</math> where <math>A</math> and <math>C</math> are classes is a valid statement. In Bernays' approach this statement has no meaning. However, if <math>A</math> is a set, there is an equivalent statement: Define "set <math>a</math> represents class <math>A</math>" if they have the same sets as members—that is, <math>\forall x(x \in a \iff x \;\eta \;A).</math> The statement <math>a \;\eta \;C</math> where set <math>a</math> represents class <math>A</math> is equivalent to Gödel's <math>A \in C.</math><ref name=Bernays1937def />

The approach adopted in this article is that of Gödel with Mendelson's modification. This means that NBG is an [[axiomatic system]] in [[first-order predicate logic]] with [[Equality in set theory|equality]], and its only [[primitive notion]]s are class and the membership relation.

=== Definitions and axioms of extensionality and pairing ===
A set is a class that belongs to at least one class: <math>A</math> is a set if and only if <math>\exist C(A \in C)</math>.
A class that is not a set is called a proper class: <math>A</math> is a proper class if and only if <math>\forall C(A \notin C)</math>.<ref>{{harvnb|Mendelson|1997|p=226}}.</ref>
Therefore, every class is either a set or a proper class, and no class is both.

Gödel introduced the convention that uppercase variables range over classes, while lowercase variables range over sets.<ref name=Godel1940p3 /> Gödel also used names that begin with an uppercase letter to denote particular classes, including functions and [[relation (math)|relation]]s defined on the class of all sets. Gödel's convention is used in this article. It allows us to write:
{{plainlist|indent=1}}
* <math>\exist x\, \phi(x)</math> instead of <math>\exist x \bigl(\exist C (x \in C) \land \phi(x)\bigr)</math>
* <math>\forall x\, \phi(x)</math> instead of <math> \forall x \bigl( \exist C (x \in C) \implies \phi(x) \bigr) </math>
{{endplainlist}}

The following axioms and definitions are needed for the proof of the class existence theorem.

'''Axiom of extensionality.{{space|thin}}''' If two classes have the same elements, then they are identical.
:<math>\forall A \,\forall B \,[\forall x(x \in A \iff x \in B) \implies A = B]</math>{{space|hair}}<ref>Gödel's axiom A3 ({{harvnb|Gödel|1940|p=3}}).</ref>

This axiom generalizes ZFC's [[axiom of extensionality]] to classes.

'''[[Axiom of pairing]].{{space|thin}}''' If <math>x</math> and <math>y</math> are sets, then there exists a set <math>p</math> whose only members are <math>x</math> and <math>y</math>.
:<math>\forall x \,\forall y \,\exists p \,\forall z \,[z \in p \iff (z = x \,\lor\, z = y)]</math>{{space|hair}}<ref>Gödel's axiom A4 ({{harvnb|Gödel|1940|p=3}}).</ref>

As in ZFC, the axiom of [[extensionality]] implies the uniqueness of the set <math>p</math>, which allows us to introduce the notation <math>\{x, y\}.</math>

[[Ordered pair]]s are defined by: 
:<math>(x, y) = \{\{x\}, \{x, y\}\}</math>
Tuples are defined [[Inductive definition|inductive]]ly using ordered pairs:
:<math>(x_1) = x_1,</math>
:<math>\text{For } n > 1\!: (x_1, \ldots, x_{n-1}, x_n) = ((x_1, \ldots, x_{n-1}), x_n).</math>{{efn|Gödel defined <math>(x_1, x_2, \ldots, x_n) = (x_1, (x_2, \ldots, x_n))</math>{{space|hair}}.<ref>{{harvnb|Gödel|1940|p=4}}).</ref> This affects the statements of some of his definitions, axioms, and theorems. This article uses Mendelson's definition.<ref>{{harvnb|Mendelson|1997|p=230}}.</ref>}}

{{Anchor|class existence axioms}}

=== Class existence axioms and axiom of regularity ===
Class existence axioms will be used to prove the class existence theorem: For every formula in <math>n</math> [[free variable|free]] set variables that quantifies only over sets, there exists a class of {{nowrap|<math>n</math>-tuples}} that satisfy it. The following example starts with two classes that are [[Function (set theory)|function]]s and builds a [[composite function]]. This example illustrates the techniques that are needed to prove the class existence theorem, which lead to the class existence axioms that are needed.

{{Anchor|Ex1}}
:{| class="wikitable"
|- style="text-align: left; vertical-align: top; style="background: white" 
|'''Example 1:{{space|thin}}''' If the classes <math>F</math> and <math>G</math> are functions, then the composite function <math>G \circ F</math> is defined by the formula: <math>\exists t[(x, t) \in F \,\land\, (t, y) \in G].</math> Since this formula has two free set variables, <math>x</math> and <math>y,</math> the class existence theorem constructs the class of ordered pairs: <math>G \circ F\,=\,\{(x, y): \exists t[(x, t) \in F \,\land\, (t, y) \in G]\}.</math>

Because this formula is built from simpler formulas using [[Conjunction (logic)|conjunction]] <math>\land</math> and [[existential quantification]] <math>\exists</math>, class [[Operation (mathematics)|operation]]s are needed that take classes representing the simpler formulas and produce classes representing the formulas with <math>\land</math> and <math>\exists</math>. To produce a class representing a formula with <math>\land</math>, [[Intersection (set theory)|intersection]] used since <math>x \in A \cap B \iff x \in A \land x \in B.</math> To produce a class representing a formula with <math>\exists</math>, the [[Domain of a relation|domain]] is used since <math>x \in Dom(A) \iff \exists t[(x,t) \in A].</math>

Before taking the intersection, the tuples in <math>F</math> and <math>G</math> need an extra component so they have the same variables. The component <math>y</math> is added to the tuples of <math>F</math> and <math>x</math> is added to the tuples of <math>G</math>: 
<math display="block">F' = \{(x, t, y): (x, t) \in F\}\,</math> and <math>\,G' = \{(t, y, x): (t, y) \in G\}</math> 
In the definition of <math>F',</math> the variable <math>y</math> is not restricted by the statement <math>(x, t) \in F,</math> so <math>y</math> ranges over the class <math>V</math> of all sets. Similarly, in the definition of <math>G',</math> the variable <math>x</math> ranges over <math>V.</math> So an axiom is needed that adds an extra component (whose values range over <math>V</math>) to the tuples of a given class.

Next, the variables are put in the same order to prepare for the intersection: 
<math display="block">F'' = \{(x, y, t): (x, t) \in F\}\,</math> and <math>\,G'' = \{(x, y, t): (t, y) \in G\}</math>
To go from <math>F'</math> to <math>F''</math> and from <math>G'</math> to <math>G''</math> requires two different [[permutation]]s, so axioms that support permutations of tuple components are needed.

The intersection of <math>F''</math> and <math>G''</math> handles <math>\land</math>:
<math display="block">F'' \cap G'' = \{(x, y, t): (x, t) \in F \,\land\, (t, y) \in G\}</math>

Since <math>(x, y, t)</math> is defined as <math>((x, y), t)</math>, taking the domain of <math>F'' \cap G''</math> handles <math>\exists t</math> and produces the composite function:
<math display="block">G \circ F = Dom(F'' \cap G'') = \{(x, y): \exists t ((x, t) \in F \,\land\, (t, y) \in G)\}</math>
So axioms of intersection and domain are needed.
|}

The class existence axioms are divided into two groups: axioms handling language primitives and axioms handling tuples. There are four axioms in the first group and three axioms in the second group.{{efn|Bernays' class existence axioms specify unique classes. Gödel weakened all but three of Bernays' axioms (intersection, complement, domain) by replacing [[biconditional]]s with [[Material conditional|implication]]s, which means they specify only the ordered pairs or the 3-tuples of the class. The axioms in this section are Gödel's except for Bernays' stronger [[#Product by V axiom|product by V axiom]], which specifies a unique class of ordered pairs. Bernays' axiom simplifies the proof of the [[#CET|class existence theorem]]. Gödel's axiom B6 appears as the fourth statement of the [[#Tuple lemma|tuple lemma]]. Bernays later realized that one of his axioms is redundant, which implies that one of Gödel's axioms is redundant. Using the other axioms, axiom B6 can be proved from axiom B8, and B8 can be proved from B6, so either axiom can be considered the redundant axiom.<ref>{{harvnb|Kanamori|2009|p=56}}; {{harvnb|Bernays|1937|p=69}}; {{harvnb|Gödel|1940|pp=5, 9}}; {{harvnb|Mendelson|1997|p=231}}.</ref> The names for the tuple-handling axioms are from the French Wikipédia article: [[:fr:Théorie des ensembles de von Neumann-Bernays-Gödel#Compréhension pour les classes|Théorie des ensembles de von Neumann]].}}

'''Axioms for handling language primitives:'''

'''Membership.{{space|thin}}''' There exists a class <math>E</math> containing all the ordered pairs whose first component is a member of the second component.
:<math>\exists E \,\forall x \,\forall y \,[(x,y) \in E \iff x \in y]\!</math>{{space|hair}}<ref>Gödel's axiom B1 ({{harvnb|Gödel|1940|p=5}}).</ref>

'''Intersection (conjunction).{{space|thin}}''' For any two classes <math>A</math> and <math>B</math>, there is a class <math>C</math> consisting precisely of the sets that belong to both <math>A</math> and <math>B</math>.
:<math>\forall A \,\forall B \,\exists C \,\forall x \,[x \in C \iff (x \in A \,\land\, x \in B)]</math>{{space|hair}}<ref>Gödel's axiom B2 ({{harvnb|Gödel|1940|p=5}}).</ref>

'''[[Complement (set theory)|Complement]] (negation).{{space|thin}}''' For any class <math>A</math>, there is a class <math>B</math> consisting precisely of the sets not belonging to <math>A</math>.
:<math>\forall A \,\exists B \,\forall x \,[x \in B \iff \neg(x \in A)]</math>{{space|hair}}<ref>Gödel's axiom B3 ({{harvnb|Gödel|1940|p=5}}).</ref>

'''Domain (existential quantifier).{{space|thin}}''' For any class <math>A</math>, there is a class <math>B</math> consisting precisely of the first components of the ordered pairs of <math>A</math>. 
:<math>\forall A \,\exists B \,\forall x \,[x \in B \iff \exists y((x,y) \in A)]</math>{{space|hair}}<ref>Gödel's axiom B4 ({{harvnb|Gödel|1940|p=5}}).</ref>

By the axiom of extensionality, class <math>C</math> in the intersection axiom and class <math>B</math> in the complement and domain axioms are unique. They will be denoted by: <math>A \cap B,</math> <math>\complement A,</math> and <math>Dom(A),</math> respectively.{{efn|name=Bourbaki|This article uses [[Nicolas Bourbaki|Bourbaki]]'s complement notation <math>\complement A</math> and relative complement notation <math>\complement_X A = \complement A \cap X</math>.<ref>{{harvnb|Bourbaki|2004|p=71}}.</ref> This prefix relative complement notation is used by the class existence theorem to [[#Mirror|mirror]] the prefix logical not (<math>\neg</math>).}}

{{Anchor|Empty class}}The first three axioms imply the existence of the empty class and the class of all sets: The membership axiom implies the existence of a class <math>E.</math> The intersection and complement axioms imply the existence of <math>E \cap \complement E</math>, which is empty. By the axiom of extensionality, this class is unique; it is denoted by <math>\empty.</math> The complement of <math>\empty</math> is the class <math>V</math> of all sets, which is also unique by extensionality. The set predicate <math>M(A)</math>, which was defined as <math>\exists C(A \in C)</math>, is now redefined as <math>A \in V</math> to avoid quantifying over classes.

'''Axioms for handling tuples:'''

{{Anchor|Product by V axiom}}'''[[Cartesian product|Product]] by <math>V</math>.{{space|thin}}''' For any class <math>A</math>, there is a class <math>B</math> consisting of the ordered pairs whose first component belongs to <math>A</math>.  
:<math>\forall A \,\exists B \,\forall u \,[u \in B \iff \exists x \, \exists y \,(u = (x, y) \land x \in A)]</math><ref>Bernays' axiom b(3) ({{harvnb|Bernays|1937|p=5}}).</ref>

'''[[Circular permutation]].{{space|thin}}''' For any class <math>A</math>, there is a class <math>B</math> whose 3{{nbhyph}}tuples are obtained by applying the circular permutation <math>(y,z,x) \mapsto (x,y,z)</math> to the 3{{nbhyph}}tuples of <math>A</math>.
:<math>\forall A \,\exists B \,\forall x \,\forall y \,\forall z \,[(x,y,z) \in B \iff (y,z,x) \in A]</math><ref>Gödel's axiom B7 ({{harvnb|Gödel|1940|p=5}}).</ref>

'''[[Transposition (mathematics)|Transposition]].{{space|thin}}''' For any class <math>A</math>, there is a class <math>B</math> whose 3{{nbhyph}}tuples are obtained by transposing the last two components of the 3{{nbhyph}}tuples of <math>A</math>.
:<math>\forall A \,\exists B \,\forall x \,\forall y \,\forall z \,[(x,y,z) \in B \iff (x,z,y) \in A]</math><ref>Gödel's axiom B8 ({{harvnb|Gödel|1940|p=5}}).</ref>

By extensionality, the product by <math>V</math> axiom implies the existence of a unique class, which is denoted by <math>A \times V.</math> This axiom is used to define the class <math>V^n</math> of all {{nowrap|<math>n</math>-tuples}}: <math>V^1 = V</math> and <math>V^{n+1} = V^n \times V.\,</math> If <math>A</math> is a class, extensionality implies that <math>A \cap V^n</math> is the unique class consisting of the {{nowrap|<math>n</math>-tuples}} of <math>A.</math> For example, the membership axiom produces a class <math>E</math> that may contain elements that are not ordered pairs, while the intersection <math>E \cap V^2</math> contains only the ordered pairs of <math>E</math>.

The circular permutation and transposition axioms do not imply the existence of unique classes because they specify only the 3{{nbhyph}}tuples of class <math>B.</math> By specifying the 3{{nbhyph}}tuples, these axioms also specify the {{nowrap|<math>n</math>-tuples}} for <math>n \ge 4</math> since: <math display="block">(x_1, \ldots, x_{n-2}, x_{n-1}, x_n) = ((x_1, \ldots, x_{n-2}), x_{n-1}, x_n).</math> The axioms for handling tuples and the domain axiom imply the following lemma, which is used in the proof of the class existence theorem.

{{Anchor|Tuple lemma}}{{math theorem | name = Tuple lemma | math_statement =<nowiki/>
# <math display="block">\forall A \,\exists B_1 \,\forall x \,\forall y \,\forall z \,[(z,x,y) \in B_1 \iff (x,y) \in A]</math>
# <math display="block">\forall A \,\exists B_2 \,\forall x \,\forall y \,\forall z \,[(x,z,y) \in B_2 \iff (x,y) \in A]</math>
# <math display="block">\forall A \,\exists B_3 \,\forall x \,\forall y \,\forall z \,[(x,y,z) \in B_3 \iff (x,y) \in A]</math>
# <math display="block">\forall A \,\exists B_4 \,\forall x \,\forall y \,\forall z \,[(y,x) \in B_4 \iff (x,y) \in A]</math>}}
{{math proof | proof =
*Class <math>B_3</math>: Apply product by <math>V</math> to <math>A</math> to produce <math>B_3.</math>
*Class <math>B_2</math>: Apply transposition to <math>B_3</math> to produce <math>B_2.</math>
*Class <math>B_1</math>: Apply circular permutation to <math>B_3</math> to produce <math>B_1.</math>
*Class <math>B_4</math>: Apply circular permutation to <math>B_2</math>, then apply domain to produce <math>B_4.</math>}}

One more axiom is needed to prove the class existence theorem: the [[axiom of regularity]]. Since the existence of the empty class has been proved, the usual statement of this axiom is given.{{efn|Since Gödel states this axiom before he proves the existence of the empty class, he states it without using the empty class.<ref name=Godelp6/>}}

{{Anchor|Axiom of regularity}}'''[[Axiom of regularity]].{{space|thin}}''' Every nonempty set has at least one element with which it has no element in common.
<math display="block">\forall a\,[a \neq \empty \implies \exists u(u \in a \land u \cap a = \empty)].</math>

This axiom implies that a set cannot belong to itself: Assume that <math>x \in x</math> and let <math>a = \{x\}.</math> Then <math>x \cap a \ne \empty</math> since <math>x \in x \cap a.</math> This contradicts the axiom of regularity because <math>x</math> is the only element in <math>a.</math> Therefore, <math>x \notin x.</math> The axiom of regularity also prohibits infinite descending membership sequences of sets: <math display="block">\cdots \in x_{n+1} \in x_n \in \cdots \in x_1 \in x_0.</math>

Gödel stated regularity for classes rather than for sets in his 1940 monograph, which was based on lectures given in 1938.<ref>{{harvnb|Gödel|1940|p=6}}; {{harvnb|Kanamori|2012|p=70}}.</ref> In 1939, he proved that regularity for sets implies regularity for classes.<ref>{{harvnb|Kanamori|2009|p=57}}; {{harvnb|Gödel|2003|p=121}}. Both references contain Gödel's proof but Kanamori's is easier to follow since he uses modern terminology.</ref>

=== Class existence theorem ===
{{Anchor|CET}}
{{math theorem | name = Class existence theorem | math_statement = Let <math>\phi(x_1, \dots, x_n, Y_1, \dots, Y_m)</math> be a formula that quantifies only over sets and contains no [[free variable]]s other than <math>x_1, \dots, x_n, Y_1, \dots, Y_m</math> (not necessarily all of these). Then for all <math>Y_1, \dots, Y_m</math>, there exists a unique class <math>A</math> of {{nowrap|<math>n</math>-tuples}} such that: <math display="block">\forall x_1 \cdots \,\forall x_n [(x_1, \dots , x_n) \in A \iff \phi(x_1, \dots, x_n, Y_1, \dots, Y_m)].</math> The class <math>A</math> is denoted by <math>\{(x_1, \dots , x_n): \phi(x_1, \dots, x_n, Y_1, \dots, Y_m)\}.</math>{{efn|The proofs in this and the next section come from Gödel's proofs, which he gave at the [[Institute for Advanced Study]] where he "could count upon an audience well versed in [[mathematical logic]]".<ref>{{harvnb|Dawson|1997|p=134}}.</ref> To make Gödel's proofs more accessible to Wikipedia readers, a few modifications have been made. The goal in this and the next section is to prove Gödel's M4, his fourth class existence theorem. The proof in this section mostly follows the M1 proof,<ref>{{harvnb|Gödel|1940|pp=8&ndash;11}}</ref> but it also uses techniques from the M3 and M4 proofs. The theorem is stated with class variables rather than M1's symbols for special classes (universal quantification over the class variables is equivalent to being true for any instantiation of the class variables). The major differences from the M1 proof are: unique classes of {{nowrap|<math>n</math>-tuples}} are generated at the end of the basis and inductive steps (which require Bernays' stronger product by <math>V</math> axiom), and [[bound variable]]s are replaced by subscripted variables that continue the numbering of the free set variables. Since bound variables are free for part of the induction, this guarantees that, when they are free, they are treated the same as the original free variables. One of the benefits of this proof is the [[#Mirror|example output]] of the function Class, which shows that a class's construction mirrors its defining formula's construction.}}}}

The theorem's proof will be done in two steps:
# Transformation rules are used to transform the given formula <math>\phi</math> into an [[logically equivalent|equivalent]] formula that simplifies the [[Mathematical induction|inductive]] part of the proof. For example, the only logical symbols in the transformed formula are <math>\neg</math>, <math>\land</math>, and <math>\exists</math>, so the induction handles logical symbols with just three cases.  
# The class existence theorem is proved inductively for transformed formulas. Guided by the structure of the transformed formula, the class existence axioms are used to produce the unique class of {{nowrap|<math>n</math>-tuples}} satisfying the formula.

'''Transformation rules.{{space|thin}}''' In rules 1 and 2 below, <math>\Delta</math> and <math>\Gamma</math> denote set or class variables. These two rules eliminate all occurrences of class variables before an <math>\in</math> and all occurrences of equality. Each time rule 1 or 2 is applied to a subformula, <math>i</math> is chosen so that <math>z_i</math> differs from the other variables in the current formula. The three rules are repeated until there are no subformulas to which they can be applied. This produces a formula that is built only with <math>\neg</math>, <math>\land</math>, <math>\exists</math>, <math>\in</math>, set variables, and class variables <math>Y_k</math> where <math>Y_k</math> does not appear before an <math>\in</math>.

# <math>\,Y_k \in \Gamma</math> is transformed into <math>\exists z_i(z_i = Y_k \,\land\, z_i \in \Gamma).</math>
# Extensionality is used to transform <math>\Delta = \Gamma</math> into <math>\forall z_i(z_i \in \Delta \iff z_i \in \Gamma).</math> 
# Logical identities are used to transform subformulas containing <math>\lor, \implies, \iff,</math> and <math>\forall</math> to subformulas that only use <math>\neg, \land,</math> and <math>\exists.</math>

'''Transformation rules: [[bound variables]].{{space|thin}}''' Consider the composite function formula of [[#Ex1|example 1]] with its free set variables replaced by <math>x_1</math> and <math>x_2</math>: <math>\exists t[(x_1, t) \in F \,\land\, (t, x_2) \in G].</math> The inductive proof will remove <math>\exists t</math>, which produces the formula <math>(x_1, t) \in F \land (t, x_2) \in G.</math> However, since the class existence theorem is stated for subscripted variables, this formula does not have the form expected by the [[induction hypothesis]]. This problem is solved by replacing the variable <math>t</math> with <math>x_3.</math> Bound variables within nested quantifiers are handled by increasing the subscript by one for each successive quantifier. This leads to rule 4, which must be applied after the other rules since rules 1 and 2 produce quantified variables.

# <li value="4">If a formula contains no free set variables other than <math>x_1, \dots, x_n,</math> then bound variables that are nested within <math>q</math> quantifiers are replaced with {{nowrap|<math>x_{n+q}</math>.}} These variables have ''(quantifier) nesting depth'' <math>q</math>.</li>

{{Anchor|Ex2}}
:{| class="wikitable"
|- style="text-align: left; vertical-align: top; style="background: white" 
|'''Example 2:''' {{space|thin}}Rule 4 is applied to the formula <math>\phi(x_1)</math> that defines the class consisting of all sets of the form <math>\{\empty, \{\empty, \dots\}, \dots\}.</math> That is, sets that contain at least <math>\empty</math> and a set containing <math>\empty</math> — for example, <math>\{\empty, \{\empty, a, b, c\}, d, e\}</math> where <math>a, b, c, d,</math> and <math>e</math> are sets.

<math display="block">\begin{align}
\phi(x_1) \,&=\, \exists u\;\,[\,u \in x_1 \,\land\, \neg\exists v\;\,(\;v\, \in \,u\,)] \,\land\, \,\exists w\;\bigl(w \in x_1 \,\land\, \exists y\;\,[(\;y\, \in w \;\land\; \neg\exists z\;\,(\;z\, \in \,y\,)]\bigr) \\
\phi_r(x_1) \, &=\, \exists x_2[x_2 \!\in\! x_1 \,\land\, \neg\exists x_3(x_3 \!\in\! x_2)] \,\land\, \,\exists x_2\bigl(x_2 \!\in\! x_1 \,\land\, \exists x_3[(x_3 \!\in\! x_2 \,\land\, \neg\exists x_4(x_4 \!\in\! x_3)]\bigr)
\end{align}</math>

Since <math>x_1</math> is the only free variable, <math>n = 1.</math> The quantified variable <math>x_3</math> appears twice in <math>x_3 \in x_2</math> at nesting depth 2. Its subscript is 3 because <math>n+q = 1+2 = 3.</math> If two quantifier scopes are at the same nesting depth, they are either identical or disjoint. The two occurrences of <math>x_3</math> are in disjoint quantifier scopes, so they do not interact with each other.
|}

'''Proof of the class existence theorem.{{space|thin}}''' The proof starts by applying the transformation rules to the given formula to produce a transformed formula. Since this formula is equivalent to the given formula, the proof is completed by proving the class existence theorem for transformed formulas.

{{math proof
| title = Proof of the class existence theorem for transformed formulas
| proof = The following lemma is used in the proof.
{{math theorem | name = Expansion lemma | math_statement = Let <math>1 \le i < j \le n,</math> and let <math>P</math> be a class containing all the ordered pairs <math>(x_i, x_j)</math> satisfying <math>R(x_i, x_j).</math> That is, <math>P \supseteq \{(x_i, x_j): R(x_i, x_j)\}.</math> Then <math>P</math> can be expanded into the unique class <math>Q</math> of {{nowrap|<math>n</math>-tuples}} satisfying <math>R(x_i, x_j)</math>. That is, <math>Q = \{(x_1, \ldots , x_n): R(x_i, x_j)\}.</math>}}

Proof:
# If <math>i = 1,</math> let <math>P_1 = P.</math>{{pb}}Otherwise, <math>i > 1,</math> so components are added in front of <math>x_i\text{:}</math> apply the [[#Tuple lemma|tuple lemma]]'s statement 1 to <math>P</math> with <math>z = (x_1, \dots, x_{i-1}).</math> This produces a class <math>P_1</math> containing all the {{nowrap|<math>(i+1)</math>-tuples}} <math display="block">((x_1, \dots, x_{i-1}), x_i, x_j) = (x_1, \dots, x_{i-1}, x_i, x_j)</math> satisfying <math>R(x_i, x_j).</math>
# If <math>j = i + 1,</math> let <math>P_2 = P_1.</math>{{pb}}Otherwise, <math>j > i + 1,</math> so components are added between <math>x_i</math> and <math>x_j\text{:}</math> add the components <math>x_{i+1}, \dots, x_{j-1}</math> one by one using the tuple lemma's statement 2. This produces a class <math>P_2</math> containing all the {{nowrap|<math>j</math>-tuples}} <math display="block">(((\cdots((x_1, \dots, x_i), x_{i+1}), \cdots), x_{j-1}), x_j) = (x_1, \dots, x_j)</math> satisfying <math>R(x_i, x_j).</math>
# If <math>j = n,</math> let <math>P_3 = P_2.</math>{{pb}}Otherwise, <math>j < n,</math> so components are added after <math>x_j\text{:}</math> add the components <math>x_{j+1}, \dots, x_n</math> one by one using the tuple lemma's statement 3. This produces a class <math>P_3</math> containing all the {{nowrap|<math>n</math>-tuples}} <math display="block">((\cdots((x_1, \dots, x_j), x_{j+1}), \cdots), x_n) = (x_1, \dots, x_n)</math> satisfying <math>R(x_i, x_j).</math>
# Let <math>Q = P_3 \cap V^n.</math> Extensionality implies that <math>Q</math> is the unique class of {{nowrap|<math>n</math>-tuples}} satisfying <math>R(x_i, x_j).</math>

{{math theorem | name = Class existence theorem for transformed formulas | math_statement =
Let <math>\phi(x_1, \ldots, x_n, Y_1, \ldots, Y_m)</math> be a formula that:
# contains no free variables other than <math>x_1, \ldots, x_n, Y_1, \ldots, Y_m</math>;
# contains only <math>\in</math>, <math>\neg</math>, <math>\land</math>, <math>\exists</math>, set variables, and the class variables <math>Y_k</math> where <math>Y_k</math> does not appear before an <math>\in</math>{{space|hair}};
# only quantifies set variables <math>x_{n+q}</math> where <math>q</math> is the quantifier nesting depth of the variable.  
Then for all <math>Y_1, \dots, Y_m</math>, there exists a unique class <math>A</math> of {{nowrap|<math>n</math>-tuples}} such that: 
<math display="block">\forall x_1 \cdots \,\forall x_n [(x_1, \ldots , x_n) \in A \iff \phi(x_1, \ldots, x_n, Y_1, \ldots, Y_m)].</math>}}

Proof: Basis step: <math>\phi</math> has 0 logical symbols. The theorem's hypothesis implies that <math>\phi</math> is an atomic formula of the form <math>x_i \in x_j</math> or <math>x_i \in Y_k.</math>

{{plainlist|indent=0.8}}
Case 1:  If <math>\phi</math> is <math>x_i \in x_j</math>, we build the class <math>E_{i,j,n} = \{(x_1, \ldots, x_{n}): x_i \in x_j\},</math> the unique class of {{nowrap|<math>n</math>-tuples}} satisfying <math>x_i \in x_j.</math>

{{plainlist|indent=0.8}}
Case a: <math>\phi</math> is <math>x_i \in x_j</math> where <math>i < j.</math> The axiom of membership produces a class <math>P</math> containing all the ordered pairs <math>(x_i, x_j)</math> satisfying <math>x_i \in x_j.</math> Apply the expansion lemma to <math>P</math> to obtain <math>E_{i,j,n} = \{(x_1, \ldots, x_{n}): x_i \in x_j\}.</math>

Case b: <math>\phi</math> is <math>x_i \in x_j</math> where <math>i > j.</math> The axiom of membership produces a class <math>P</math> containing all the ordered pairs <math>(x_i, x_j)</math> satisfying <math>x_i \in x_j.</math> Apply the tuple lemma's statement 4 to <math>P</math> to obtain <math>P'</math> containing all the ordered pairs <math>(x_j, x_i)</math> satisfying <math>x_i \in x_j.</math> Apply the expansion lemma to <math>P'</math> to obtain <math>E_{i,j,n} = \{(x_1, \ldots, x_{n}): x_i \in x_j\}.</math>

Case c: <math>\phi</math> is <math>x_i \in x_j</math> where <math>i = j.</math> Since this formula is false by the [[#Axiom of regularity|axiom of regularity]], no {{nowrap|<math>n</math>-tuples}} satisfy it, so <math>E_{i,j,n} = \empty.</math>
{{endplainlist}}

Case 2: If <math>\phi</math> is <math>x_i \in Y_k</math>, we build the class <math>E_{i,Y_k,n} = \{(x_1, \ldots, x_{n}): x_i \in Y_k\},</math> the unique class of {{nowrap|<math>n</math>-tuples}} satisfying <math>x_i \in Y_k.</math>

{{plainlist|indent=0.8}}
Case a: <math>\phi</math> is <math>x_i \in Y_k</math> where <math>i < n.</math> Apply the axiom of product by <math>V</math> to <math>Y_k</math> to produce the class <math>P = Y_k \times V = \{(x_i, x_{i+1}): x_i \in Y_k\}.</math> Apply the expansion lemma to <math>P</math> to obtain <math>E_{i,Y_k,n} = \{(x_1, \ldots, x_{n}): x_i \in Y_k\}.</math>

Case b: <math>\phi</math> is <math>x_i \in Y_k</math> where <math>i = n > 1.</math> Apply the axiom of product by <math>V</math> to <math>Y_k</math> to produce the class <math>P = Y_k \times V = \{(x_i, x_{i-1}): x_i \in Y_k\}.</math> Apply the tuple lemma's statement 4 to <math>P</math> to obtain <math>P' = V \times Y_k = \{(x_{i-1}, x_i): x_i \in Y_k\}.</math> Apply the expansion lemma to <math>P'</math> to obtain <math>E_{i,Y_k,n} = \{(x_1, \ldots, x_{n}): x_i \in Y_k\}.</math>

Case c: <math>\phi</math> is <math>x_i \in Y_k</math> where <math>i = n = 1.</math> Then <math>E_{i,Y_k,n} = Y_k.</math>
{{endplainlist}}
{{endplainlist}}

Inductive step: <math>\phi</math> has <math>k</math> logical symbols where <math>k>0</math>. Assume the induction hypothesis that the theorem is true for all <math>\psi</math> with less than <math>k</math> logical symbols. We now prove the theorem for <math>\phi</math> with <math>k</math> logical symbols. In this proof, the list of class variables <math>Y_1, \dots, Y_m</math> is abbreviated by <math>\vec{Y}</math>, so a formula—such as <math>\phi(x_1, \dots, x_n, Y_1, \dots, Y_m)</math>—can be written as <math>\phi(x_1, \dots, x_n, \vec{Y}).</math>

{{plainlist|indent=0.8}}
Case 1: <math>\phi(x_1, \ldots, x_n, \vec{Y}) = \neg \psi(x_1, \ldots, x_n, \vec{Y}).</math> Since <math>\psi</math> has <math>k-1</math> logical symbols, the induction hypothesis implies that there is a unique class <math>A</math> of {{nowrap|<math>n</math>-tuples}} such that:
<math display="block">\quad(x_1, \ldots , x_n) \in A \iff \psi(x_1, \ldots, x_n, \vec{Y}).</math> 
By the complement axiom, there is a class <math>\complement A</math> such that <math>\forall u\,[u\in \complement A \iff \neg(u \in A)].</math> However, <math>\complement A</math> contains elements other than {{nowrap|<math>n</math>-tuples}} if <math>n > 1.</math> To eliminate these elements, use <math>\complement_{V^n} A =\, </math><math>\complement A \cap V^n =\,</math><math>V^n \setminus A,</math> which is the complement relative to the class <math>V^n</math> of all {{nowrap|<math>n</math>-tuples.}}{{efn|name=Bourbaki}} Then, by extensionality, <math>\complement_{V^n} A</math> is the unique class of {{nowrap|<math>n</math>-tuples}} such that:
<math display="block">\begin{alignat}{2}
\quad&(x_1, \ldots, x_n) \in \complement_{V^n} A &&\iff \neg [(x_1, \ldots , x_n) \in A] \\
& &&\iff \neg \psi(x_1, \ldots, x_n, \vec{Y}) \\
& &&\iff \phi(x_1, \ldots, x_n, \vec{Y}). 
\end{alignat}</math>

Case 2: <math>\phi(x_1, \ldots, x_n, \vec{Y}) = \psi_1(x_1, \ldots, x_n, \vec{Y}) \land \psi_2(x_1, \ldots, x_n, \vec{Y}).</math> Since both <math>\psi_1</math> and <math>\psi_2</math> have less than <math>k</math> logical symbols, the induction hypothesis implies that there are unique classes of {{nowrap|<math>n</math>-tuples,}} <math>A_1</math> and <math>A_2</math>, such that:
:<math>\begin{align}
\quad&(x_1, \ldots , x_n) \in A_1 \iff \psi_1(x_1, \ldots, x_n, \vec{Y}). \\
&(x_1, \ldots , x_n) \in A_2 \iff \psi_2(x_1, \ldots, x_n, \vec{Y}).
\end{align}</math>
By the axioms of intersection and extensionality, <math>A_1 \cap A_2</math> is the unique class of {{nowrap|<math>n</math>-tuples}} such that:
<math display="block">\begin{alignat}{2}
\quad&(x_1, \ldots, x_n) \in A_1 \cap A_2 &&\iff (x_1, \ldots, x_n) \in A_1 \land (x_1, \ldots, x_n) \in A_2 \\
& &&\iff \psi_1(x_1, \ldots, x_n, \vec{Y}) \land \psi_2(x_1, \ldots, x_n, \vec{Y}) \\
& &&\iff  \phi(x_1, \ldots, x_n, \vec{Y}).
\end{alignat}</math>

Case 3: <math>\phi(x_1, \ldots, x_n, \vec{Y}) = \exists x_{n+1} \psi(x_1, \ldots, x_n, x_{n+1}, \vec{Y}).</math> The quantifier nesting depth of <math>\psi</math> is one more than that of <math>\phi</math> and the additional free variable is <math>x_{n+1}.</math> Since <math>\psi</math> has <math>k-1</math> logical symbols, the induction hypothesis implies that there is a unique class <math>A</math> of {{nowrap|<math>(n+1)</math>-tuples}} such that:
<math display="block">\quad(x_1, \ldots, x_n, x_{n+1}) \in A \iff \psi(x_1, \ldots, x_n, x_{n+1}, \vec{Y}).</math>
By the axioms of domain and extensionality, <math>Dom(A)</math> is the unique class of {{nowrap|<math>n</math>-tuples}} such that:{{efn|One detail has been left out of this proof. Gödel's convention is being used, so <math>\exist x\, \phi(x)</math> is defined to be <math>\exist x[\exist C (x \in C) \land \phi(x)].</math> Since this formula quantifies over classes, it must be replaced with the equivalent <math>\exist x[x \in V \land \phi(x)].</math> Then the three formulas in the proof having the form <math>\exist x_{n+1}[x_{n+1} \land \dots]</math> become <math>\exist x_{n+1}[x_{n+1} \in V \land \dots],</math> which produces a valid proof.}}
<math display="block">\begin{alignat}{2}
\quad&(x_1, \ldots, x_n) \in Dom(A) &&\iff \exists x_{n+1}[((x_1, \ldots, x_n), x_{n+1}) \in A] \\
& &&\iff \exists x_{n+1}[(x_1, \ldots, x_n, x_{n+1}) \in A] \\
& &&\iff \exists x_{n+1}\,\psi(x_1, \ldots, x_n, x_{n+1}, \vec{Y}) \\
& &&\iff \phi(x_1, \ldots, x_n, \vec{Y}). 
\end{alignat}</math>
{{endplainlist}}
}}

Gödel pointed out that the class existence theorem "is a [[metatheorem]], that is, a theorem about the system [NBG], not in the system …"<ref>{{harvnb|Gödel|1940|p=11}}.</ref> It is a theorem about NBG because it is proved in the [[metatheory]] by induction on NBG formulas. Also, its proof—instead of invoking finitely many NBG axioms—inductively describes how to use NBG axioms to construct a class satisfying a given formula. For every formula, this description can be turned into a constructive existence proof that is in NBG. Therefore, this metatheorem can generate the NBG proofs that replace
uses of NBG's class existence theorem.

A [[Recursion (computer science)|recursive]] [[computer program]] succinctly captures the construction of a class from a given formula. The definition of this program does not depend on the proof of the class existence theorem. However, the proof is needed to prove that the class constructed by the program satisfies the given formula and is built using the axioms. This program is written in [[pseudocode]] that uses a [[Pascal (programming language)|Pascal]]-style [[case statement]].{{efn|Recursive computer programs written in pseudocode have been used elsewhere in [[pure mathematics]]. For example, they have been used to prove the [[Heine-Borel theorem]] and other theorems of [[Analysis (math)|analysis]].<ref>{{harvnb|Gray|1991}}.</ref>}}
<math display="block">\begin{array}{l}
\mathbf{function} \;\text{Class}(\phi, \,n) \\
\quad\begin{array}{rl}
\mathbf{input}\!: \;\,&\phi \text{ is a transformed formula of the form } \phi(x_1, \ldots, x_n, Y_1, \ldots, Y_m); \\
&n \text{ specifies that a class of } n\text{-tuples is returned.} \\
\;\;\;\;\mathbf{output}\!: \;\,&\text{class } A \text{ of } n\text{-tuples satisfying } \\
&\,\forall x_1 \cdots \,\forall x_n [(x_1, \ldots , x_n) \in A \iff \phi(x_1, \ldots, x_n, Y_1, \ldots, Y_m)].
\end{array}
\\
\mathbf{begin} \\
\quad \mathbf{case} \;\phi \;\mathbf{of} \\
\qquad \begin{alignat}{2}
x_i \in x_j: \;\;&\mathbf{return} \;\,E_{i,j,n}; &&\text{// } E_{i,j,n} \;\,= \{(x_1, \dots, x_n): x_i \in x_j\} \\
x_i \in Y_k: \;\;&\mathbf{return} \;\,E_{i,Y_k,n}; &&\text{// } E_{i,Y_k,n} = \{(x_1, \dots, x_{n}): x_i \in Y_k\} \\
\neg\psi: \;\;&\mathbf{return} \;\,\complement_{V^n}\text{Class}(\psi, \,n);  &&\text{// } \complement_{V^n}\text{Class}(\psi, \,n) = V^n \setminus \text{Class}(\psi, \,n) \\
\psi_1 \land \psi_2: \;\;&\mathbf{return} \;\,\text{Class}(\psi_1, \,n) \cap \text{Class}(\psi_2, \,n);&& \\
\;\;\;\;\,\exists x_{n+1}(\psi): \;\;&\mathbf{return} \;\,Dom(\text{Class}(\psi, \,n+1));  &&\text{// } x_{n+1} \text{ is free in } \psi; \text{ Class}(\psi, \,n+1) \\
&\ &&\text{// returns a class of } (n+1)\text{-tuples}
\end{alignat} \\
\quad \mathbf{end} \\
\mathbf{end}
\end{array}</math>

{{Anchor|Mirror}}Let <math>\phi</math> be the formula of [[#Ex2|example 2]]. The function call <math>A = Class(\phi, 1)</math> generates the class <math>A,</math> which is compared below with <math>\phi.</math> This shows that the construction of the class <math>A</math> mirrors the construction of its defining formula <math>\phi.</math>

<math display="block">\begin{alignat}{2}
&\phi \;&&=
\;\;\exists x_2\,(x_2 \!\in\! x_1 \land \;\;\neg\;\;\;\;\exists x_3\;(x_3 \!\in\! x_2)) \,\land \;\;\,\exists x_2\,(x_2 \!\in\! x_1 \land 
\;\;\,\exists x_3\,(x_3 \!\in\! x_2 \,\land\;\;\neg\;\;\;\;\exists x_4\;(x_4 \!\in\! x_3))) \\
&A \;&&=
Dom\,(\;E_{2,1,2}\; \cap \;\complement_{V^2}\,Dom\,(\;E_{3,2,3}\;)) \,\cap\, Dom\,(\;E_{2,1,2}\;\cap \,
Dom\,(\;\,E_{3,2,3}\; \cap \;\complement_{V^3}\,Dom\,(\;E_{4,3,4}\;)))
\end{alignat}</math>

=== Extending the class existence theorem ===
Gödel extended the class existence theorem to formulas <math>\phi</math> containing [[Finitary relation|relation]]s over classes (such as <math>Y_1 \subseteq Y_2</math> and the [[unary relation]] <math>M(Y_1)</math>), special classes (such as <math>Ord</math>{{space|hair|2}}), and [[operation (mathematics)|operation]]s (such as <math>(x_1, x_2)</math> and <math>x_1 \cap Y_1</math>).<ref>{{harvnb|Gödel|1940|pp=11&ndash;13}}.</ref> To extend the class existence theorem, the formulas defining relations, special classes, and operations must quantify only over sets. Then <math>\phi</math> can be transformed into an equivalent formula satisfying the [[#CET|hypothesis of the class existence theorem]].

The following definitions specify how formulas define relations, special classes, and operations:
# A relation <math>R</math> is defined by: <math>R(Z_1, \dots, Z_k) \iff \psi_R(Z_1, \dots, Z_k).</math>
# A special class <math>C</math> is defined by: <math>u \in C \iff \psi_C(u).</math>
# An operation <math>P</math> is defined by: <math>u \in P(Z_1, \dots, Z_k) \iff \psi_P(u, Z_1, \dots, Z_k).</math>

A {{em|[[Term (logic)|term]]}} is defined by:
# Variables and special classes are terms.
# If <math>P</math> is an operation with <math>k</math> arguments and <math>\Gamma_1, \dots, \Gamma_k</math> are terms, then <math>P(\Gamma_1, \dots, \Gamma_k)</math> is a term.

The following transformation rules eliminate relations, special classes, and operations. Each time rule 2b, 3b, or 4 is applied to a subformula, <math>i</math> is chosen so that <math>z_i</math> differs from the other variables in the current formula. The rules are repeated until there are no subformulas to which they can be applied. <math>\, \Gamma_1, \dots, \Gamma_k, \Gamma,</math> and <math>\Delta</math> denote terms.

# A relation <math>R(Z_1, \dots, Z_k)</math> is replaced by its defining formula <math>\psi_R(Z_1, \dots, Z_k).</math>
# Let <math>\psi_C(u)</math> be the defining formula for the special class <math>C.</math> {{ordered list|type=lower-alpha 
 | <math>\Delta \in C</math> is replaced by <math>\psi_C(\Delta).</math>
 | <math>C \in \Delta</math> is replaced by <math>\exists z_i[z_i = C \land z_i \in \Delta].</math>}}
# Let <math>\psi_P(u, Z_1, \dots, Z_k)</math> be the defining formula for the operation <math>P(Z_1, \dots, Z_k).</math> {{ordered list|type=lower-alpha 
 | <math>\Delta \in P(\Gamma_1, \dots, \Gamma_k)</math> is replaced by <math>\psi_P(\Delta, \Gamma_1, \dots, \Gamma_k).</math>
 | <math>P(\Gamma_1, \dots, \Gamma_k) \in \Delta</math> is replaced by <math>\exists z_i[z_i = P(\Gamma_1, \dots, \Gamma_k) \land z_i \in \Delta].</math>}} 
# Extensionality is used to transform <math>\Delta = \Gamma</math> into <math>\forall z_i(z_i \in \Delta \iff z_i \in \Gamma).</math>

:{| class="wikitable"
|- style="text-align: left; vertical-align: top; style="background: white" 
|'''Example 3:{{space|thin}}''' Transforming <math>Y_1 \subseteq Y_2.</math>
<math>Y_1 \subseteq Y_2 \iff \forall z_1(z_1 \in Y_1 \implies z_1 \in Y_2) \quad\text{(rule 1)}</math>
|}

:{| class="wikitable"
|- style="text-align: left; vertical-align: top; style="background: white" 
|'''Example 4:{{space|thin}}''' Transforming <math>x_1 \cap Y_1 \in x_2.</math>
<math>\begin{alignat}{2}
x_1 \cap Y_1 \in x_2 &\iff \exists z_1[z_1 = x_1 \cap Y_1 \,\land\, z_1 \in x_2] &&\text{(rule 3b)} \\
&\iff \exists z_1[\forall z_2(z_2 \in z_1 \iff z_2 \in x_1 \cap Y_1) \,\land\, z_1 \in x_2] &&\text{(rule 4)} \\
&\iff \exists z_1[\forall z_2(z_2 \in z_1 \iff z_2 \in x_1 \land z_2 \in Y_1) \,\land\, z_1 \in x_2] \quad&&\text{(rule 3a)} \\
\end{alignat}</math>

This example illustrates how the transformation rules work together to eliminate an operation.
|}

{{math theorem | name = Class existence theorem (extended version) | math_statement = Let <math>\phi(x_1, \dots, x_n, Y_1, \dots, Y_m)</math> be a formula that quantifies only over sets, contains no free variables other than <math>x_1, \dots, x_n,  Y_1, \dots, Y_m</math>, and may contain relations, special classes, and operations defined by formulas that quantify only over sets. Then for all <math>Y_1, \dots, Y_m,</math> there exists a unique class <math>A</math> of {{nowrap|<math>n</math>-tuples}} such that <math display="block">\forall x_1 \cdots \,\forall x_n [(x_1, \dots , x_n) \in A \iff \phi(x_1, \dots, x_n, Y_1, \dots, Y_m)].</math>{{efn|This theorem is Gödel's theorem M4. He proved it by first proving M1, a class existence theorem that uses symbols for special classes rather than free class variables. M1 produces a class containing all the {{nowrap|<math>n</math>-tuples}} satisfying <math>\phi</math>, but which may contain elements that are not {{nowrap|<math>n</math>-tuples}}. Theorem M2 extends this theorem to formulas containing relations, special classes, and operations. Theorem M3 is obtained from M2 by replacing the symbols for special classes with free variables. Gödel used M3 to define <math display="block">A \times B = \{x: \exists y \exists z[x = (y, z) \land y \in A \land z \in B]\},</math> which is unique by extensionality. He used <math>A \times B</math> to define <math>V^n.</math> Theorem M4 is obtained from M3 by intersecting the class produced by M3 with <math>V^n</math> to produce the unique class of {{nowrap|<math>n</math>-tuples}} satisfying the given formula. Gödel's approach, especially his use of M3 to define <math>A \times B</math>, eliminates the need for Bernays' stronger form of the product by <math>V</math> axiom.<ref>{{harvnb|Gödel|1940|pp=8&ndash;15}}.</ref>}}}}

{{math proof | proof = Apply the transformation rules to <math>\phi</math> to produce an equivalent formula containing no relations, special classes, or operations. This formula satisfies the hypothesis of the class existence theorem. Therefore, for all <math>Y_1, \dots, Y_m,</math> there is a unique class <math>A</math> of {{nowrap|<math>n</math>-tuples}} satisfying <math display="block">\forall x_1 \cdots \,\forall x_n [(x_1, \dots, x_n) \in A \iff \phi(x_1, \dots, x_n, Y_1, \dots, Y_m)].</math>}}

=== Set axioms ===
The axioms of pairing and regularity, which were needed for the proof of the class existence theorem, have been given above. NBG contains four other set axioms. Three of these axioms deal with class operations being applied to sets.

'''Definition.{{space|thin}}''' <math>F</math> is a [[Function (set theory)|function]] if <math display="block">F \subseteq V^2 \land \forall x\, \forall y\, \forall z\, [(x,y) \in F \,\land\, (x,z) \in F \implies y = z].</math>

In set theory, the definition of a function does not require specifying the domain or codomain of the function (see [[Function (set theory)]]). NBG's definition of function generalizes ZFC's definition from a set of ordered pairs to a class of ordered pairs.

ZFC's definitions of the set operations of [[Image (set theory)|image]], [[Union (set theory)|union]], and [[power set]] are also generalized to class operations. The image of class <math>A</math> under the function <math>F</math> is <math>F[A] = \{y: \exists x(x \in A \,\land\, (x, y) \in F)\}.</math> This definition does not require that <math>A \subseteq Dom(F).</math> The union of class <math>A</math> is <math>\cup A = \{x: \exists y(x \in y\, \,\land\, y \in A)\}.</math> The power class of <math>A</math> is <math>\mathcal{P}(A) = \{x: x \subseteq A\}.</math> The extended version of the class existence theorem implies the existence of these classes. The axioms of replacement, [[Axiom of union|union]], and [[Axiom of power set|power set]] imply that when these operations are applied to sets, they produce sets.<ref>{{harvnb|Gödel|1940|pp=16&ndash;18}}.</ref>

{{Anchor|NBG's axiom of replacement}}'''Axiom of replacement.{{space|thin}}''' If <math>F</math> is a function and <math>a</math> is a set, then <math>F[a]</math>, the [[Image (set theory)|image]] of <math>a</math> under <math>F</math>, is a set.
<math display="block">\forall F \,\forall a \,[F \text{ is a function}\implies \exists b \,\forall y\,(y \in b \iff \exists x(x \in a \,\land\, (x, y) \in F))].</math>

Not having the requirement <math>A \subseteq Dom(F)</math> in the definition of <math>F[A]</math> produces a stronger axiom of replacement, which is used in the following proof.

{{Anchor|NBG's axiom of separation}}{{math theorem | name = Theorem (NBG's [[axiom of separation]]) | math_statement = If <math>a</math> is a set and <math>B</math> is a subclass of <math>a,</math> then <math>B</math> is a set.}}
{{math proof | proof = The class existence theorem constructs the [[Restriction (mathematics)|restriction]] of the [[identity function]] to <math>B</math>: <math>I{\restriction_B} = \{(x_1, x_2): x_1 \in B \land x_2 = x_1\}.</math> Since the image of <math>a</math> under <math>I{\restriction_B}</math> is <math>B</math>, the axiom of replacement implies that <math>B</math> is a set. This proof depends on the definition of image not having the requirement <math>a \subseteq Dom(F)</math> since <math>Dom(I{\restriction_B}) = B \subseteq a</math> rather than <math>a \subseteq Dom(I{\restriction_B}).</math>}}

'''Axiom of union.{{space|thin}}''' If <math>a</math> is a set, then there is a set containing <math>\cup a.</math>
<math display="block">\forall a\, \exists b\, \forall x\,[\,\exists y(x \in y\, \,\land\, y \in a) \implies x \in b\,].</math>

'''Axiom of power set.{{space|thin}}''' If <math>a</math> is a set, then there is a set containing <math>\mathcal{P}(a).</math>
:<math>\forall a\, \exists b\, \forall x\, (x \subseteq a \implies x \in b).</math>{{efn|Gödel weakened Bernays' axioms of union and power set, which state the existence of these sets, to the above axioms that state there is a set containing the union and a set containing the power set.<ref>{{harvnb|Bernays|1941|p=2}}; {{harvnb|Gödel|1940|p=5}}).</ref> Bernays published his axioms after Gödel, but had sent them to Gödel in 1931.<ref name="auto">{{harvnb|Kanamori|2009|p=48}}; {{harvnb|Gödel|2003|pp=104&ndash;115}}.</ref>}}

{{math theorem | If <math>a</math> is a set, then <math>\cup a</math> and <math>\mathcal{P}(a)</math> are sets.}}
{{math proof | proof = The axiom of union states that <math>\cup a</math> is a subclass of a set <math>b</math>, so the axiom of separation implies <math>\cup a</math> is a set. Likewise, the axiom of power set states that <math>\mathcal{P}(a)</math> is a subclass of a set <math>b</math>, so the axiom of separation implies that  <math>\mathcal{P}(a)</math> is a set.}}

{{anchor|Axiom of infinity}}'''Axiom of infinity.{{space|thin}}''' There exists a nonempty set <math>a</math> such that for all <math>x</math> in <math>a</math>, there exists a <math>y</math> in <math>a</math> such that <math>x</math> is a proper subset of <math>y</math>.
<math display="block">\exists a\, [\exists u(u \in a) \,\land\, \forall x(x \in a \implies \exists y(y \in a \,\land\, x \subset y))].</math>

The axioms of infinity and replacement prove the existence of the [[empty set]]. In the [[#Empty class|discussion of the class existence axioms]], the existence of the empty class <math>\empty</math> was proved. We now prove that <math>\empty</math> is a set. Let function <math>F = \empty</math> and let <math>a</math> be the set given by the axiom of infinity. By replacement, the image of <math>a</math> under <math>F</math>, which equals <math>\empty</math>, is a set.

NBG's axiom of infinity is implied by ZFC's [[axiom of infinity]]: <math>\,\exists a\, [\empty \in a \,\land\, \forall x(x \in a \implies x \cup \{x\} \in a)].\,</math> The first [[Conjunct (logic)|conjunct]] of ZFC's axiom, <math>\empty \in a</math>, implies the first conjunct of NBG's axiom. The second conjunct of ZFC's axiom, <math>\forall x(x \in a \implies x \cup \{x\} \in a)</math>, implies the second conjunct of NBG's axiom since <math>x \subset x \cup \{x\}.</math> To prove ZFC's axiom of infinity from NBG's axiom of infinity requires some of the other NBG axioms (see [[Weak axiom of infinity]]).{{efn|Since ZFC's axiom requires the existence of the empty set, an advantage of NBG's axiom is that the axiom of the empty set is not needed. Mendelson's axiom system uses the ZFC's axiom of infinity and also has the axiom of the empty set.<ref>{{harvnb|Mendelson|1997|pp=228, 239}}.</ref>}}

=== Axiom of global choice ===
The class concept allows NBG to have a stronger axiom of choice than ZFC. A [[choice function]] is a function <math>f</math> defined on a set <math>s</math> of nonempty sets such that <math>f(x) \in x</math> for all <math>x \in s.</math> ZFC's axiom of choice states that there exists a choice function for every set of nonempty sets. A global choice function is a function <math>G</math> defined on the class of all nonempty sets such that <math>G(x) \in x</math> for every nonempty set <math>x.</math> The axiom of global choice states that there exists a global choice function. This axiom implies ZFC's axiom of choice since for every set <math>s</math> of nonempty sets, <math>G\vert_s</math> (the [[Restriction (mathematics)|restriction]] of <math>G</math> to <math>s</math>) is a choice function for <math>s.</math> In 1964, [[William Bigelow Easton|William B. Easton]] proved that global choice is stronger than the axiom of choice by using [[Forcing (mathematics)|forcing]] to construct a [[Model (mathematical logic)|model]] that satisfies the axiom of choice and all the axioms of NBG except the axiom of global choice.<ref>{{harvnb|Easton|1964|pp=56a&ndash;64}}.</ref> The axiom of global choice is equivalent to every class having a well-ordering, while ZFC's axiom of choice is equivalent to every set having a well-ordering.{{efn|For <math>V</math> having a well-ordering implying global choice, see [[Implications of the axiom of limitation of size]]. For global choice implying the well-ordering of any class, see {{harvnb|Kanamori|2009|p=53}}.}}

'''Axiom of global choice.{{space|thin}}''' There exists a function that chooses an element from every nonempty set.
:<math>\exists G\,[G \text{ is a function}\, \land \forall x(x \ne \empty \implies \exists y(y \in x \land (x,y) \in G))].</math>

==History==
[[File:NBG Evolution svg.svg|thumb|400px|alt=refer to caption|History of approaches that led to NBG set theory]]

=== Von Neumann's 1925 axiom system ===
Von Neumann published an introductory article on his axiom system in 1925. In 1928, he provided a detailed treatment of his system.<ref>{{harvnb|von Neumann|1925}}, {{harvnb|von Neumann|1928}}.</ref> Von Neumann based his axiom system on two domains of [[Primitive notion|primitive]] objects: functions and arguments. These domains overlap—objects that are in both domains are called argument-functions. Functions correspond to classes in NBG, and argument-functions correspond to sets. Von Neumann's primitive operation is [[function application]], denoted by [''a'',&nbsp;''x''] rather than ''a''(''x'') where ''a'' is a function and ''x'' is an argument. This operation produces an argument. Von Neumann defined classes and sets using functions and argument-functions that take only two values, ''A'' and ''B''. He defined ''x''&nbsp;∈&nbsp;''a'' if [''a'',&nbsp;''x'']&nbsp;≠&nbsp;''A''.<ref name=VN1925def />

Von Neumann's work in set theory was influenced by [[Georg Cantor]]'s articles, [[Zermelo set theory|Ernst Zermelo's 1908 axioms for set theory]], and the 1922 critiques of [[Ernst Zermelo|Zermelo]]'s set theory that were given independently by [[Abraham Fraenkel]] and [[Thoralf Skolem]]. Both Fraenkel and Skolem pointed out that Zermelo's axioms cannot prove the existence of the set {''Z''<sub>0</sub>,&nbsp;''Z''<sub>1</sub>,&nbsp;''Z''<sub>2</sub>,&nbsp;...} where ''Z''<sub>0</sub> is the set of [[natural number]]s and ''Z''<sub>''n''+1</sub> is the [[power set]] of ''Z''<sub>''n''</sub>. They then introduced the axiom of replacement, which would guarantee the existence of such sets.<ref>{{harvnb|Ferreirós|2007|p=369}}.</ref>{{efn|In 1917, [[Dmitry Mirimanoff]] published a form of replacement based on cardinal equivalence.<ref>{{harvnb|Mirimanoff|1917|p=49}}.</ref>}} However, they were reluctant to adopt this axiom: Fraenkel stated "that Replacement was too strong an axiom for 'general set theory'", while "Skolem only wrote that 'we could introduce' Replacement".<ref>{{harvnb|Kanamori|2012|p=62}}.</ref>

Von Neumann worked on the problems of [[Zermelo set theory]] and provided solutions for some of them:
* '''A theory of ordinals''' 
** Problem: Cantor's theory of [[ordinal number]]s cannot be developed in Zermelo set theory because it lacks the axiom of replacement.{{efn|name=ordinaltheorem|In 1928, von Neumann stated: "A treatment of ordinal number closely related to mine was known to Zermelo in 1916, as I learned subsequently from a personal communication. Nevertheless, the fundamental theorem, according to which to each well-ordered set there is a similar ordinal, could not be rigorously proved because the replacement axiom was unknown."<ref>{{harvnb|Hallett|1984|p=280}}.</ref>}} 
** Solution: Von Neumann recovered Cantor's theory by defining the ordinals using sets that are [[well-ordered]] by the ∈-relation,{{efn|{{harvnb|von Neumann|1923}}. Von Neumann's definition also used the theory of well-ordered sets. Later, his definition was simplified to the current one: An ordinal is a [[transitive set]] that is well-ordered by ∈.<ref>{{harvnb|Kunen|1980|p=16}}.</ref>}} and by using the axiom of replacement to prove key theorems about the ordinals, such as every well-ordered set is [[order-isomorphic]] with an ordinal.{{efn|name=ordinaltheorem}} In contrast to Fraenkel and Skolem, von Neumann emphasized how important the replacement axiom is for set theory: "In fact, I believe that no theory of ordinals is possible at all without this axiom."<ref>{{harvnb|von Neumann|1925|p=223}} (footnote); English translation: {{Harvnb|van&nbsp;Heijenoort|2002b|p=398 (footnote)}}.</ref>
* '''A criterion identifying classes that are too large to be sets''' 
** Problem: Zermelo did not provide such a criterion. His set theory avoids the large classes that lead to the [[Georg Cantor#Absolute infinite, well-ordering theorem, and paradoxes|paradoxes]], but it leaves out many sets, such as the one mentioned by Fraenkel and Skolem.{{efn|After introducing the [[cumulative hierarchy]], von Neumann could show that Zermelo's axioms do not prove the existence of ordinals α&nbsp;≥&nbsp;ω&nbsp;+&nbsp;ω, which include uncountably many [[hereditarily countable set]]s. This follows from Skolem's result that V<sub>ω+ω</sub> satisfies Zermelo's axioms<ref>{{harvnb|Kanamori|2012|p=61}}</ref> and from α&nbsp;∈&nbsp;V<sub>β</sub> implying α&nbsp;<&nbsp;β.<ref>{{harvnb|Kunen|1980|pp=95&ndash;96}}. Uses the notation R(β) instead of ''V''<sub>β</sub>.</ref>}} 
** Solution: Von Neumann introduced the criterion: A class is too large to be a set if and only if it can be mapped [[onto]] the class ''V'' of all sets. Von Neumann realized that the set-theoretic paradoxes could be avoided by not allowing such large classes to be members of any class. Combining this restriction with his criterion, he obtained his [[axiom of limitation of size]]: A class ''C'' is not a member of any class if and only if ''C'' can be mapped onto ''V''.<ref>{{harvnb|Hallett|1984|pp=288&ndash;290}}.</ref>{{efn|Von Neumann stated his axiom in an equivalent functional form.<ref>{{harvnb|von Neumann|1925|p=225}}; English translation: {{Harvnb|van&nbsp;Heijenoort|2002b|p=400}}.</ref>}}
* '''Finite axiomatization''' 
** Problem: Zermelo had used the imprecise concept of "definite [[propositional function]]" in [[Zermelo set theory#The axioms of Zermelo set theory|his axiom of separation]].
** Solutions: Skolem introduced the [[axiom schema of separation]] that was later used in ZFC, and Fraenkel introduced an equivalent solution.<ref>Fraenkel, ''Historical Introduction'' in {{harvnb|Bernays|1991|p=13}}.</ref> However, Zermelo rejected both approaches "particularly because they implicitly involve the concept of natural number which, in Zermelo's view, should be based upon set theory."{{efn|Skolem's approach implicitly involves natural numbers because the formulas of an axiom schema are built using [[structural recursion]], which is a generalization of [[mathematical recursion]] over the natural numbers.}} Von Neumann avoided [[axiom schema]]s by formalizing the concept of "definite propositional function" with his functions, whose construction requires only finitely many axioms. This led to his set theory having finitely many axioms.<ref>{{harvnb|von Neumann|1925|pp=224&ndash;226}}; English translation: {{Harvnb|van&nbsp;Heijenoort|2002b|pp=399&ndash;401}}.</ref> In 1961, [[Richard Montague]] proved that ZFC cannot be finitely axiomatized.<ref>{{harvnb|Montague|1961}}.</ref>
* '''The axiom of regularity''' 
** Problem: Zermelo set theory starts with the empty set and an infinite set, and iterates the axioms of pairing, union, power set, separation, and choice to generate new sets. However, it does not restrict sets to these. For example, it allows sets that are not [[well-founded set|well-founded]], such as a set ''x'' satisfying ''x''&nbsp;∈&nbsp;''x''.{{efn|Mirimanoff defined well-founded sets in 1917.<ref>{{harvnb|Mirimanoff|1917|p=41}}.</ref>}} 
** Solutions: Fraenkel introduced an axiom to exclude these sets. Von Neumann analyzed Fraenkel's axiom and stated that it was not "precisely formulated", but it would approximately say: "Besides the sets ... whose existence is absolutely required by the axioms, there are no further sets."<ref>{{harvnb|von Neumann|1925|pp=230&ndash;232}}; English translation: {{Harvnb|van&nbsp;Heijenoort|2002b|pp=404&ndash;405}}.</ref> Von Neumann proposed the axiom of regularity as a way to exclude non-well-founded sets, but did not include it in his axiom system. In 1930, Zermelo became the first to publish an axiom system that included regularity.{{efn|[[Akihiro Kanamori]] points out that Bernays lectured on his axiom system in 1929-1930 and states that "… he and Zermelo must have arrived at the idea of incorporating Foundation [regularity] almost at the same time."<ref>{{harvnb|Kanamori|2009|pp=53&ndash;54}}.</ref> However, Bernays did not publish the part of his axiom system containing regularity until 1941.<ref>{{harvnb|Bernays|1941|p=6}}.</ref>}}

=== Von Neumann's 1929 axiom system ===
[[File:JohnvonNeumann-LosAlamos.gif|thumb|upright=0.8|alt=refer to caption|John von Neumann]]

In 1929, von Neumann published an article containing the axioms that would lead to NBG. {{Anchor|von Neumann's concern}}This article was motivated by his concern about the consistency of the axiom of limitation of size. He stated that this axiom "does a lot, actually too much." Besides implying the axioms of separation and replacement, and the [[well-ordering theorem]], it also implies that any class whose [[cardinality]] is less than that of ''V'' is a set. Von Neumann thought that this last implication went beyond Cantorian set theory and concluded: "We must therefore discuss whether its [the axiom's] consistency is not even more problematic than an axiomatization of set theory that does not go beyond the necessary Cantorian framework."<ref>{{harvnb|von Neumann|1929|p=229}}; {{harvnb|Ferreirós|2007|pp=379&ndash;380}}.</ref>

Von Neumann started his consistency investigation by introducing his 1929 axiom system, which contains all the axioms of his 1925 axiom system except the axiom of limitation of size. He replaced this axiom with two of its consequences, the axiom of replacement and a choice axiom. Von Neumann's choice axiom states: "Every relation ''R'' has a subclass that is a function with the same domain as ''R''."<ref>{{harvnb|Kanamori|2009|pp=49, 53}}.</ref>

Let ''S'' be von Neumann's 1929 axiom system. Von Neumann introduced the axiom system ''S'' + Regularity (which consists of ''S'' and the axiom of regularity) to demonstrate that his 1925 system is [[relative consistency|consistent relative]] to ''S''. He proved:
# If ''S'' is consistent, then ''S'' + Regularity is consistent.
# ''S'' + Regularity implies the axiom of limitation of size. Since this is the only axiom of his 1925 axiom system that ''S'' + Regularity does not have, ''S'' + Regularity implies all the axioms of his 1925 system. 
These results imply: If ''S'' is consistent, then von Neumann's 1925 axiom system is consistent. Proof: If ''S'' is consistent, then ''S'' + Regularity is consistent (result 1). Using [[proof by contradiction]], assume that the 1925 axiom system is inconsistent, or equivalently: the 1925 axiom system implies a contradiction. Since ''S'' + Regularity implies the axioms of the 1925 system (result 2), ''S'' + Regularity also implies a contradiction. However, this contradicts the consistency of ''S'' + Regularity. Therefore, if ''S'' is consistent, then von Neumann's 1925 axiom system is consistent.

Since ''S'' is his 1929 axiom system, von Neumann's 1925 axiom system is consistent relative to his 1929 axiom system, which is closer to Cantorian set theory. The major differences between Cantorian set theory and the 1929 axiom system are classes and von Neumann's choice axiom. The axiom system ''S'' + Regularity was modified by Bernays and Gödel to produce the equivalent NBG axiom system.

=== Bernays' axiom system ===
[[File:ETH-BIB-Bernays, Paul (1888-1977)-Portrait-Portr 00025 (cropped).tif|thumb|upright=0.8|Paul Bernays]]
In 1929, [[Paul Bernays]] started modifying von Neumann's new axiom system by taking classes and sets as primitives. He published his work in a series of articles appearing from 1937 to 1954.<ref>{{harvnb|Kanamori|2009|pp=48, 58}}. Bernays' articles are reprinted in {{harvnb|Müller|1976|pp=1&ndash;117}}.</ref> Bernays stated that:
{{quote|The purpose of modifying the von Neumann system is to remain nearer to the structure of the original Zermelo system and to utilize at the same time some of the set-theoretic concepts of the [[Ernst Schröder (mathematician)#Work|Schröder logic]] and of ''[[Principia Mathematica]]'' which have become familiar to logicians. As will be seen, a considerable simplification results from this arrangement.<ref>{{harvnb|Bernays|1937|p=65}}.</ref>}}
Bernays handled sets and classes in a [[Many-sorted first-order logic|two-sorted logic]] and introduced two membership primitives: one for membership in sets and one for membership in classes. With these primitives, he rewrote and simplified von Neumann's 1929 axioms. Bernays also included the axiom of regularity in his axiom system.<ref>{{harvnb|Kanamori|2009|pp=48&ndash;54}}.</ref>

=== Gödel's axiom system (NBG) ===
[[File:Kurt gödel.jpg|thumb|upright=0.8|alt=refer to caption|Kurt Gödel, {{spaces|4|hair}}{{circa}} 1926]]
In 1931, Bernays sent a letter containing his set theory to [[Kurt Gödel]].<ref name="auto"/> Gödel simplified Bernays' theory by making every set a class, which allowed him to use just one sort and one membership primitive. He also weakened some of Bernays' axioms and replaced von Neumann's choice axiom with the equivalent axiom of global choice.<ref>{{harvnb|Kanamori|2009|p=56}}.</ref>{{efn|Proof that von Neumann's axiom implies global choice: Let <math>R = \{(x, y): x \ne \empty \land y \in x\}.</math> Von Neumann's axiom implies there is a function <math>G \subseteq R</math> such that <math>Dom(G) = Dom(R).</math> The function <math>G</math> is a global choice function since for all nonempty sets <math>x,</math> <math>G(x) \in x.</math><br/> Proof that global choice implies von Neumann's axiom: Let <math>G</math> be a global choice function, and let <math>R</math> be a relation. For <math>x \in Dom(R),</math> let <math>\alpha(x) = \text{least}\,\{\alpha: \exists y[(x, y) \in R \cap V_\alpha]\}</math> where <math>V_\alpha</math> is the set of all sets having [[Rank (set theory)|rank]] less than <math>\alpha.</math> Let <math>z_x = \{y: (x, y) \in R \cap V_{\alpha(x)}\}.</math> Then <math>F = \{(x, G(z_x)): x \in Dom(R)\}</math> is a function that satisfies von Neumann's axiom since <math>F \subseteq R</math> and <math>Dom(F) = Dom(R).</math>}} Gödel used his axioms in his 1940 monograph on the relative consistency of global choice and the generalized continuum hypothesis.<ref>{{harvnb|Kanamori|2009|pp=56&ndash;58}}; {{harvnb|Gödel|1940|loc=Chapter I: The axioms of abstract set theory, pp. 3–7}}.</ref>

Several reasons have been given for Gödel choosing NBG for his monograph:{{efn|Gödel used von Neumann's 1929 axioms in his 1938 announcement of his relative consistency theorem and stated "A corresponding theorem holds if ''T'' denotes the system of ''Principia mathematica''".<ref>{{harvnb|Gödel|1990|p=26}}.</ref> His 1939 sketch of his proof is for Zermelo set theory and ZF.<ref>{{harvnb|Gödel|1990|pp=28&ndash;32}}.</ref> Proving a theorem in multiple [[formal systems]] was not unusual for Gödel. For example, he proved his [[incompleteness theorem]] for the system of ''Principia mathematica'', but pointed out that it "holds for a wide class of formal systems ...".<ref>{{harvnb|Gödel|1986|p=145}}.</ref>}}
* Gödel gave a mathematical reason—NBG's global choice produces a stronger consistency theorem: "This stronger form of the axiom [of choice], if consistent with the other axioms, implies, of course, that a weaker form is also consistent."<ref name=Godelp6/>
* [[Robert Solovay]] conjectured: "My guess is that he [Gödel] wished to avoid a discussion of the technicalities involved in developing the rudiments of [[model theory]] within axiomatic set theory."<ref>{{harvnb|Solovay|1990|p=13}}.</ref>{{efn|Gödel's consistency proof builds the [[constructible universe]]. To build this in ZF requires some model theory. Gödel built it in NBG without model theory. For Gödel's construction, see {{harvnb|Gödel|1940|pp=35&ndash;46}} or {{harvnb|Cohen|1966|pp=99&ndash;103}}.}}
* [[Kenneth Kunen]] gave a reason for Gödel avoiding this discussion: "There is also a much more combinatorial approach to '''L''' [the [[constructible universe]]], developed by ... [Gödel in his 1940 monograph] in an attempt to explain his work to non-logicians. ... This approach has the merit of removing all vestiges of logic from the treatment of '''L'''."<ref>{{harvnb|Kunen|1980|p=176}}.</ref>
* [[Charles Parsons (philosopher)|Charles Parsons]] provided a philosophical reason for Gödel's choice: "This view [that 'property of set' is a primitive of set theory] may be reflected in Gödel's choice of a theory with class variables as the framework for ... [his monograph]."<ref>{{harvnb|Gödel|1990|p=108}}, footnote i. The paragraph containing this footnote discusses why Gödel considered "property of set" a primitive of set theory and how it fit into his [[ontology]]. "Property of set" corresponds to the "class" primitive in NBG.</ref>

Gödel's achievement together with the details of his presentation led to the prominence that NBG would enjoy for the next two decades.<ref>{{harvnb|Kanamori|2009|p=57}}.</ref> In 1963, [[Paul Cohen (mathematician)|Paul Cohen]] proved his [[Independence (mathematical logic)|independence]] proofs for ZF with the help of some tools that Gödel had developed for his relative consistency proofs for NBG.<ref>{{harvnb|Cohen|1963}}.</ref> Later, ZFC became more popular than NBG.  This was caused by several factors, including the extra work required to handle [[Forcing (mathematics)|forcing]] in NBG,<ref>{{harvnb|Kanamori|2009|p=65}}: "Forcing itself went a considerable distance in downgrading any formal theory of classes because of the added encumbrance of having to specify the classes of generic extensions."</ref> Cohen's 1966 presentation of forcing, which used ZF,<ref>{{harvnb|Cohen|1966|pp=107&ndash;147}}.</ref>{{efn|Cohen also gave a detailed proof of Gödel's relative consistency theorems using ZF.<ref>{{harvnb|Cohen|1966|pp=85&ndash;99}}.</ref>}} and the proof that NBG is a conservative extension of ZFC.{{efn|In the 1960s, this conservative extension theorem was proved independently by Paul Cohen, [[Saul Kripke]], and Robert Solovay. In his 1966 book, Cohen mentioned this theorem and stated that its proof requires forcing. It was also proved independently by [[Ronald Jensen]] and Ulrich Felgner, who published his proof in 1971.<ref>{{harvnb|Ferreirós|2007|pp=381&ndash;382}}; {{harvnb|Cohen|1966|p=77}}; {{harvnb|Felgner|1971}}.</ref>}}

==NBG, ZFC, and MK==
NBG is not logically equivalent to ZFC because its language is more expressive: it can make statements about classes, which cannot be made in ZFC. However, NBG and ZFC imply the same statements about sets. Therefore, NBG is a [[conservative extension]] of ZFC. NBG implies theorems that ZFC does not imply, but since NBG is a conservative extension, these theorems must involve proper classes. For example, it is a theorem of NBG that the global axiom of choice implies that the proper class ''V'' can be well-ordered and that every proper class can be put into one-to-one correspondence with ''V''.{{efn|Both conclusions follow from the conclusion that every proper class can be put into one-to-one correspondence with the class of all ordinals. A proof of this is outlined in {{harvnb|Kanamori|2009|p=53}}.}}

One consequence of conservative extension is that ZFC and NBG are [[equiconsistent]]. Proving this uses the [[principle of explosion]]: from a [[contradiction]], everything is provable. Assume that either ZFC or NBG is inconsistent. Then the inconsistent theory implies the contradictory statements ∅&nbsp;=&nbsp;∅ and ∅&nbsp;≠&nbsp;∅, which are statements about sets. By the conservative extension property, the other theory also implies these statements. Therefore, it is also inconsistent. So although NBG is more expressive, it is equiconsistent with ZFC. This result together with von Neumann's 1929 relative consistency proof implies that his 1925 axiom system with the axiom of limitation of size is equiconsistent with ZFC. This completely resolves [[#von Neumann's concern|von Neumann's concern]] about the relative consistency of this powerful axiom since ZFC is within the Cantorian framework.

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 {{harvnb|Pudlák|1998}}.

[[Morse–Kelley set theory]] has an axiom schema of class comprehension that includes formulas whose quantifiers range over classes. MK is a stronger theory than NBG because MK proves the consistency of NBG,<ref>{{harvnb|Mostowski|1950|p=113}}, footnote 11. Footnote references [[Hao Wang (academic)|Wang]]'s NQ set theory, which later evolved into MK.</ref> while [[Gödel's second incompleteness theorem]] implies that NBG cannot prove the consistency of NBG.

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 {{harvnb|Potter|2004}}.

===Models===
ZFC, NBG, and MK have [[Model (mathematical logic)|model]]s describable in terms of the [[cumulative hierarchy]] ''V<sub>α</sub>''{{space|hair}} and the [[constructible hierarchy]] ''L<sub>α</sub>''{{space|hair}}. Let  ''V'' include an [[inaccessible cardinal]] κ, let ''X'' ⊆ ''V<sub>κ</sub>'', and let Def(''X'') denote the class of [[definable set|first-order definable subset]]s of ''X'' with parameters. In symbols where "<math>(X,\in)</math>" denotes the model with [[Model (mathematical logic)#domain|domain]] <math>X</math> and relation <math>\in</math>, and "<math>\models</math>" denotes the [[Model (mathematical logic)#Satisfaction relation|satisfaction relation]]:
<math display="block">\operatorname{Def}(X) := \Bigl\{ \{ x \mid x \in X \text{ and } (X,\in) \models \phi(x,y_1,\ldots,y_n) \}: \phi \text{ is a first-order formula and } y_{1},\ldots,y_{n} \in X \Bigr\}.</math>

Then:
* <math>(V_\kappa,\in)</math> and <math>(L_\kappa,\in)</math> are models of [[ZFC]].<ref>{{harvnb|Kanamori|2009b|pp=18, 29}}.</ref>
* (''V''<sub>κ</sub>,&nbsp;''V''<sub>κ+1</sub>,&nbsp;∈) is a model of MK where ''V''<sub>κ</sub> consists of the sets of the model and ''V''<sub>κ+1</sub> consists of the classes of the model.<ref>{{harvnb|Chuaqui|1981|p=313}} proves that (''V''<sub>κ</sub>,&nbsp;''V''<sub>κ+1</sub>,&nbsp;∈) is a model of MKTR + AxC. MKT is Tarski's axioms for MK without Choice or Replacement. MKTR + AxC is MKT with Replacement and Choice ({{harvnb|Chuaqui|1981|pp=4, 125}}), which is equivalent to MK.</ref> Since a model of MK is a model of NBG, this model is also a model of NBG. 
* (''V''<sub>κ</sub>,&nbsp;Def(''V''<sub>κ</sub>),&nbsp;∈) is a model of Mendelson's version of NBG, which replaces NBG's axiom of global choice with ZFC's axiom of choice.<ref>{{harvnb|Mendelson|1997|p=275}}.</ref> The axioms of ZFC are true in this model because (''V''<sub>κ</sub>,&nbsp;∈) is a model of ZFC. In particular, ZFC's axiom of choice holds, but NBG's global choice may fail.{{efn|Easton built a [[Axiom of limitation of size#Easton's choice model|model of Mendelson's version of NBG]] in which ZFC's axiom of choice holds but global choice fails.}} NBG's class existence axioms are true in this model because the classes whose existence they assert can be defined by first-order definitions. For example, the membership axiom holds since the class <math>E</math> is defined by: <math display="block">E = \{x \in V_\kappa: (V_\kappa,\in) \models \exists u  \ \exists v [x = (u, v) \land u \in v]\}.</math>
* (''L''<sub>κ</sub>, ''L''<sub>κ<sup>+</sup></sub>, ∈), where κ<sup>+</sup> is the [[successor cardinal]] of κ, is a model of NBG.{{efn|In the cumulative hierarchy V<sub>κ</sub>, the subsets of V<sub>κ</sub> are in V<sub>κ+1</sub>. The constructible hierarchy ''L''<sub>κ</sub> produces subsets more slowly, which is why the subsets of ''L''<sub>κ</sub> are in ''L''<sub>κ<sup>+</sup></sub> rather than ''L''<sub>κ+1</sub>.<ref>{{harvnb|Gödel|1940|p=54}}; {{harvnb|Solovay|1990|pp=9&ndash;11}}.</ref>}} NBG's class existence axioms are true in (''L''<sub>κ</sub>,&nbsp;''L''<sub>κ<sup>+</sup></sub>,&nbsp;∈). For example, the membership axiom holds since the class <math>E</math> is defined by: <math display="block">E = \{x \in L_\kappa: (L_\kappa,\in) \models \exists u  \ \exists v [x = (u, v) \land u \in v]\}.</math> So ''E''&nbsp;∈&nbsp;𝒫(''L''<sub>κ</sub>). In his proof that [[generalized continuum hypothesis|GCH]] is true in ''L'', Gödel proved that 𝒫(''L''<sub>κ</sub>)&nbsp;⊆&nbsp;''L''<sub>κ<sup>+</sup></sub>.<ref>{{harvnb|Gödel|1940|p=54}}.</ref> Therefore, ''E''&nbsp;∈&nbsp;''L''<sub>κ<sup>+</sup></sub>, so the membership axiom is true in (''L''<sub>κ</sub>,&nbsp;''L''<sub>κ<sup>+</sup></sub>,&nbsp;∈). Likewise, the other class existence axioms are true. The axiom of global choice is true because ''L''<sub>κ</sub> is well-ordered by the [[Restriction (mathematics)|restriction]] of [[#Gödel's function|Gödel's function]] (which maps the class of ordinals to the constructible sets) to the ordinals less than κ. Therefore, (''L''<sub>κ</sub>,&nbsp;''L''<sub>κ<sup>+</sup></sub>,&nbsp;∈) is a model of NBG.
* If <math>M</math> is a nonstandard model of <math>\mathrm{ZFC}</math>, then <math>(M,\mathrm{Def}(M))\vDash \mathrm{GB}+\Delta^1_1\text{-CA}</math> is equivalent to "there exists an <math>X</math> such that <math>(M,X)\vDash\mathrm{GB}+\Delta^1_1\text{-CA}</math>", where <math>\mathrm{Def}(M)</math> is the set of subsets of <math>M</math> that are definable over <math>M</math>.<ref>A. Enayat, "[https://www.sciencedirect.com/science/article/pii/S0168007222000732 Set theoretical analogues of the Barwise-Schlipf theorem]". Annals of Pure and Applied Logic vol. 173 (2022).</ref> This provides a second-order part for extending a given first-order nonstandard model of <math>\mathrm{ZFC}</math> to a nonstandard model of <math>\mathrm{GB}</math>, if there is such an extension at all.

==Category theory==
The ontology of NBG provides scaffolding for speaking about "large objects" without risking paradox. For instance, in some developments of [[category theory]], a "[[large category]]" is defined as one whose [[object (category theory)|object]]s and [[morphism]]s make up a proper class. On the other hand, a "small category" is one whose objects and morphisms are members of a set. Thus, we can speak of the "[[category of all sets]]" or "[[category of all small categories]]" without risking paradox since NBG supports large categories.

However, NBG does not support a "category of all categories" since large categories would be members of it and NBG does not allow proper classes to be members of anything. An ontological extension that enables us to talk formally about such a "category" is the [[Conglomerate (mathematics)|conglomerate]], which is a collection of classes. Then the "category of all categories" is defined by its objects: the conglomerate of all categories; and its morphisms: the conglomerate of all morphisms from ''A'' to ''B'' where ''A'' and ''B'' are objects.<ref>{{harvnb|Adámek|Herrlich|Strecker|2004|pp=15&ndash;16, 40}}.</ref> On whether an ontology including classes as well as sets is adequate for category theory, see {{harvnb|Muller|2001}}.

== Notes ==
{{Notelist}}

==References==
{{Reflist}}

==Bibliography==
* {{Citation|last1=Adámek |first1=Jiří |last2=Herrlich |first2=Horst |last3=Strecker |first3=George E. |title=Abstract and Concrete Categories (The Joy of Cats) |edition=1st |url=http://katmat.math.uni-bremen.de/acc/ |year=1990 |publisher=Wiley & Sons |location=New York |isbn=978-0-471-60922-3}}.
**{{Citation|last1=Adámek |first1=Jiří |last2=Herrlich |first2=Horst |last3=Strecker |first3=George E. |title=Abstract and Concrete Categories (The Joy of Cats) |edition=Dover |orig-year=1990 |url=http://katmat.math.uni-bremen.de/acc/ |year=2004 |publisher=Dover Publications |location=New York |isbn=978-0-486-46934-8}}.
* {{Citation|last = Bernays |first = Paul |title = A System of Axiomatic Set Theory—Part I |journal = [[The Journal of Symbolic Logic]] |volume = 2 |issue = 1 |pages = 65&ndash;77 |year = 1937 |doi=10.2307/2268862 |jstor=2268862}}.
* {{Citation|last = Bernays |first = Paul |title = A System of Axiomatic Set Theory—Part II |journal = The Journal of Symbolic Logic |volume = 6 |issue = 1 |pages = 1&ndash;17 |year = 1941 |doi=10.2307/2267281 |jstor=2267281|s2cid = 250344277 }}.
* {{Citation|last=Bernays |first=Paul |title=Axiomatic Set Theory |edition=2nd Revised |publisher=Dover Publications |year=1991 |isbn=978-0-486-66637-2}}.
* {{Citation|last=Bourbaki |first=Nicolas |title=Elements of Mathematics: Theory of Sets |publisher=Springer |year=2004 | url=https://archive.org/details/springer_10.1007-978-3-642-59309-3 |isbn=978-3-540-22525-6}}.
* {{Citation|last=Chuaqui |first=Rolando |author-link=Rolando Chuaqui |title=Axiomatic Set Theory: Impredicative Theories of Classes |publisher=North-Holland |year=1981 |isbn=0-444-86178-5}}.
* {{Citation |last=Cohen |first=Paul |title=The Independence of the Continuum Hypothesis |doi=10.1073/pnas.50.6.1143 |journal=[[Proceedings of the National Academy of Sciences of the United States of America]] |volume=50 |issue=6 |pages=1143–1148 |year=1963 |pmid=16578557 |pmc=221287|bibcode=1963PNAS...50.1143C |doi-access=free }}.
* {{Citation |last=Cohen |first=Paul |title=Set Theory and the Continuum Hypothesis |publisher=W. A. Benjamin |year=1966}}.
**{{Citation |last=Cohen |first=Paul |title=Set Theory and the Continuum Hypothesis |publisher=Dover Publications |year=2008 |url={{Google books|Z4NCAwAAQBAJ|Set Theory and the Continuum Hypothesis||plainurl=yes}} |isbn=978-0-486-46921-8}}.
* {{Citation |last=Dawson |first=John W. |year=1997 |title=Logical dilemmas: The life and work of Kurt Gödel |place=Wellesley, MA |publisher=AK Peters}}.
* {{Citation|last=Easton |first=William B. |year=1964 |title=Powers of Regular Cardinals |type=PhD thesis |publisher=Princeton University}}.
* {{Citation|last=Felgner |first=Ulrich | title=Comparison of the axioms of local and universal choice |url=http://matwbn.icm.edu.pl/ksiazki/fm/fm71/fm7113.pdf |journal=Fundamenta Mathematicae |volume=71 |pages=43–62 |year=1971|doi=10.4064/fm-71-1-43-62 |doi-access=free }}.
* {{Citation |last=Ferreirós |first=José |title=Labyrinth of Thought: A History of Set Theory and Its Role in Mathematical Thought |place=Basel, Switzerland |publisher=Birkhäuser |year=2007 |edition=2nd revised |isbn=978-3-7643-8349-7}}.
* {{Citation|last=Gödel |first=Kurt |title=The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory |edition=Revised |publisher=Princeton University Press |year=1940 |isbn=978-0-691-07927-1}}.
**{{Citation|last=Gödel |first=Kurt |others=with a foreword by [[Richard Laver|Laver, Richard]] |title=The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory |edition=Paperback |publisher=Ishi Press |year=2008 |isbn=978-0-923891-53-4}}.
* {{Citation|last=Gödel |first=Kurt |title=Collected Works, Volume 1: Publications 1929&ndash;1936 |publisher=Oxford University Press |year=1986 |isbn=978-0-19-514720-9}}.
* {{Citation|last=Gödel |first=Kurt |title=Collected Works, Volume 2: Publications 1938&ndash;1974 |publisher=Oxford University Press |year=1990 |isbn=978-0-19-514721-6}}.
* {{Citation|last=Gödel |first=Kurt |title=Collected Works, Volume 4: Correspondence A&ndash;G |publisher=Oxford University Press |year=2003 |isbn=978-0-19-850073-5}}.
* {{Citation |last = Gray |first = Robert |title = Computer programs and mathematical proofs |journal = [[The Mathematical Intelligencer]] |volume = 13 |issue = 4 |pages = 45&ndash;48 |year = 1991 |doi=10.1007/BF03028342|s2cid = 121229549 }}.
* {{Citation|last=Hallett |first=Michael |title=Cantorian Set Theory and Limitation of Size |edition=Hardcover |place=Oxford |publisher=Clarendon Press |year=1984 |isbn=978-0-19-853179-1}}.
**{{Citation|last=Hallett |first=Michael |title=Cantorian Set Theory and Limitation of Size |edition=Paperback |place=Oxford |publisher=Clarendon Press |year=1986 |isbn=978-0-19-853283-5}}.
* {{Citation|last=Kanamori |first=Akihiro |author-link=Akihiro Kanamori |title=The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings|title-link=The Higher Infinite |publisher=Springer |year=2009b |isbn=978-3-540-88867-3}}.
* {{Citation|last=Kanamori |first=Akihiro |title=Bernays and Set Theory |url=http://math.bu.edu/people/aki/17a.pdf |journal=[[Bulletin of Symbolic Logic]] |volume=15 |issue=1 |pages=43–69 |year=2009 |doi=10.2178/bsl/1231081769 |jstor=25470304|s2cid=15567244 }}.
* {{Citation|last=Kanamori |first=Akihiro |title=In Praise of Replacement |url=http://math.bu.edu/people/aki/20.pdf |journal=[[Bulletin of Symbolic Logic]] |volume=18 |issue=1 |pages=46–90 |year=2012 |doi=10.2178/bsl/1327328439 |jstor=41472440|s2cid=18951854 }}.
* {{Citation|last=Kunen |first=Kenneth |author-link=Kenneth Kunen |title=Set Theory: An Introduction to Independence Proofs |edition=Hardcover |publisher=North-Holland |year=1980 |isbn=978-0-444-86839-8|title-link=Set Theory: An Introduction to Independence Proofs }}.
**{{Citation|last=Kunen |first=Kenneth |title=Set Theory: An Introduction to Independence Proofs |edition=Paperback |publisher=North-Holland |year=2012 |isbn=978-0-444-56402-3}}.
* {{Citation|last=Mendelson |first=Elliott |author-link=Elliott Mendelson |year=1997 |title=An Introduction to Mathematical Logic |edition=4th |location=London |publisher=Chapman and Hall/CRC |isbn=978-0-412-80830-2}}. - Pp.&nbsp;225&ndash;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.
* {{Citation|last1=Mirimanoff |first1=Dmitry |title=Les antinomies de Russell et de Burali-Forti et le problème fondamental de la théorie des ensembles|year=1917 |journal=L'Enseignement Mathématique |volume=19 |pages=37–52}}.
* {{Citation| last = Montague | first = Richard | contribution = Semantic Closure and Non-Finite Axiomatizability I | editor = Buss, Samuel R. | editor-link = Samuel Buss | title = Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics | publisher = Pergamon Press | date = 1961 | pages = 45&ndash;69}}.
* {{Citation|last=Mostowski |first=Andrzej |author-link=Andrzej Mostowski |title=Some impredicative definitions in the axiomatic set theory |url=http://matwbn.icm.edu.pl/ksiazki/fm/fm37/fm37110.pdf |journal=[[Fundamenta Mathematicae]] |volume=37 |pages=111–124 |year=1950|doi=10.4064/fm-37-1-111-124 |doi-access=free }}.
* {{Citation|last1=Muller |first1=F. A. |date=1 September 2001 |title=Sets, classes, and categories |journal=British Journal for the Philosophy of Science |volume=52 |issue=3 |pages=539–73 |doi=10.1093/bjps/52.3.539 |url=http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF }}.
* {{Citation|editor-last=Müller |editor-first=Gurt |title=Sets and Classes: On the Work of Paul Bernays |series=Studies in Logic and the Foundations of Mathematics Volume 84 |location=Amsterdam |publisher=North Holland |year=1976 |isbn=978-0-7204-2284-9}}.
* {{Citation|last=Potter |first=Michael |title=Set Theory and Its Philosophy: A Critical Introduction |edition=Hardcover |publisher=Oxford University Press |year=2004 |isbn=978-0-19-926973-0}}.
**{{Citation|last=Potter |first=Michael |title=Set Theory and Its Philosophy: A Critical Introduction |edition=Paperback |publisher=Oxford University Press |year=2004p |isbn=978-0-19-927041-5}}.
* {{Citation| last = Pudlák | first = Pavel | contribution = The Lengths of Proofs | contribution-url = http://users.math.cas.cz/~pudlak/length.pdf | editor = Buss, Samuel R. | editor-link = Samuel Buss | title = Handbook of Proof Theory | publisher = Elsevier | date = 1998 | pages = 547&ndash;637 | isbn = 978-0-444-89840-1}}.
* {{Citation|last1=Smullyan |first1=Raymond M. |author1-link=Raymond Smullyan |last2=Fitting |first2=Melvin |author2-link=Melvin Fitting |title=Set Theory and the Continuum Problem |publisher=Dover |year=2010 |orig-year=Revised and corrected edition: first published in 1996 by Oxford University Press |isbn=978-0-486-47484-7}}.
*{{Citation|last=Solovay |first=Robert M. |chapter= Introductory note to ''1938'', ''1939'', ''1939a'' and ''1940'' |title=Kurt Gödel Collected Works, Volume 2: Publications 1938&ndash;1974 |publisher=Oxford University Press |year=1990 |pages=1&ndash;25 |isbn=978-0-19-514721-6}}.
*{{Citation|last=von Neumann |first=John |title=Zur Einführung der transfiniten Zahlen |url=http://bbi-math.narod.ru/newmann/newmann.html |journal=Acta Litt. Acad. Sc. Szeged X. |volume=1 |pages=199–208 |year=1923}}. 
**English translation: {{citation|last=van Heijenoort |first=Jean |orig-year=1967 |year=2002a |publisher=Harvard University Press |title=From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 |chapter=On the introduction of transfinite numbers |edition=Fourth Printing |pages=346–354 |chapter-url={{Google books|v4tBTBlU05sC|On the introduction of transfinite numbers|page=346|plainurl=yes}} |isbn=978-0-674-32449-7}}.
**English translation: {{citation |last=van Heijenoort |first=Jean |orig-year=1967 |year=2002b |publisher=Harvard University Press |title=From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 |chapter=An axiomatization of set theory |edition=Fourth Printing |pages=393–413 |chapter-url={{Google books|v4tBTBlU05sC|An axiomatization of set theory|page=393|plainurl=yes}} |isbn=978-0-674-32449-7}}.
*{{Citation|last=von Neumann |first=John |title=Eine Axiomatisierung der Mengenlehre |url=http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN243919689_0154&DMDID=DMDLOG_0025 |journal=[[Journal für die Reine und Angewandte Mathematik]] |volume=154 |pages=219–240 |year=1925}}.
*{{Citation|last=von Neumann |first=John |title=Die Axiomatisierung der Mengenlehre |url=http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN266833020_0027&DMDID=DMDLOG_0042 |journal=[[Mathematische Zeitschrift]] |volume=27 |pages=669–752 |year=1928 |doi=10.1007/bf01171122|s2cid=123492324 }}.
*{{Citation|last=von Neumann |first=John |title=Über eine Widerspruchsfreiheitsfrage in der axiomatischen Mengenlehre |url=http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN243919689_0160&DMDID=DMDLOG_0019 |journal=Journal für die Reine und Angewandte Mathematik |volume=160 |pages=227–241 |year=1929}}.

==External links==
* {{PlanetMath reference|urlname=VonNeumannBernaysGodelSetTheory|title= von Neumann-Bernays-Gödel set theory}}
* {{MathWorld|title=von Neumann-Bernays-Gödel Set Theory |id=vonNeumann-Bernays-GoedelSetTheory |author=Szudzik, Matthew}}

{{Set theory}}
{{Mathematical logic}}

{{DEFAULTSORT:Von Neumann-Bernays-Godel set theory}}
[[Category:Foundations of mathematics]]
[[Category:John von Neumann]]
[[Category:Systems of set theory]]
[[Category:Works by Kurt Gödel]]