In the
foundations of mathematics
Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathe ...
, von Neumann–Bernays–Gödel set theory (NBG) is an
axiomatic set theory
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concern ...
that is a
conservative extension of
Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the
notion of
class
Class or The Class may refer to:
Common uses not otherwise categorized
* Class (biology), a taxonomic rank
* Class (knowledge representation), a collection of individuals or objects
* Class (philosophy), an analytical concept used differently ...
, which is a collection of
sets defined by a
formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
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
In the foundations of mathematics, Morse–Kelley set theory (MK), Kelley–Morse set theory (KM), Morse–Tarski set theory (MT), Quine–Morse set theory (QM) or the system of Quine and Morse is a first-order axiomatic set theory that is closely ...
(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
axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
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
set-theoretic paradoxes, and for stating the
axiom of global choice, which is stronger than ZFC's
axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
.
John von Neumann
John von Neumann (; hu, Neumann János Lajos, ; December 28, 1903 – February 8, 1957) was a Hungarian-American mathematician, physicist, computer scientist, engineer and polymath. He was regarded as having perhaps the widest c ...
introduced classes into set theory in 1925. The
primitive notions of his theory were
function and
argument
An argument is a statement or group of statements called premises intended to determine the degree of truth or acceptability of another statement called conclusion. Arguments can be studied from three main perspectives: the logical, the dialecti ...
. Using these notions, he defined class and set.
[; English translation: .] Paul Bernays
Paul Isaac Bernays (17 October 1888 – 18 September 1977) was a Swiss mathematician who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant and close collaborator of ...
reformulated von Neumann's theory by taking class and set as primitive notions.
[, pp. 66–67.] Kurt Gödel
Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imm ...
simplified Bernays' theory for his
relative consistency
In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent i ...
proof of the
axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
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
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
"
[.]—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
A choice function (selector, selection) is a mathematical function ''f'' that is defined on some collection ''X'' of nonempty sets and assigns some element of each set ''S'' in that collection to ''S'' by ''f''(''S''); ''f''(''S'') maps ''S'' to ...
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-order
In mathematics, a well-order (or well-ordering or well-order relation) on a set ''S'' is a total order on ''S'' with the property that every non-empty subset of ''S'' has a least element in this ordering. The set ''S'' together with the well-or ...
ed by
. So, by definition,
is an ordinal. Hence,
, which contradicts
being a well-ordering of
Therefore,
is not a set. Because a class that is not a set is called a
proper class
Proper may refer to:
Mathematics
* Proper map, in topology, a property of continuous function between topological spaces, if inverse images of compact subsets are compact
* Proper morphism, in algebraic geometry, an analogue of a proper map f ...
,
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
An image is a visual representation of something. It can be two-dimensional, three-dimensional, or somehow otherwise feed into the visual system to convey information. An image can be an artifact, such as a photograph or other two-dimensio ...
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 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. Bernays used
many-sorted logic
Many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming. Both functional and assertive "parts of speech" ...
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
Elliott Mendelson (May 24, 1931 – May 7, 2020) was an American logician. He was a professor of mathematics at Queens College of the City University of New York, and the Graduate Center, CUNY. He was Jr. Fellow, Society of Fellows, Harvard Un ...
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
In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range.
Overview
The doma ...
.
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.
: