Von Neumann–Bernays–Gödel set theory

Ontology

The defining aspect of NBG is the distinction between proper class and set. Let a and s be two individuals. Then the atomic sentence a ∈ s is defined if a is a set and s is a class. In other words, a ∈ s is defined unless a is a proper class. A proper class is very large; NBG even admits of "the class of all sets", the universal class called V. However, NBG does not admit "the class of all classes" (which fails because proper classes are not "objects" that can be put into classes in NBG) or "the set of all sets" (whose existence cannot be justified with NBG axioms).

By NBG's axiom schema of class comprehension, all objects satisfying any given formula in the first-order language of NBG form a class; if a class is not a set in ZFC, it is an NBG proper class.

The development of classes mirrors the development of naive set theory. The principle of abstraction is given, and thus classes can be formed out of all individuals satisfying any statement of first-order logic whose atomic sentences all involve either the membership relation or predicates definable from membership. Equality, pairing, subclass, and such, are all definable and so need not be axiomatized – their definitions denote a particular abstraction of a formula.

Sets are developed in a manner very similarly to ZF. Let Rp(A,a), meaning "the set a represents the class A," denote a binary relation defined as follows:

That is, a "represents" A if every element of a is an element of A, and conversely. Classes lacking representations, such as the class of all sets that do not contain themselves (the class invoked by the Russell paradox), are the proper classes.

History

In two articles published in 1925 and 1928, John von Neumann stated his axioms and showed they were adequate to develop set theory. Von Neumann took functions and arguments as primitives. His functions correspond to classes, and functions that can be used as arguments correspond to sets. In fact, he defined classes and sets using functions that can take only two values (that is, indicator functions whose domain is the class of all arguments).

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 {Z₀, Z₁, Z₂, ... } where Z₀ is the set of natural numbers, and Z_n+1 is the power set of Z_n. They then introduced the axiom of replacement, which would guarantee the existence of such sets. However, they were reluctant to adopt this axiom: Fraenkel's opinion was "that Replacement was too strong an axiom for 'general set theory' ... and ... Skolem only wrote that 'we could introduce' Replacement".

Von Neumann worked on the deficiencies in Zermelo's set theory and introduced several innovations to remedy them, including:

A theory of ordinals. Zermelo's set theory does not contain Cantor's theory of ordinal numbers. Von Neumann recovered this theory by defining the ordinals using sets that are well-ordered by the ∈-relation. In contrast to Fraenkel and Skolem, von Neumann found the axiom of replacement so essential to his work that he declared: "In fact, I believe that no theory of ordinals is possible at all without this axiom."

A criterion identifying classes that are too large to be sets. Zermelo did not provide such a criterion. His set theory avoids the large classes that lead to the paradoxes, but it leaves out many sets, such as the one mentioned by Fraenkel and Skolem. Von Neumann's criterion is: A class is too large to be a set if and only if it can be mapped onto the universal class. Von Neumann realized that the paradoxes can be avoided by not allowing such large classes to be members of any class. Combining this restriction with his criterion, he obtained his axiom of limitation of size: A class X is not a member of any class if and only if X can be mapped onto the universal class.

Finite axiomatization. Fraenkel and Skolem formalized Zermelo's imprecise concept of "definite propositional function", which appears in his axiom of separation. Skolem gave the axiom schema of separation that is currently used in ZFC; Fraenkel gave an equivalent approach. Zermelo rejected both approaches "particularly because they implicitly involve the concept of natural number which, in Zermelo's view, should be based upon set theory." Von Neumann avoided axiom schemas by formalizing the concept of "definite propositional function" with his functions, whose construction requires only finitely many axioms. This led to his set theory having finitely many axioms. In 1961, Richard Montague proved that ZFC cannot be finitely axiomatized.

The axiom of regularity. Zermelo's set theory does not exclude non-well-founded sets. Fraenkel and von Neumann introduced axioms to exclude these sets. Von Neumann introduced the axiom of regularity, which states that all sets are well-founded. However, von Neumann did not adopt regularity in his axiom system. In 1930, Zermelo became the first to include regularity in an axiom system.

In 1929, von Neumann published his last article on set theory, which contains the axioms that would lead to NGB. Von Neumann wrote that his axiom of limitation of size "does a lot, actually too much." It implies 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—he said that this went beyond Cantorian set theory. He 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 approached this consistency problem by first replacing the axiom of limitation of size with two of its consequences—namely, replacement and the choice axiom: "Every relation R has a subclass which is a function and has the same domain as R. This axiom is equivalent to the axiom of global choice. Next, he proved that if this weaker axiom system is consistent, it remains consistent after adding the axiom of regularity. This produces the axiom system that (after modifications by Bernays and Gödel) would become NBG. Finally, he showed that this axiom system implies the axiom of limitation of size. Therefore, his 1925 axiom system is relatively consistent with an axiom system that is closer to ZFC—the major remaining differences are that this system uses classes and its choice axiom is stronger.

In 1929, Paul Bernays started modifying this axiom system by taking classes and sets as primitives. He published his work in a series of articles appearing from 1937 to 1954. By using sets, Bernays was following the tradition established by Cantor, Richard Dedekind, and Zermelo. His classes followed the tradition of Boolean algebra since they permit the operation of complement as well as union and intersection. 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, Bernays rewrote and simplified von Neumann's 1929 axioms.

Kurt Gödel simplified Bernays' theory by making every set a class, which allowed him to use just one sort for classes and one membership primitive. Gödel modified some of Bernays' axioms and replaced von Neumann's choice axiom with the axiom of global choice. He 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 1940 monograph:

Gödel gave a mathematical reason—NBG's global choice produces a stronger consistency theorem: "This stronger form of the axiom [of choice], if consistent with the other axioms, implies, of course, that a weaker form is also consistent."

Robert Solovay conjectured: "My guess is that he [Gödel] wished to avoid a discussion of the technicalities involved in developing the rudiments of model theory within axiomatic set theory."

Kenneth Kunen gave a reason for Gödel avoiding this discussion: "There is also a much more combinatorial approach to L [the constructible universe], developed by ... [Gödel in his 1940 monograph] in an attempt to explain his work to non-logicians. ... This approach has the merit of removing all vestiges of logic from the treatment of L."

Charles Parsons provided a philosophical reason for Gödel's choice of NBG: "This view [that 'property of set' is a primitive of set theory] may be reflected in Gödel's choice of a theory with class variables as the framework for ... [his monograph]."

Gödel's achievement together with the details of his presentation led to the prominence that NBG would enjoy for the next two decades. Even Paul Cohen's 1963 independence proofs for ZF used tools that Gödel developed for his work in NBG. However, in the 1960s, 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 uses techniques that naturally belong to ZF), and the proof that NBG is a conservative extension of ZFC.

Axiomatizating NBG

NBG is presented here as a two-sorted theory, with lower case letters denoting variables ranging over sets, and upper case letters denoting variables ranging over classes. Hence " x ∈ y " should be read "set x is a member of set y," and " x ∈ Y " as "set x is a member of class Y." Statements of equality may take the form " x = y " or " X = Y ". The statement " a = A " stands for " ∀ x ( x ∈ a ↔ x ∈ A ) " and is an abuse of notation. NBG can also be presented as a one-sorted theory of classes, with sets being those classes that are members of at least one other class.

We first axiomatize NBG using the axiom schema of Class Comprehension. This schema is provably equivalent to 9 of its finite instances, stated in the following section. Hence these 9 finite axioms can replace Class Comprehension. This is the precise sense in which NBG can be finitely axiomatized.

With Class Comprehension schema

The following five axioms are identical to their ZFC counterparts:

extensionality: ∀ a ∀ b [ ∀ x ( x ∈ a ↔ x ∈ b ) → a = b ] . Sets with the same elements are the same set.

pairing: ∀ x ∀ y ∃ z ∀ w [ w ∈ z ↔ ( w = x ∨ w = y ) ] . For any sets x and y, there is a set, { x , y } , whose elements are exactly x and y.

pairing implies that for any set x, the set {x} (the singleton set) exists. Also, given any two sets x and y and the usual set-theoretic definition of the ordered pair, the ordered pair (x,y) exists and is a set. By Class Comprehension, all relations on sets are classes. Moreover, certain kinds of class relations are one or more of functions, injections, and bijections from one class to another. pairing is an axiom in Zermelo set theory and a theorem in ZFC.

union: For any set x, there is a set which contains exactly the elements of elements of x.

power set: For any set x, there is a set which contains exactly the subsets of x.

infinity: There exists an inductive set, namely a set x whose members are (i) the empty set; (ii) for every member y of x, y ∪ { y } is also a member of x.

infinity can be formulated so as to imply the existence of the empty set.

The remaining axioms have capitalized names because they are primarily concerned with classes rather than sets. The next two axioms differ from their ZFC counterparts only in that their quantified variables range over classes, not sets:

Extensionality: ∀ x ( x ∈ A ↔ x ∈ B ) → A = B . : Classes with the same elements are the same class.

Foundation (Regularity): Each nonempty class is disjoint from one of its elements.

The last two axioms are peculiar to NBG:

Limitation of Size: For any class C, a set x such that x=C exists if and only if there is no bijection between C and the class V of all sets.

From this axiom, due to von Neumann, Subsets, Replacement, and Global Choice can all be derived. This axiom implies the axiom of global choice because the class of ordinals is not a set; hence there exists a bijection between the ordinals and the universe. If Limitation of Size were weakened to "If the domain of a class function is a set, then the range of that function is likewise a set," then no form of the axiom of choice is an NBG theorem. In this case, any of the usual local forms of Choice may be taken as an added axiom, if desired. Limitation of Size cannot be found in Mendelson (1997) NBG. In its place, we find the usual axiom of choice for sets, and the following form of the axiom schema of replacement: if the class F is a function whose domain is a set, the range of F is also a set .

Class Comprehension schema: For any formula ϕ containing no quantifiers over classes (it may contain class and set parameters), there is a class A such that ∀ x ( x ∈ A ↔ ϕ ( x ) ) .

This axiom asserts that invoking the principle of unrestricted comprehension of naive set theory yields a class rather than a set, thereby banishing the paradoxes of set theory. Class Comprehension is the only axiom schema of NBG. In the next section, we show how this schema can be replaced by a number of its own instances. Hence NBG can be finitely axiomatized. If the quantified variables in φ(x) range over classes instead of sets, the result is Morse–Kelley set theory, a proper extension of ZFC which cannot be finitely axiomatized.

Replacing Class Comprehension with finite instances thereof

An appealing but somewhat mysterious feature of NBG is that its axiom schema of Class Comprehension is equivalent to the conjunction of a finite number of its instances. The axioms of this section may replace the Axiom Schema of Class Comprehension in the preceding section. The finite axiomatization presented below does not necessarily resemble exactly any NBG axiomatization in print.

We develop our axiomatization by considering the structure of formulas.

Sets: For any set x, there is a class X such that x=X.

This axiom, in combination with the set existence axioms from the previous axiomatization, assures the existence of classes from the outset, and enables formulas with class parameters.

Let A = { x ∣ ϕ } and B = { x ∣ ψ } . Then { x ∣ ¬ ϕ } = V − A and { x ∣ ϕ ∧ ψ } = A ∩ B suffice for handling all sentential connectives, because ∧ and ¬ are a functionally complete set of connectives.

Complement: For any class A, the complement V − A = { x ∣ x ∉ A } is a class.

Intersection: For any classes A and B, the intersection A ∩ B = { x ∣ x ∈ A ∧ x ∈ B } is a class.

We now turn to quantification. In order to handle multiple variables, we need the ability to represent relations. Define the ordered pair ( a , b ) as { { a } , { a , b } } , as usual. Note that three applications of pairing to a and b assure that (a,b) is indeed a set.

Products: For any classes A and B, the class A × B = { ( a , b ) ∣ a ∈ A ∧ b ∈ B } is a class. (In practice, only V × A is needed.)

Converses: For any class R, the classes:

C o n v 1 ( R ) = { ( b , a ) ∣ ( a , b ) ∈ R } and C o n v 2 ( R ) = { ( b , ( a , c ) ) ∣ ( a , ( b , c ) ) ∈ R } exist.

Association: For any class R, the classes:

A s s o c 1 ( R ) = { ( ( a , b ) , c ) ∣ ( a , ( b , c ) ) ∈ R } and A s s o c 2 ( R ) = { ( d , ( a , ( b , c ) ) ) ∣ ( d , ( ( a , b ) , c ) ) ∈ R } exist.

These axioms license adding dummy arguments, and rearranging the order of arguments, in relations of any arity. The peculiar form of Association is designed exactly to make it possible to bring any term in a list of arguments to the front (with the help of Converses). We represent the argument list ( x 1 , x 2 , … , x n ) as ( x 1 , ( x 2 , … , x n ) ) (it is a pair with the first argument as its first projection and the "tail" of the argument list as the second projection). The idea is to apply Assoc1 until the argument to be brought to the front is second, then apply Conv1 or Conv2 as appropriate to bring the second argument to the front, then apply Assoc2 until the effects of the original applications of Assoc1 (which are now behind the moved argument) are corrected.

If { ( x , y ) ∣ ϕ ( x , y ) } is a class considered as a relation, then its range, { y ∣ ∃ x [ ϕ ( x , y ) ] } , is a class. This gives us the existential quantifier. The universal quantifier can be defined in terms of the existential quantifier and negation.

Ranges: For any class R, the class R n g ( R ) = { y ∣ ∃ x [ ( x , y ) ∈ R ] } exists.

The above axioms can reorder the arguments of any relation so as to bring any desired argument to the front of the argument list, where it can be quantified.

Finally, each atomic formula implies the existence of a corresponding class relation:

Membership: The class [ ∈ ] = { ( x , y ) ∣ x ∈ y } exists.

Diagonal: The class [ = ] = { ( x , y ) ∣ x = y } exists.

Diagonal, together with addition of dummy arguments and rearrangement of arguments, can build a relation asserting the equality of any two of its arguments; thus repeated variables can be handled.

Mendelson's variant

Mendelson refers to his axioms B1-B7 of class comprehension as "axioms of class existence." Four of these identical to axioms already stated above: B1 is Membership; B2, Intersection; B3, Complement; B5, Product. B4 is Ranges modified to assert the existence of the domain of R (by existentially quantifying y instead of x). The last two axioms are:

B6: ∀ X ∃ Y ∀ u v w [ ( u , v , w ) ∈ Y ↔ ( v , w , u ) ∈ X ] , B7: ∀ X ∃ Y ∀ u v w [ ( u , v , w ) ∈ Y ↔ ( u , w , v ) ∈ X ] .

B6 and B7 enable what Converses and Association enable: given any class X of ordered triples, there exists another class Y whose members are the members of X each reordered in the same way.

Discussion

For a discussion of some ontological and other philosophical issues posed by NBG, especially when contrasted with ZFC and MK, see Appendix C of Potter (2004).

Even though NBG is a conservative extension of ZFC, a theorem may have a shorter and more elegant proof in NBG than in ZFC (or vice versa). For a survey of known results of this nature, see Pudlak (1998).

Model theory

ZFC, NBG, and MK have models describable in terms of V, the standard model of ZFC and the von Neumann universe. Now let the members of V include the inaccessible cardinal κ. Also let Def(X) denote the Δ₀ definable subsets of X (see constructible universe). Then:

V_κ is an intended model of ZFC;

Def(V_κ) is an intended model of Mendelson's version of NBG which excludes global choice, replacing limitation of size by replacement and ordinary choice;

V_κ+1 is an intended model of MK.

Note that Def(V_κ) is not necessarily a model of NBG, since Limitation of Size might fail; in the other two cases the structures are always models of ZFC and MK, respectively.

Category theory

The ontology of NBG provides scaffolding for speaking about "large objects" without risking paradox. In some developments of category theory, for instance, a "large category" is defined as one whose objects make up a proper class, with the same being true of its morphisms. A "small category", on the other hand, is one whose objects and morphisms are members of some set. We can thus easily speak of the "category of all sets" or "category of all small categories" without risking paradox. Those categories are large, of course. There is no "category of all categories" since it would have to contain large categories which no category can do. Although yet another ontological extension can enable one to talk formally about such a "category" (see for example the "quasicategory of all categories" of Adámek et al. (1990), whose objects and morphisms form a "proper conglomerate").

On whether an ontology including classes as well as sets is adequate for category theory, see Muller (2001).