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–choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose 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 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 formulas (membership and equality) and finitely many logical symbols, only finitely many axioms 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 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 notions of his theory were function and argument. Using these notions, he defined class and set. Paul Bernays reformulated von Neumann's theory by taking class and set as primitive notions. Kurt Gödel simplified Bernays' theory for his relative consistency proof of the axiom of choice and the generalized continuum hypothesis.

Classes in set theory

The uses of classes

Classes have several uses in NBG:

  • They produce a finite axiomatization of set theory.
  • They are used to state a "very strong form of the axiom of choice"—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>
  • The set-theoretic paradoxes are handled by recognizing that some classes cannot be sets. For example, assume that the class <math>Ord</math> of all ordinals is a set. Then <math>Ord</math> is a transitive set well-ordered 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.
  • 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 of this function.

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 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 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.

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. Then these axioms are used to prove the class existence theorem, which implies every instance of the axiom schema. 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> 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. In Bernays' theory, every set has two representations: one as a set and the other as a class. Also, there are two membership relations: the first, denoted by "∈", is between two sets; the second, denoted by "η", is between a set and a class.

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.

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

Axiom of pairing. 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>

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 pairs are defined by:

:<math>(x, y) = \{\{x\}, \{x, y\}\}</math>

Tuples are defined inductively 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>

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 set variables that quantifies only over sets, there exists a class of that satisfy it. The following example starts with two classes that are functions 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.

:{| class="wikitable"

|- style="text-align: left; vertical-align: top; style="background: white"

|Example 1: 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 <math>\land</math> and existential quantification <math>\exists</math>, class operations 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 is 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 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 permutations, 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.

Axioms for handling language primitives:

Membership. 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>

Intersection (conjunction). 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>

Complement (negation). 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>

Domain (existential quantifier). 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>

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.

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:

Product by <math>V</math>. 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>

Circular permutation. For any class <math>A</math>, there is a class <math>B</math> whose 3tuples are obtained by applying the circular permutation <math>(y,z,x) \mapsto (x,y,z)</math> to the 3tuples 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>

Transposition. For any class <math>A</math>, there is a class <math>B</math> whose 3tuples are obtained by transposing the last two components of the 3tuples 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>

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 : <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 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 3tuples of class <math>B.</math> By specifying the 3tuples, these axioms also specify the 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.

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.