Von Neumann–Bernays–Gödel set theory


In the foundations of mathematics, von Neumann–Bernays–Gödel set theory is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel-Choice set theory. 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 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 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:
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 with two sorts: classes and sets. Gödel avoided sorts by introducing primitive predicates: for " is a class" and for " is a set". 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 does not affect what can be proved, but it does 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:
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 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.
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 :
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 to the tuples of a given class.
Next, the variables are put in the same order to prepare for the intersection:
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. For any two classes and, there is a class consisting precisely of the sets that belong to both and.
Complement. For any class, there is a class consisting precisely of the sets not belonging to.
Domain. 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. On the other hand, extensionality is not applicable to in the membership axiom since it specifies only those sets in that are ordered pairs.
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 3tuples are obtained by applying the circular permutation to the 3tuples of.
Transposition. For any class, there is a class whose 3tuples are obtained by transposing the last two components of the 3tuples 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 : and If is a class, extensionality implies that is the unique class consisting of the 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 3tuples of class By specifying the 3tuples, these axioms also specify the 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.
Proof: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 . Then for all, there exists a unique class of such that: The class is denoted by
The theorem's proof will be done in two steps:
  1. 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.
  2. 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 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.
  1. is transformed into
  2. Extensionality is used to transform into
  3. 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.
  2. If a formula contains no free set variables other than then bound variables that are nested within quantifiers are replaced with These variables have nesting depth.
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.
Proof of the class existence theorem for transformed formulas
The following lemma is used in the proof.
Let and let be a class containing all the ordered pairs satisfying That is, Then can be expanded into the unique class of satisfying. That is,
1. 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 satisfying
2. 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 satisfying
3. 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 satisfying
4. Let Extensionality implies that is the unique class of satisfying
Let be a formula that:
1. contains no free variables other than ;
2. contains only,,,, set variables, and the class variables where does not appear before an ;

3. only quantifies set variables where is the quantifier nesting depth of the variable.
Then for all, there exists a unique class of such that:
has 0 logical symbols. The theorem's hypothesis implies that is an atomic formula of the form or
If is, we build the class the unique class of satisfying
is where The axiom of membership produces a class containing all the ordered pairs satisfying Apply the expansion lemma to to obtain
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
is where Since this formula is false by the axiom of regularity, no satisfy it, so
If is, we build the class the unique class of satisfying
is where Apply the axiom of product by to to produce the class Apply the expansion lemma to to obtain
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
is where Then
has logical symbols where. Assume the induction hypothesis that the theorem is true for all with less than logical symbols. We now prove the theorem for with logical symbols. In this proof, the list of class variables is abbreviated by, so a formula—such as —can be written as
Since has logical symbols, the induction hypothesis implies that there is a unique class of such that:
By the complement axiom, there is a class such that However, contains elements other than if To eliminate these elements, use which is the complement relative to the class of all Then, by extensionality, is the unique class of such that:
Since both and have less than logical symbols, the induction hypothesis implies that there are unique classes of and, such that:
By the axioms of intersection and extensionality, is the unique class of such that:
The quantifier nesting depth of is one more than that of and the additional free variable is Since has logical symbols, the induction hypothesis implies that there is a unique class of such that:
By the axioms of domain and extensionality, is the unique class of such that:

Gödel pointed out that the class existence theorem "is a metatheorem, that is, a theorem about the system , not in the system …" 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 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, this 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-style case statement.
Let be the formula of [|example 2]. The function call generates the class which is compared below with This shows that the construction of the class mirrors the construction of its defining formula

Extending the class existence theorem

Gödel extended the class existence theorem to formulas containing relations over classes, special classes, and operations. To extend the class existence theorem, the formulas defining relations, special classes, and operations must quantify only over sets. Then can be transformed into an equivalent formula satisfying the [|hypothesis of the class existence theorem].
The following definitions specify how formulas define relations, special classes, and operations:
  1. A relation is defined by:
  2. A special class is defined by:
  3. An operation is defined by:
A is defined by:
  1. Variables and special classes are terms.
  2. If is an operation with arguments and are terms, then 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, is chosen so that differs from the other variables in the current formula. The rules are repeated until there are no subformulas to which they can be applied. and denote terms.
This example illustrates how the transformation rules work together to eliminate an operation.
Class existence theorem. Let be a formula that quantifies only over sets, contains no free variables other than, and may contain relations, special classes, and operations defined by formulas that quantify only over sets. Then for all there exists a unique class of such that
Proof: Apply the transformation rules to 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 there is a unique class of satisfying

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. is a function if
In set theory, the definition of a function does not require specifying the domain or codomain of the function. 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, union, and power set are also generalized to class operations. The image of class under the function is This definition does not require that The union of class is The power class of is The extended version of the class existence theorem implies the existence of these classes. The axioms of replacement, union, and power set imply that when these operations are applied to sets, they produce sets.
Axiom of replacement. If is a function and is a set, then, the image of under, is a set.
Not having the requirement in the definition of produces a stronger axiom of replacement, which is used in the following proof.
Theorem. If is a set and is a subclass of then is a set.
Proof: The class existence theorem constructs the restriction of the identity function to : Since the image of under is, the axiom of replacement implies that is a set. This proof depends on the definition of image not having the requirement since rather than
Axiom of union. If is a set, then there is a set containing
Axiom of power set. If is a set, then there is a set containing
Theorem. If is a set, then and are sets.
Proof: The axiom of union states that is a subclass of a set, so the axiom of separation implies is a set. Likewise, the axiom of power set states that is a subclass of a set, so the axiom of separation implies that is a set.
Axiom of infinity. There exists a nonempty set such that for all in, there exists a in such that is a proper subset of.
The axioms of infinity and replacement prove the existence of the empty set. In the [|discussion of the class existence axioms], the existence of the empty class was proved. We now prove that is a set. Let function and let be the set given by the axiom of infinity. By replacement, the image of under, which equals, is a set.
NBG's axiom of infinity is implied by ZFC's axiom of infinity: The first conjunct of ZFC's axiom,, implies the first conjunct of NBG's axiom. The second conjunct of ZFC's axiom,, implies the second conjunct of NBG's axiom since To prove ZFC's axiom of infinity from NBG's axiom of infinity requires some of the other NBG axioms.

Axiom of global choice

The class concept allows NBG to have a stronger axiom of choice than ZFC. A choice function is a function defined on a set of nonempty sets such that for all 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 defined on the class of all nonempty sets such that for every nonempty set 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 of nonempty sets, is a choice function for In 1964, William B. Easton proved that global choice is stronger than the axiom of choice by using forcing to construct a model that satisfies the axiom of choice and all the axioms of NBG except the axiom of global choice. 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.
Axiom of global choice. There exists a function that chooses an element from every nonempty set.

History

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. Von Neumann based his axiom system on two domains of 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 rather than a 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 ∈ a if ≠ A.
Von Neumann's work in set theory was influenced by Georg Cantor's articles, Ernst Zermelo's 1908 axioms for set theory, and the 1922 critiques of 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 where Z0 is the set of natural numbers and Zn+1 is the power set of Zn. They then introduced the axiom of replacement, which would guarantee the existence of such sets. 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".
Von Neumann worked on the problems of Zermelo set theory and provided solutions for some of them:
In 1929, von Neumann published an article containing the axioms that would lead to NBG. 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 consistency is not even more problematic than an axiomatization of set theory that does not go beyond the necessary Cantorian framework."
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."
Let S be von Neumann's 1929 axiom system. Von Neumann introduced the axiom system S + Regularity to demonstrate that his 1925 system is consistent relative to S. He proved:
  1. If S is consistent, then S + Regularity is consistent.
  2. 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. 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, 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

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. Bernays stated that:
Bernays handled sets and classes in a 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.

Gödel's axiom system (NBG)

In 1931, Bernays sent a letter containing his set theory to Kurt Gödel. 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. Gödel used his axioms in his 1940 monograph on the relative consistency of global choice and the generalized continuum hypothesis.
Several reasons have been given for Gödel choosing NBG for his monograph:
Gödel's achievement together with the details of his presentation led to the prominence that NBG would enjoy for the next two decades. In 1963, Paul Cohen proved his independence proofs for ZF with the help of some tools that Gödel had developed for his relative consistency proofs for NBG. Later, ZFC became more popular than NBG. This was caused by several factors, including the extra work required to handle forcing in NBG, Cohen's 1966 presentation of forcing, which used ZF, and the proof that NBG is a conservative extension of ZFC.

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, NBG 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.
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 ∅ = ∅ and ∅ ≠ ∅, 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] 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. For a survey of known results of this nature, see.
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, while Gödel's second incompleteness theorem implies that NBG cannot prove the consistency of NBG.
For a discussion of some ontological and other philosophical issues posed by NBG, especially when contrasted with ZFC and MK, see Appendix C of.

Models

ZFC, NBG, and MK have models describable in terms of the cumulative hierarchy Vα and the constructible hierarchy Lα. Let V include an inaccessible cardinal κ, let X ⊆ Vκ, and let Def denote the class of first-order definable subsets of X with parameters. In symbols where "" denotes the model with domain and relation, and "" denotes the satisfaction relation:
Then:
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 objects and morphisms 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, 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. On whether an ontology including classes as well as sets is adequate for category theory, see.