
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
defined on the class of all nonempty sets such that
for every nonempty set
This is stronger than ZFC's axiom of choice: For every set
of nonempty sets, there exists a choice function
defined on
such that
for all
- The set-theoretic paradoxes are handled by recognizing that some classes cannot be sets. For example, assume that the class
of all ordinals is a set. Then
is a transitive set well-ordered by
. So, by definition,
is an ordinal. Hence,
, which contradicts
being a well-ordering of
Therefore,
is not a set. A class that is not a set is called a proper class;
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 that quantifies only over sets, there exists a class
consisting of the
-tuples satisfying the formula—that is,
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. The 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.[non-primary source needed] Bernays used many-sorted logic with two sorts: classes and sets. Gödel avoided sorts by introducing primitive predicates: for "
is a class" and
for "
is a set" (in German, "set" is Menge). He also introduced axioms stating that every set is a class and that if class
is a member of a class, then
is a set. 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
as
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. 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, where
and
are classes is a valid statement. In Bernays' approach this statement has no meaning. However, if
is a set, there is an equivalent statement: Define "set
represents class
" if they have the same sets as members—that is,
The statement
where set
represents class
is equivalent to Gödel's
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, and its only primitive notions 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: is a set if and only if
. A class that is not a set is called a proper class:
is a proper class if and only if
. 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. Gödel also used names that begin with an uppercase letter to denote particular classes, including functions and relations defined on the class of all sets. Gödel's convention is used in this article. It allows us to write:
instead of
instead of
The following axioms and definitions are needed for the proof of the class existence theorem.
Axiom of extensionality. If two classes have the same elements, then they are identical.
This axiom generalizes ZFC's axiom of extensionality to classes.
Axiom of pairing. If and
are sets, then there exists a set
whose only members are
and
.
As in ZFC, the axiom of extensionality implies the uniqueness of the set , which allows us to introduce the notation
Ordered pairs are defined by:
Tuples are defined inductively using ordered pairs:
Class existence axioms and axiom of regularity
Class existence axioms will be used to prove the class existence theorem: For every formula in free set variables that quantifies only over sets, there exists a class of
-tuples 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.
Example 1: If the classes and
are functions, then the composite function
is defined by the formula:
Since this formula has two free set variables,
and
the class existence theorem constructs the class of ordered pairs:
Because this formula is built from simpler formulas using conjunction
and existential quantification
, class operations are needed that take classes representing the simpler formulas and produce classes representing the formulas with
and
. To produce a class representing a formula with
, intersection used since
To produce a class representing a formula with
, the domain is used since
Before taking the intersection, the tuples in
and
need an extra component so they have the same variables. The component
is added to the tuples of
and
is added to the tuples of
:
and
In the definition of
the variable
is not restricted by the statement
so
ranges over the class
of all sets. Similarly, in the definition of
the variable
ranges over
So an axiom is needed that adds an extra component (whose values range over
) to the tuples of a given class.
Next, the variables are put in the same order to prepare for the intersection:
and
To go from
to
and from
to
requires two different permutations, so axioms that support permutations of tuple components are needed.
The intersection of
and
handles
:
Since
is defined as
, taking the domain of
handles
and produces the composite function:
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 containing all the ordered pairs whose first component is a member of the second component.
Intersection (conjunction). For any two classes and
, there is a class
consisting precisely of the sets that belong to both
and
.
Complement (negation). For any class , there is a class
consisting precisely of the sets not belonging to
.
Domain (existential quantifier). For any class , there is a class
consisting precisely of the first components of the ordered pairs of
.
By the axiom of extensionality, class in the intersection axiom and class
in the complement and domain axioms are unique. They will be denoted by:
and
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 The intersection and complement axioms imply the existence of
, which is empty. By the axiom of extensionality, this class is unique; it is denoted by
The complement of
is the class
of all sets, which is also unique by extensionality. The set predicate
, which was defined as
, is now redefined as
to avoid quantifying over classes.
Axioms for handling tuples:
Product by . For any class
, there is a class
consisting of the ordered pairs whose first component belongs to
.
Circular permutation. For any class , there is a class
whose 3‑tuples are obtained by applying the circular permutation
to the 3‑tuples of
.
Transposition. For any class , there is a class
whose 3‑tuples are obtained by transposing the last two components of the 3‑tuples of
.
By extensionality, the product by axiom implies the existence of a unique class, which is denoted by
This axiom is used to define the class
of all
-tuples:
and
If
is a class, extensionality implies that
is the unique class consisting of the
-tuples of
For example, the membership axiom produces a class
that may contain elements that are not ordered pairs, while the intersection
contains only the ordered pairs of
.
The circular permutation and transposition axioms do not imply the existence of unique classes because they specify only the 3‑tuples of class By specifying the 3‑tuples, these axioms also specify the
-tuples for
since:
The axioms for handling tuples and the domain axiom imply the following lemma, which is used in the proof of the class existence theorem.
Tuple lemma —
- Class
: Apply product by
to
to produce
- Class
: Apply transposition to
to produce
- Class
: Apply circular permutation to
to produce
- Class
: Apply circular permutation to
, then apply domain to produce
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.
Axiom of regularity. Every nonempty set has at least one element with which it has no element in common.
This axiom implies that a set cannot belong to itself: Assume that and let
Then
since
This contradicts the axiom of regularity because
is the only element in
Therefore,
The axiom of regularity also prohibits infinite descending membership sequences of sets:
Gödel stated regularity for classes rather than for sets in his 1940 monograph, which was based on lectures given in 1938. In 1939, he proved that regularity for sets implies regularity for classes.
Class existence theorem
Class existence theorem — Let be a formula that quantifies only over sets and contains no free variables other than
(not necessarily all of these). Then for all
, there exists a unique class
of
-tuples such that:
The class
is denoted by
The theorem's proof will be done in two steps:
- Transformation rules are used to transform the given formula
into an equivalent formula that simplifies the inductive part of the proof. For example, the only logical symbols in the transformed formula are
,
, and
, 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
-tuples satisfying the formula.
Transformation rules. In rules 1 and 2 below, and
denote set or class variables. These two rules eliminate all occurrences of class variables before an
and all occurrences of equality. Each time rule 1 or 2 is applied to a subformula,
is chosen so that
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
,
,
,
, set variables, and class variables
where
does not appear before an
.
is transformed into
- Extensionality is used to transform
into
- Logical identities are used to transform subformulas containing
and
to subformulas that only use
and
Transformation rules: bound variables. Consider the composite function formula of example 1 with its free set variables replaced by and
:
The inductive proof will remove
, which produces the formula
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
with
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.
Example 2: Rule 4 is applied to the formula that defines the class consisting of all sets of the form
That is, sets that contain at least
and a set containing
— for example,
where
and
are sets.
Since
is the only free variable,
The quantified variable
appears twice in
at nesting depth 2. Its subscript is 3 because
If two quantifier scopes are at the same nesting depth, they are either identical or disjoint. The two occurrences of
are in disjoint quantifier scopes, so they do not interact with each other.
Proof of the class existence theorem. 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.
The following lemma is used in the proof.
Expansion lemma — Let and let
be a class containing all the ordered pairs
satisfying
That is,
Then
can be expanded into the unique class
of
-tuples satisfying
. That is,
Proof:
- If
let
Otherwise,
so components are added in front of
apply the tuple lemma's statement 1 to
with
This produces a class
containing all the
-tuples
satisfying
- If
let
Otherwise,
so components are added between
and
add the components
one by one using the tuple lemma's statement 2. This produces a class
containing all the
-tuples
satisfying
- If
let
Otherwise,
so components are added after
add the components
one by one using the tuple lemma's statement 3. This produces a class
containing all the
-tuples
satisfying
- Let
Extensionality implies that
is the unique class of
-tuples satisfying
Class existence theorem for transformed formulas — Let be a formula that:
- contains no free variables other than
;
- contains only
,
,
,
, set variables, and the class variables
where
does not appear before an
;
- only quantifies set variables
where
is the quantifier nesting depth of the variable.
Then for all , there exists a unique class
of
-tuples such that:
Proof: Basis step: has 0 logical symbols. The theorem's hypothesis implies that
is an atomic formula of the form
or
Case 1: If is
, we build the class
the unique class of
-tuples satisfying
Case a: is
where
The axiom of membership produces a class
containing all the ordered pairs
satisfying
Apply the expansion lemma to
to obtain
Case b: is
where
The axiom of membership produces a class
containing all the ordered pairs
satisfying
Apply the tuple lemma's statement 4 to
to obtain
containing all the ordered pairs
satisfying
Apply the expansion lemma to
to obtain
Case c: is
where
Since this formula is false by the axiom of regularity, no
-tuples satisfy it, so
Case 2: If is
, we build the class
the unique class of
-tuples satisfying
Case a: is
where
Apply the axiom of product by
to
to produce the class
Apply the expansion lemma to
to obtain
Case b: is
where
Apply the axiom of product by
to
to produce the class
Apply the tuple lemma's statement 4 to
to obtain
Apply the expansion lemma to
to obtain
Case c: is
where
Then
Inductive step: has
logical symbols where
In the foundations of mathematics von Neumann Bernays Godel 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 Godel simplified Bernays theory for his relative consistency proof of the axiom of choice and the generalized continuum hypothesis Classes in set theoryThe 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 G displaystyle G defined on the class of all nonempty sets such that G x x displaystyle G x in x for every nonempty set x displaystyle x This is stronger than ZFC s axiom of choice For every set s displaystyle s of nonempty sets there exists a choice function f displaystyle f defined on s displaystyle s such that f x x displaystyle f x in x for all x s displaystyle x in s The set theoretic paradoxes are handled by recognizing that some classes cannot be sets For example assume that the class Ord displaystyle Ord of all ordinals is a set Then Ord displaystyle Ord is a transitive set well ordered by displaystyle in So by definition Ord displaystyle Ord is an ordinal Hence Ord Ord displaystyle Ord in Ord which contradicts displaystyle in being a well ordering of Ord displaystyle Ord Therefore Ord displaystyle Ord is not a set A class that is not a set is called a proper class Ord displaystyle Ord 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 Godel 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 ϕ x1 xn displaystyle phi x 1 ldots x n that quantifies only over sets there exists a class A displaystyle A consisting of the n displaystyle n tuples satisfying the formula that is x1 xn x1 xn A ϕ x1 xn displaystyle forall x 1 cdots forall x n x 1 ldots x n in A iff phi x 1 ldots x n 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 The 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 NBGClasses 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 non primary source needed Bernays used many sorted logic with two sorts classes and sets Godel avoided sorts by introducing primitive predicates Cls A displaystyle mathfrak Cls A for A displaystyle A is a class and M A displaystyle mathfrak M A for A displaystyle A is a set in German set is Menge He also introduced axioms stating that every set is a class and that if class A displaystyle A is a member of a class then A displaystyle A is a set Using predicates is the standard way to eliminate sorts Elliott Mendelson modified Godel s approach by having everything be a class and defining the set predicate M A displaystyle M A as C A C displaystyle exists C A in C This modification eliminates Godel 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 h is between a set and a class 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 Godel s approach A C displaystyle A in C where A displaystyle A and C displaystyle C are classes is a valid statement In Bernays approach this statement has no meaning However if A displaystyle A is a set there is an equivalent statement Define set a displaystyle a represents class A displaystyle A if they have the same sets as members that is x x a xhA displaystyle forall x x in a iff x eta A The statement ahC displaystyle a eta C where set a displaystyle a represents class A displaystyle A is equivalent to Godel s A C displaystyle A in C The approach adopted in this article is that of Godel with Mendelson s modification This means that NBG is an axiomatic system in first order predicate logic with equality and its only primitive notions 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 A displaystyle A is a set if and only if C A C displaystyle exists C A in C A class that is not a set is called a proper class A displaystyle A is a proper class if and only if C A C displaystyle forall C A notin C Therefore every class is either a set or a proper class and no class is both Godel introduced the convention that uppercase variables range over classes while lowercase variables range over sets Godel also used names that begin with an uppercase letter to denote particular classes including functions and relations defined on the class of all sets Godel s convention is used in this article It allows us to write xϕ x displaystyle exists x phi x instead of x C x C ϕ x displaystyle exists x bigl exists C x in C land phi x bigr xϕ x displaystyle forall x phi x instead of x C x C ϕ x displaystyle forall x bigl exists C x in C implies phi x bigr The following axioms and definitions are needed for the proof of the class existence theorem Axiom of extensionality If two classes have the same elements then they are identical A B x x A x B A B displaystyle forall A forall B forall x x in A iff x in B implies A B This axiom generalizes ZFC s axiom of extensionality to classes Axiom of pairing If x displaystyle x and y displaystyle y are sets then there exists a set p displaystyle p whose only members are x displaystyle x and y displaystyle y x y p z z p z x z y displaystyle forall x forall y exists p forall z z in p iff z x lor z y As in ZFC the axiom of extensionality implies the uniqueness of the set p displaystyle p which allows us to introduce the notation x y displaystyle x y Ordered pairs are defined by x y x x y displaystyle x y x x y Tuples are defined inductively using ordered pairs x1 x1 displaystyle x 1 x 1 For n gt 1 x1 xn 1 xn x1 xn 1 xn displaystyle text For n gt 1 x 1 ldots x n 1 x n x 1 ldots x n 1 x n Class existence axioms and axiom of regularity Class existence axioms will be used to prove the class existence theorem For every formula in n displaystyle n free set variables that quantifies only over sets there exists a class of n displaystyle n tuples 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 Example 1 If the classes F displaystyle F and G displaystyle G are functions then the composite function G F displaystyle G circ F is defined by the formula t x t F t y G displaystyle exists t x t in F land t y in G Since this formula has two free set variables x displaystyle x and y displaystyle y the class existence theorem constructs the class of ordered pairs G F x y t x t F t y G displaystyle G circ F x y exists t x t in F land t y in G Because this formula is built from simpler formulas using conjunction displaystyle land and existential quantification displaystyle exists class operations are needed that take classes representing the simpler formulas and produce classes representing the formulas with displaystyle land and displaystyle exists To produce a class representing a formula with displaystyle land intersection used since x A B x A x B displaystyle x in A cap B iff x in A land x in B To produce a class representing a formula with displaystyle exists the domain is used since x Dom A t x t A displaystyle x in Dom A iff exists t x t in A Before taking the intersection the tuples in F displaystyle F and G displaystyle G need an extra component so they have the same variables The component y displaystyle y is added to the tuples of F displaystyle F and x displaystyle x is added to the tuples of G displaystyle G F x t y x t F displaystyle F x t y x t in F and G t y x t y G displaystyle G t y x t y in G In the definition of F displaystyle F the variable y displaystyle y is not restricted by the statement x t F displaystyle x t in F so y displaystyle y ranges over the class V displaystyle V of all sets Similarly in the definition of G displaystyle G the variable x displaystyle x ranges over V displaystyle V So an axiom is needed that adds an extra component whose values range over V displaystyle V to the tuples of a given class Next the variables are put in the same order to prepare for the intersection F x y t x t F displaystyle F x y t x t in F and G x y t t y G displaystyle G x y t t y in G To go from F displaystyle F to F displaystyle F and from G displaystyle G to G displaystyle G requires two different permutations so axioms that support permutations of tuple components are needed The intersection of F displaystyle F and G displaystyle G handles displaystyle land F G x y t x t F t y G displaystyle F cap G x y t x t in F land t y in G Since x y t displaystyle x y t is defined as x y t displaystyle x y t taking the domain of F G displaystyle F cap G handles t displaystyle exists t and produces the composite function G F Dom F G x y t x t F t y G displaystyle G circ F Dom F cap G x y exists t x t in F land t y in G 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 E displaystyle E containing all the ordered pairs whose first component is a member of the second component E x y x y E x y displaystyle exists E forall x forall y x y in E iff x in y Intersection conjunction For any two classes A displaystyle A and B displaystyle B there is a class C displaystyle C consisting precisely of the sets that belong to both A displaystyle A and B displaystyle B A B C x x C x A x B displaystyle forall A forall B exists C forall x x in C iff x in A land x in B Complement negation For any class A displaystyle A there is a class B displaystyle B consisting precisely of the sets not belonging to A displaystyle A A B x x B x A displaystyle forall A exists B forall x x in B iff neg x in A Domain existential quantifier For any class A displaystyle A there is a class B displaystyle B consisting precisely of the first components of the ordered pairs of A displaystyle A A B x x B y x y A displaystyle forall A exists B forall x x in B iff exists y x y in A By the axiom of extensionality class C displaystyle C in the intersection axiom and class B displaystyle B in the complement and domain axioms are unique They will be denoted by A B displaystyle A cap B A displaystyle complement A and Dom A displaystyle Dom A 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 E displaystyle E The intersection and complement axioms imply the existence of E E displaystyle E cap complement E which is empty By the axiom of extensionality this class is unique it is denoted by displaystyle emptyset The complement of displaystyle emptyset is the class V displaystyle V of all sets which is also unique by extensionality The set predicate M A displaystyle M A which was defined as C A C displaystyle exists C A in C is now redefined as A V displaystyle A in V to avoid quantifying over classes Axioms for handling tuples Product by V displaystyle V For any class A displaystyle A there is a class B displaystyle B consisting of the ordered pairs whose first component belongs to A displaystyle A A B u u B x y u x y x A displaystyle forall A exists B forall u u in B iff exists x exists y u x y land x in A Circular permutation For any class A displaystyle A there is a class B displaystyle B whose 3 tuples are obtained by applying the circular permutation y z x x y z displaystyle y z x mapsto x y z to the 3 tuples of A displaystyle A A B x y z x y z B y z x A displaystyle forall A exists B forall x forall y forall z x y z in B iff y z x in A Transposition For any class A displaystyle A there is a class B displaystyle B whose 3 tuples are obtained by transposing the last two components of the 3 tuples of A displaystyle A A B x y z x y z B x z y A displaystyle forall A exists B forall x forall y forall z x y z in B iff x z y in A By extensionality the product by V displaystyle V axiom implies the existence of a unique class which is denoted by A V displaystyle A times V This axiom is used to define the class Vn displaystyle V n of all n displaystyle n tuples V1 V displaystyle V 1 V and Vn 1 Vn V displaystyle V n 1 V n times V If A displaystyle A is a class extensionality implies that A Vn displaystyle A cap V n is the unique class consisting of the n displaystyle n tuples of A displaystyle A For example the membership axiom produces a class E displaystyle E that may contain elements that are not ordered pairs while the intersection E V2 displaystyle E cap V 2 contains only the ordered pairs of E displaystyle E The circular permutation and transposition axioms do not imply the existence of unique classes because they specify only the 3 tuples of class B displaystyle B By specifying the 3 tuples these axioms also specify the n displaystyle n tuples for n 4 displaystyle n geq 4 since x1 xn 2 xn 1 xn x1 xn 2 xn 1 xn displaystyle x 1 ldots x n 2 x n 1 x n x 1 ldots x n 2 x n 1 x n The axioms for handling tuples and the domain axiom imply the following lemma which is used in the proof of the class existence theorem Tuple lemma A B1 x y z z x y B1 x y A displaystyle forall A exists B 1 forall x forall y forall z z x y in B 1 iff x y in A A B2 x y z x z y B2 x y A displaystyle forall A exists B 2 forall x forall y forall z x z y in B 2 iff x y in A A B3 x y z x y z B3 x y A displaystyle forall A exists B 3 forall x forall y forall z x y z in B 3 iff x y in A A B4 x y z y x B4 x y A displaystyle forall A exists B 4 forall x forall y forall z y x in B 4 iff x y in A Proof Class B3 displaystyle B 3 Apply product by V displaystyle V to A displaystyle A to produce B3 displaystyle B 3 Class B2 displaystyle B 2 Apply transposition to B3 displaystyle B 3 to produce B2 displaystyle B 2 Class B1 displaystyle B 1 Apply circular permutation to B3 displaystyle B 3 to produce B1 displaystyle B 1 Class B4 displaystyle B 4 Apply circular permutation to B2 displaystyle B 2 then apply domain to produce B4 displaystyle B 4 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 Axiom of regularity Every nonempty set has at least one element with which it has no element in common a a u u a u a displaystyle forall a a neq emptyset implies exists u u in a land u cap a emptyset This axiom implies that a set cannot belong to itself Assume that x x displaystyle x in x and let a x displaystyle a x Then x a displaystyle x cap a neq emptyset since x x a displaystyle x in x cap a This contradicts the axiom of regularity because x displaystyle x is the only element in a displaystyle a Therefore x x displaystyle x notin x The axiom of regularity also prohibits infinite descending membership sequences of sets xn 1 xn x1 x0 displaystyle cdots in x n 1 in x n in cdots in x 1 in x 0 Godel stated regularity for classes rather than for sets in his 1940 monograph which was based on lectures given in 1938 In 1939 he proved that regularity for sets implies regularity for classes Class existence theorem Class existence theorem Let ϕ x1 xn Y1 Ym displaystyle phi x 1 dots x n Y 1 dots Y m be a formula that quantifies only over sets and contains no free variables other than x1 xn Y1 Ym displaystyle x 1 dots x n Y 1 dots Y m not necessarily all of these Then for all Y1 Ym displaystyle Y 1 dots Y m there exists a unique class A displaystyle A of n displaystyle n tuples such that x1 xn x1 xn A ϕ x1 xn Y1 Ym displaystyle 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 The class A displaystyle A is denoted by x1 xn ϕ x1 xn Y1 Ym displaystyle x 1 dots x n phi x 1 dots x n Y 1 dots Y m The theorem s proof will be done in two steps Transformation rules are used to transform the given formula ϕ displaystyle phi into an equivalent formula that simplifies the inductive part of the proof For example the only logical symbols in the transformed formula are displaystyle neg displaystyle land and displaystyle exists 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 n displaystyle n tuples satisfying the formula Transformation rules In rules 1 and 2 below D displaystyle Delta and G displaystyle Gamma denote set or class variables These two rules eliminate all occurrences of class variables before an displaystyle in and all occurrences of equality Each time rule 1 or 2 is applied to a subformula i displaystyle i is chosen so that zi displaystyle z i 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 displaystyle neg displaystyle land displaystyle exists displaystyle in set variables and class variables Yk displaystyle Y k where Yk displaystyle Y k does not appear before an displaystyle in Yk G displaystyle Y k in Gamma is transformed into zi zi Yk zi G displaystyle exists z i z i Y k land z i in Gamma Extensionality is used to transform D G displaystyle Delta Gamma into zi zi D zi G displaystyle forall z i z i in Delta iff z i in Gamma Logical identities are used to transform subformulas containing displaystyle lor implies iff and displaystyle forall to subformulas that only use displaystyle neg land and displaystyle exists Transformation rules bound variables Consider the composite function formula of example 1 with its free set variables replaced by x1 displaystyle x 1 and x2 displaystyle x 2 t x1 t F t x2 G displaystyle exists t x 1 t in F land t x 2 in G The inductive proof will remove t displaystyle exists t which produces the formula x1 t F t x2 G displaystyle x 1 t in F land t x 2 in G 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 t displaystyle t with x3 displaystyle x 3 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 Example 2 Rule 4 is applied to the formula ϕ x1 displaystyle phi x 1 that defines the class consisting of all sets of the form displaystyle emptyset emptyset dots dots That is sets that contain at least displaystyle emptyset and a set containing displaystyle emptyset for example a b c d e displaystyle emptyset emptyset a b c d e where a b c d displaystyle a b c d and e displaystyle e are sets ϕ x1 u u x1 v v u w w x1 y y w z z y ϕr x1 x2 x2 x1 x3 x3 x2 x2 x2 x1 x3 x3 x2 x4 x4 x3 displaystyle begin aligned phi x 1 amp 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 amp 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 aligned Since x1 displaystyle x 1 is the only free variable n 1 displaystyle n 1 The quantified variable x3 displaystyle x 3 appears twice in x3 x2 displaystyle x 3 in x 2 at nesting depth 2 Its subscript is 3 because n q 1 2 3 displaystyle n q 1 2 3 If two quantifier scopes are at the same nesting depth they are either identical or disjoint The two occurrences of x3 displaystyle x 3 are in disjoint quantifier scopes so they do not interact with each other Proof of the class existence theorem 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 Proof of the class existence theorem for transformed formulas The following lemma is used in the proof Expansion lemma Let 1 i lt j n displaystyle 1 leq i lt j leq n and let P displaystyle P be a class containing all the ordered pairs xi xj displaystyle x i x j satisfying R xi xj displaystyle R x i x j That is P xi xj R xi xj displaystyle P supseteq x i x j R x i x j Then P displaystyle P can be expanded into the unique class Q displaystyle Q of n displaystyle n tuples satisfying R xi xj displaystyle R x i x j That is Q x1 xn R xi xj displaystyle Q x 1 ldots x n R x i x j Proof If i 1 displaystyle i 1 let P1 P displaystyle P 1 P Otherwise i gt 1 displaystyle i gt 1 so components are added in front of xi displaystyle x i text apply the tuple lemma s statement 1 to P displaystyle P with z x1 xi 1 displaystyle z x 1 dots x i 1 This produces a class P1 displaystyle P 1 containing all the i 1 displaystyle i 1 tuples x1 xi 1 xi xj x1 xi 1 xi xj displaystyle x 1 dots x i 1 x i x j x 1 dots x i 1 x i x j satisfying R xi xj displaystyle R x i x j If j i 1 displaystyle j i 1 let P2 P1 displaystyle P 2 P 1 Otherwise j gt i 1 displaystyle j gt i 1 so components are added between xi displaystyle x i and xj displaystyle x j text add the components xi 1 xj 1 displaystyle x i 1 dots x j 1 one by one using the tuple lemma s statement 2 This produces a class P2 displaystyle P 2 containing all the j displaystyle j tuples x1 xi xi 1 xj 1 xj x1 xj displaystyle cdots x 1 dots x i x i 1 cdots x j 1 x j x 1 dots x j satisfying R xi xj displaystyle R x i x j If j n displaystyle j n let P3 P2 displaystyle P 3 P 2 Otherwise j lt n displaystyle j lt n so components are added after xj displaystyle x j text add the components xj 1 xn displaystyle x j 1 dots x n one by one using the tuple lemma s statement 3 This produces a class P3 displaystyle P 3 containing all the n displaystyle n tuples x1 xj xj 1 xn x1 xn displaystyle cdots x 1 dots x j x j 1 cdots x n x 1 dots x n satisfying R xi xj displaystyle R x i x j Let Q P3 Vn displaystyle Q P 3 cap V n Extensionality implies that Q displaystyle Q is the unique class of n displaystyle n tuples satisfying R xi xj displaystyle R x i x j Class existence theorem for transformed formulas Let ϕ x1 xn Y1 Ym displaystyle phi x 1 ldots x n Y 1 ldots Y m be a formula that contains no free variables other than x1 xn Y1 Ym displaystyle x 1 ldots x n Y 1 ldots Y m contains only displaystyle in displaystyle neg displaystyle land displaystyle exists set variables and the class variables Yk displaystyle Y k where Yk displaystyle Y k does not appear before an displaystyle in only quantifies set variables xn q displaystyle x n q where q displaystyle q is the quantifier nesting depth of the variable Then for all Y1 Ym displaystyle Y 1 dots Y m there exists a unique class A displaystyle A of n displaystyle n tuples such that x1 xn x1 xn A ϕ x1 xn Y1 Ym displaystyle 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 Proof Basis step ϕ displaystyle phi has 0 logical symbols The theorem s hypothesis implies that ϕ displaystyle phi is an atomic formula of the form xi xj displaystyle x i in x j or xi Yk displaystyle x i in Y k Case 1 If ϕ displaystyle phi is xi xj displaystyle x i in x j we build the class Ei j n x1 xn xi xj displaystyle E i j n x 1 ldots x n x i in x j the unique class of n displaystyle n tuples satisfying xi xj displaystyle x i in x j Case a ϕ displaystyle phi is xi xj displaystyle x i in x j where i lt j displaystyle i lt j The axiom of membership produces a class P displaystyle P containing all the ordered pairs xi xj displaystyle x i x j satisfying xi xj displaystyle x i in x j Apply the expansion lemma to P displaystyle P to obtain Ei j n x1 xn xi xj displaystyle E i j n x 1 ldots x n x i in x j Case b ϕ displaystyle phi is xi xj displaystyle x i in x j where i gt j displaystyle i gt j The axiom of membership produces a class P displaystyle P containing all the ordered pairs xi xj displaystyle x i x j satisfying xi xj displaystyle x i in x j Apply the tuple lemma s statement 4 to P displaystyle P to obtain P displaystyle P containing all the ordered pairs xj xi displaystyle x j x i satisfying xi xj displaystyle x i in x j Apply the expansion lemma to P displaystyle P to obtain Ei j n x1 xn xi xj displaystyle E i j n x 1 ldots x n x i in x j Case c ϕ displaystyle phi is xi xj displaystyle x i in x j where i j displaystyle i j Since this formula is false by the axiom of regularity no n displaystyle n tuples satisfy it so Ei j n displaystyle E i j n emptyset Case 2 If ϕ displaystyle phi is xi Yk displaystyle x i in Y k we build the class Ei Yk n x1 xn xi Yk displaystyle E i Y k n x 1 ldots x n x i in Y k the unique class of n displaystyle n tuples satisfying xi Yk displaystyle x i in Y k Case a ϕ displaystyle phi is xi Yk displaystyle x i in Y k where i lt n displaystyle i lt n Apply the axiom of product by V displaystyle V to Yk displaystyle Y k to produce the class P Yk V xi xi 1 xi Yk displaystyle P Y k times V x i x i 1 x i in Y k Apply the expansion lemma to P displaystyle P to obtain Ei Yk n x1 xn xi Yk displaystyle E i Y k n x 1 ldots x n x i in Y k Case b ϕ displaystyle phi is xi Yk displaystyle x i in Y k where i n gt 1 displaystyle i n gt 1 Apply the axiom of product by V displaystyle V to Yk displaystyle Y k to produce the class P Yk V xi xi 1 xi Yk displaystyle P Y k times V x i x i 1 x i in Y k Apply the tuple lemma s statement 4 to P displaystyle P to obtain P V Yk xi 1 xi xi Yk displaystyle P V times Y k x i 1 x i x i in Y k Apply the expansion lemma to P displaystyle P to obtain Ei Yk n x1 xn xi Yk displaystyle E i Y k n x 1 ldots x n x i in Y k Case c ϕ displaystyle phi is xi Yk displaystyle x i in Y k where i n 1 displaystyle i n 1 Then Ei Yk n Yk displaystyle E i Y k n Y k Inductive step ϕ displaystyle phi has k displaystyle k logical symbols where k gt 0 displaystyle k gt 0