Von Neumann–Bernays–Gödel set theory

Case a: [math]\displaystyle{ \phi }[/math] is [math]\displaystyle{ x_i \in x_j }[/math] where [math]\displaystyle{ i \lt j. }[/math] The axiom of membership produces a class [math]\displaystyle{ P }[/math] containing all the ordered pairs [math]\displaystyle{ (x_i, x_j) }[/math] satisfying [math]\displaystyle{ x_i \in x_j. }[/math] Apply the expansion lemma to [math]\displaystyle{ P }[/math] to obtain [math]\displaystyle{ E_{i,j,n} = \{(x_1, \ldots, x_{n}): x_i \in x_j\}. }[/math]

Case b: [math]\displaystyle{ \phi }[/math] is [math]\displaystyle{ x_i \in x_j }[/math] where [math]\displaystyle{ i \gt j. }[/math] The axiom of membership produces a class [math]\displaystyle{ P }[/math] containing all the ordered pairs [math]\displaystyle{ (x_i, x_j) }[/math] satisfying [math]\displaystyle{ x_i \in x_j. }[/math] Apply the tuple lemma's statement 4 to [math]\displaystyle{ P }[/math] to obtain [math]\displaystyle{ P' }[/math] containing all the ordered pairs [math]\displaystyle{ (x_j, x_i) }[/math] satisfying [math]\displaystyle{ x_i \in x_j. }[/math] Apply the expansion lemma to [math]\displaystyle{ P' }[/math] to obtain [math]\displaystyle{ E_{i,j,n} = \{(x_1, \ldots, x_{n}): x_i \in x_j\}. }[/math]

Case c: [math]\displaystyle{ \phi }[/math] is [math]\displaystyle{ x_i \in x_j }[/math] where [math]\displaystyle{ i = j. }[/math] Since this formula is false by the axiom of regularity, no [math]\displaystyle{ n }[/math]-tuples satisfy it, so [math]\displaystyle{ E_{i,j,n} = \empty. }[/math]

Case 2: If [math]\displaystyle{ \phi }[/math] is [math]\displaystyle{ x_i \in Y_k }[/math], we build the class [math]\displaystyle{ E_{i,Y_k,n} = \{(x_1, \ldots, x_{n}): x_i \in Y_k\}, }[/math] the unique class of [math]\displaystyle{ n }[/math]-tuples satisfying [math]\displaystyle{ x_i \in Y_k. }[/math]

Gödel pointed out that the class existence theorem "is a metatheorem, that is, a theorem about the system [NBG], not in the system …"^[30] 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, the 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.^{[lower-alpha 9]} [math]\displaystyle{ \begin{array}{l} \mathbf{function} \;\text{Class}(\phi, \,n) \\ \quad\begin{array}{rl} \mathbf{input}\!: \;\,&\phi \text{ is a transformed formula of the form } \phi(x_1, \ldots, x_n, Y_1, \ldots, Y_m); \\ &n \text{ specifies that a class of } n\text{-tuples is returned.} \\ \;\;\;\;\mathbf{output}\!: \;\,&\text{class } A \text{ of } n\text{-tuples satisfying } \\ &\,\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)]. \end{array} \\ \mathbf{begin} \\ \quad \mathbf{case} \;\phi \;\mathbf{of} \\ \qquad \begin{alignat}{2} x_i \in x_j: \;\;&\mathbf{return} \;\,E_{i,j,n}; &&\text{// } E_{i,j,n} \;\,= \{(x_1, \dots, x_n): x_i \in x_j\} \\ x_i \in Y_k: \;\;&\mathbf{return} \;\,E_{i,Y_k,n}; &&\text{// } E_{i,Y_k,n} = \{(x_1, \dots, x_{n}): x_i \in Y_k\} \\ \neg\psi: \;\;&\mathbf{return} \;\,\complement_{V^n}\text{Class}(\psi, \,n); &&\text{// } \complement_{V^n}\text{Class}(\psi, \,n) = V^n \setminus \text{Class}(\psi, \,n) \\ \psi_1 \land \psi_2: \;\;&\mathbf{return} \;\,\text{Class}(\psi_1, \,n) \cap \text{Class}(\psi_2, \,n);&& \\ \;\;\;\;\,\exists x_{n+1}(\psi): \;\;&\mathbf{return} \;\,Dom(\text{Class}(\psi, \,n+1)); &&\text{// } x_{n+1} \text{ is free in } \psi; \text{ Class}(\psi, \,n+1) \\ &\ &&\text{// returns a class of } (n+1)\text{-tuples} \end{alignat} \\ \quad \mathbf{end} \\ \mathbf{end} \end{array} }[/math]

Let [math]\displaystyle{ \phi }[/math] be the formula of example 2. The function call [math]\displaystyle{ A = Class(\phi, 1) }[/math] generates the class [math]\displaystyle{ A, }[/math] which is compared below with [math]\displaystyle{ \phi. }[/math] This shows that the construction of the class [math]\displaystyle{ A }[/math] mirrors the construction of its defining formula [math]\displaystyle{ \phi. }[/math]

[math]\displaystyle{ \begin{alignat}{2} &\phi \;&&= \;\;\exists x_2\,(x_2 \!\in\! x_1 \land \;\;\neg\;\;\;\;\exists x_3\;(x_3 \!\in\! x_2)) \,\land \;\;\,\exists x_2\,(x_2 \!\in\! x_1 \land \;\;\,\exists x_3\,(x_3 \!\in\! x_2 \,\land\;\;\neg\;\;\;\;\exists x_4\;(x_4 \!\in\! x_3))) \\ &A \;&&= Dom\,(\;E_{2,1,2}\; \cap \;\complement_{V^2}\,Dom\,(\;E_{3,2,3}\;)) \,\cap\, Dom\,(\;E_{2,1,2}\;\cap \, Dom\,(\;\,E_{3,2,3}\; \cap \;\complement_{V^3}\,Dom\,(\;E_{4,3,4}\;))) \end{alignat} }[/math]

Extending the class existence theorem

Gödel extended the class existence theorem to formulas [math]\displaystyle{ \phi }[/math] containing relations over classes (such as [math]\displaystyle{ Y_1 \subseteq Y_2 }[/math] and the unary relation [math]\displaystyle{ M(Y_1) }[/math]), special classes (such as [math]\displaystyle{ Ord }[/math] ), and operations (such as [math]\displaystyle{ (x_1, x_2) }[/math] and [math]\displaystyle{ x_1 \cap Y_1 }[/math]).^[32] To extend the class existence theorem, the formulas defining relations, special classes, and operations must quantify only over sets. Then [math]\displaystyle{ \phi }[/math] 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 [math]\displaystyle{ R }[/math] is defined by: [math]\displaystyle{ R(Z_1, \dots, Z_k) \iff \psi_R(Z_1, \dots, Z_k). }[/math]
2. A special class [math]\displaystyle{ C }[/math] is defined by: [math]\displaystyle{ u \in C \iff \psi_C(u). }[/math]
3. An operation [math]\displaystyle{ P }[/math] is defined by: [math]\displaystyle{ u \in P(Z_1, \dots, Z_k) \iff \psi_P(u, Z_1, \dots, Z_k). }[/math]

A term is defined by:

1. Variables and special classes are terms.
2. If [math]\displaystyle{ P }[/math] is an operation with [math]\displaystyle{ k }[/math] arguments and [math]\displaystyle{ \Gamma_1, \dots, \Gamma_k }[/math] are terms, then [math]\displaystyle{ P(\Gamma_1, \dots, \Gamma_k) }[/math] 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, [math]\displaystyle{ i }[/math] is chosen so that [math]\displaystyle{ z_i }[/math] differs from the other variables in the current formula. The rules are repeated until there are no subformulas to which they can be applied. [math]\displaystyle{ \, \Gamma_1, \dots, \Gamma_k, \Gamma, }[/math] and [math]\displaystyle{ \Delta }[/math] denote terms.

1. A relation [math]\displaystyle{ R(Z_1, \dots, Z_k) }[/math] is replaced by its defining formula [math]\displaystyle{ \psi_R(Z_1, \dots, Z_k). }[/math]
2. Let [math]\displaystyle{ \psi_C(u) }[/math] be the defining formula for the special class [math]\displaystyle{ C. }[/math]
   1. [math]\displaystyle{ \Delta \in C }[/math] is replaced by [math]\displaystyle{ \psi_C(\Delta). }[/math]
   2. [math]\displaystyle{ C \in \Delta }[/math] is replaced by [math]\displaystyle{ \exists z_i[z_i = C \land z_i \in \Delta]. }[/math]
3. Let [math]\displaystyle{ \psi_P(u, Z_1, \dots, Z_k) }[/math] be the defining formula for the operation [math]\displaystyle{ P(Z_1, \dots, Z_k). }[/math]
   1. [math]\displaystyle{ \Delta \in P(\Gamma_1, \dots, \Gamma_k) }[/math] is replaced by [math]\displaystyle{ \psi_P(\Delta, \Gamma_1, \dots, \Gamma_k). }[/math]
   2. [math]\displaystyle{ P(\Gamma_1, \dots, \Gamma_k) \in \Delta }[/math] is replaced by [math]\displaystyle{ \exists z_i[z_i = P(\Gamma_1, \dots, \Gamma_k) \land z_i \in \Delta]. }[/math]
4. Extensionality is used to transform [math]\displaystyle{ \Delta = \Gamma }[/math] into [math]\displaystyle{ \forall z_i(z_i \in \Delta \iff z_i \in \Gamma). }[/math]

Example 3:  Transforming [math]\displaystyle{ Y_1 \subseteq Y_2. }[/math] [math]\displaystyle{ Y_1 \subseteq Y_2 \iff \forall z_1(z_1 \in Y_1 \implies z_1 \in Y_2) \quad\text{(rule 1)} }[/math]

Example 4:  Transforming [math]\displaystyle{ x_1 \cap Y_1 \in x_2. }[/math] [math]\displaystyle{ \begin{alignat}{2} x_1 \cap Y_1 \in x_2 &\iff \exists z_1[z_1 = x_1 \cap Y_1 \,\land\, z_1 \in x_2] &&\text{(rule 3b)} \\ &\iff \exists z_1[\forall z_2(z_2 \in z_1 \iff z_2 \in x_1 \cap Y_1) \,\land\, z_1 \in x_2] &&\text{(rule 4)} \\ &\iff \exists z_1[\forall z_2(z_2 \in z_1 \iff z_2 \in x_1 \land z_2 \in Y_1) \,\land\, z_1 \in x_2] \quad&&\text{(rule 3a)} \\ \end{alignat} }[/math] This example illustrates how the transformation rules work together to eliminate an operation.

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.  [math]\displaystyle{ F }[/math] is a function if [math]\displaystyle{ F \subseteq V^2 \land \forall x\, \forall y\, \forall z\, [(x,y) \in F \,\land\, (x,z) \in F \implies y = z]. }[/math]

In set theory, the definition of a function does not require specifying the domain or codomain of the function (see Function (set theory)). 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 [math]\displaystyle{ A }[/math] under the function [math]\displaystyle{ F }[/math] is [math]\displaystyle{ F[A] = \{y: \exists x(x \in A \,\land\, (x, y) \in F)\}. }[/math] This definition does not require that [math]\displaystyle{ A \subseteq Dom(F). }[/math] The union of class [math]\displaystyle{ A }[/math] is [math]\displaystyle{ \cup A = \{x: \exists y(x \in y\, \,\land\, y \in A)\}. }[/math] The power class of [math]\displaystyle{ A }[/math] is [math]\displaystyle{ \mathcal{P}(A) = \{x: x \subseteq A\}. }[/math] 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.^[34]

Axiom of replacement.  If [math]\displaystyle{ F }[/math] is a function and [math]\displaystyle{ a }[/math] is a set, then [math]\displaystyle{ F[a] }[/math], the image of [math]\displaystyle{ a }[/math] under [math]\displaystyle{ F }[/math], is a set. [math]\displaystyle{ \forall F \,\forall a \,[F \text{ is a function}\implies \exists b \,\forall y\,(y \in b \iff \exists x(x \in a \,\land\, (x, y) \in F))]. }[/math]

Not having the requirement [math]\displaystyle{ A \subseteq Dom(F) }[/math] in the definition of [math]\displaystyle{ F[A] }[/math] produces a stronger axiom of replacement, which is used in the following proof.

Axiom of union.  If [math]\displaystyle{ a }[/math] is a set, then there is a set containing [math]\displaystyle{ \cup a. }[/math] [math]\displaystyle{ \forall a\, \exists b\, \forall x\,[\,\exists y(x \in y\, \,\land\, y \in a) \implies x \in b\,]. }[/math]

Axiom of power set.  If [math]\displaystyle{ a }[/math] is a set, then there is a set containing [math]\displaystyle{ \mathcal{P}(a). }[/math]

[math]\displaystyle{ \forall a\, \exists b\, \forall x\, (x \subseteq a \implies x \in b). }[/math]^{[lower-alpha 11]}

Axiom of infinity.  There exists a nonempty set [math]\displaystyle{ a }[/math] such that for all [math]\displaystyle{ x }[/math] in [math]\displaystyle{ a }[/math], there exists a [math]\displaystyle{ y }[/math] in [math]\displaystyle{ a }[/math] such that [math]\displaystyle{ x }[/math] is a proper subset of [math]\displaystyle{ y }[/math]. [math]\displaystyle{ \exists a\, [\exists u(u \in a) \,\land\, \forall x(x \in a \implies \exists y(y \in a \,\land\, x \subset y))]. }[/math]

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 [math]\displaystyle{ \empty }[/math] was proved. We now prove that [math]\displaystyle{ \empty }[/math] is a set. Let function [math]\displaystyle{ F = \empty }[/math] and let [math]\displaystyle{ a }[/math] be the set given by the axiom of infinity. By replacement, the image of [math]\displaystyle{ a }[/math] under [math]\displaystyle{ F }[/math], which equals [math]\displaystyle{ \empty }[/math], is a set.

NBG's axiom of infinity is implied by ZFC's axiom of infinity: [math]\displaystyle{ \,\exists a\, [\empty \in a \,\land\, \forall x(x \in a \implies x \cup \{x\} \in a)].\, }[/math] The first conjunct of ZFC's axiom, [math]\displaystyle{ \empty \in a }[/math], implies the first conjunct of NBG's axiom. The second conjunct of ZFC's axiom, [math]\displaystyle{ \forall x(x \in a \implies x \cup \{x\} \in a) }[/math], implies the second conjunct of NBG's axiom since [math]\displaystyle{ x \subset x \cup \{x\}. }[/math] To prove ZFC's axiom of infinity from NBG's axiom of infinity requires some of the other NBG axioms (see Weak axiom of infinity).^{[lower-alpha 12]}

Axiom of global choice

The class concept allows NBG to have a stronger axiom of choice than ZFC. A choice function is a function [math]\displaystyle{ f }[/math] defined on a set [math]\displaystyle{ s }[/math] of nonempty sets such that [math]\displaystyle{ f(x) \in x }[/math] for all [math]\displaystyle{ x \in s. }[/math] 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 [math]\displaystyle{ G }[/math] defined on the class of all nonempty sets such that [math]\displaystyle{ G(x) \in x }[/math] for every nonempty set [math]\displaystyle{ x. }[/math] 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 [math]\displaystyle{ s }[/math] of nonempty sets, [math]\displaystyle{ G\vert_s }[/math] (the restriction of [math]\displaystyle{ G }[/math] to [math]\displaystyle{ s }[/math]) is a choice function for [math]\displaystyle{ s. }[/math] 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.^[38] 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.^{[lower-alpha 13]}

Axiom of global choice.  There exists a function that chooses an element from every nonempty set.

[math]\displaystyle{ \exists G\,[G \text{ is a function}\, \land \forall x(x \ne \empty \implies \exists y(y \in x \land (x,y) \in G))]. }[/math]

History

History of approaches that led to NBG set theory

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.^[39] 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 [a, x] rather than a(x) 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, x] ≠ A.^[1]

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.^{[40][lower-alpha 14]} 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".^[42]

Von Neumann worked on the problems of Zermelo set theory and provided solutions for some of them:

• A theory of ordinals
  • Problem: Cantor's theory of ordinal numbers cannot be developed in Zermelo set theory because it lacks the axiom of replacement.^{[lower-alpha 15]}
  • Solution: Von Neumann recovered Cantor's theory by defining the ordinals using sets that are well-ordered by the ∈-relation,^{[lower-alpha 16]} and by using the axiom of replacement to prove key theorems about the ordinals, such as every well-ordered set is order-isomorphic with an ordinal.^{[lower-alpha 15]} In contrast to Fraenkel and Skolem, von Neumann emphasized how important the replacement axiom is for set theory: "In fact, I believe that no theory of ordinals is possible at all without this axiom."^[45]
• A criterion identifying classes that are too large to be sets
  • Problem: 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.^{[lower-alpha 17]}
  • Solution: Von Neumann introduced the criterion: A class is too large to be a set if and only if it can be mapped onto the class V of all sets. Von Neumann realized that the set-theoretic paradoxes could 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 C is not a member of any class if and only if C can be mapped onto V.^{[48][lower-alpha 18]}
• Finite axiomatization
  • Problem: Zermelo had used the imprecise concept of "definite propositional function" in his axiom of separation.
  • Solutions: Skolem introduced the axiom schema of separation that was later used in ZFC, and Fraenkel introduced an equivalent solution.^[50] However, 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."^{[lower-alpha 19]} 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.^[51] In 1961, Richard Montague proved that ZFC cannot be finitely axiomatized.^[52]
• The axiom of regularity
  • Problem: Zermelo set theory starts with the empty set and an infinite set, and iterates the axioms of pairing, union, power set, separation, and choice to generate new sets. However, it does not restrict sets to these. For example, it allows sets that are not well-founded, such as a set x satisfying x ∈ x.^{[lower-alpha 20]}
  • Solutions: Fraenkel introduced an axiom to exclude these sets. Von Neumann analyzed Fraenkel's axiom and stated that it was not "precisely formulated", but it would approximately say: "Besides the sets ... whose existence is absolutely required by the axioms, there are no further sets."^[54] Von Neumann proposed the axiom of regularity as a way to exclude non-well-founded sets, but did not include it in his axiom system. In 1930, Zermelo became the first to publish an axiom system that included regularity.^{[lower-alpha 21]}

Von Neumann's 1929 axiom system

John von Neumann

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 [the axiom's] consistency is not even more problematic than an axiomatization of set theory that does not go beyond the necessary Cantorian framework."^[57]

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."^[58]

Let S be von Neumann's 1929 axiom system. Von Neumann introduced the axiom system S + Regularity (which consists of S and the axiom of 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 (result 1). 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 (result 2), 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

File:ETH-BIB-Bernays, Paul (1888-1977)-Portrait-Portr 00025 (cropped).tif 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.^[59] Bernays stated that:

The purpose of modifying the von Neumann system is to remain nearer to the structure of the original Zermelo system and to utilize at the same time some of the set-theoretic concepts of the Schröder logic and of Principia Mathematica which have become familiar to logicians. As will be seen, a considerable simplification results from this arrangement.^[60]

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.^[61]

Gödel's axiom system (NBG)

Kurt Gödel,     c. 1926

In 1931, Bernays sent a letter containing his set theory to Kurt Gödel.^[36] 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.^{[62][lower-alpha 22]} Gödel used his axioms in his 1940 monograph on the relative consistency of global choice and the generalized continuum hypothesis.^[63]

Several reasons have been given for Gödel choosing NBG for his monograph:^{[lower-alpha 23]}

• 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."^[5]
• 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."^{[67][lower-alpha 24]}
• 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."^[68]
• Charles Parsons provided a philosophical reason for Gödel's choice: "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]."^[69]

Gödel's achievement together with the details of his presentation led to the prominence that NBG would enjoy for the next two decades.^[70] 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.^[71] Later, ZFC became more popular than NBG. This was caused by several factors, including the extra work required to handle forcing in NBG,^[72] Cohen's 1966 presentation of forcing, which used ZF,^{[73][lower-alpha 25]} and the proof that NBG is a conservative extension of ZFC.^{[lower-alpha 26]}

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, it is a theorem of NBG that the global axiom of choice 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.^{[lower-alpha 27]}

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 (or vice versa). For a survey of known results of this nature, see Pudlák 1998.

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,^[76] 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 Potter 2004.

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(X) denote the class of first-order definable subsets of X with parameters. In symbols where "[math]\displaystyle{ (X,\in) }[/math]" denotes the model with domain [math]\displaystyle{ X }[/math] and relation [math]\displaystyle{ \in }[/math], and "[math]\displaystyle{ \models }[/math]" denotes the satisfaction relation: [math]\displaystyle{ \operatorname{Def}(X) := \Bigl\{ \{ x \mid x \in X \text{ and } (X,\in) \models \phi(x,y_1,\ldots,y_n) \}: \phi \text{ is a first-order formula and } y_{1},\ldots,y_{n} \in X \Bigr\}. }[/math]

Then:

• (V_κ, ∈) and (L_κ, ∈) are models of ZFC.^[77]
• (V_κ, V_κ+1, ∈) is a model of MK where V_κ consists of the sets of the model and V_κ+1 consists of the classes of the model.^[78] Since a model of MK is a model of NBG, this model is also a model of NBG.
• (V_κ, Def(V_κ), ∈) is a model of Mendelson's version of NBG, which replaces NBG's axiom of global choice with ZFC's axiom of choice.^[79] The axioms of ZFC are true in this model because (V_κ, ∈) is a model of ZFC. In particular, ZFC's axiom of choice holds, but NBG's global choice may fail.^{[lower-alpha 28]} NBG's class existence axioms are true in this model because the classes whose existence they assert can be defined by first-order definitions. For example, the membership axiom holds since the class [math]\displaystyle{ E }[/math] is defined by: [math]\displaystyle{ E = \{x \in V_\kappa: (V_\kappa,\in) \models \exists u \ \exists v [x = (u, v) \land u \in v]\}. }[/math]
• (L_κ, L_κ⁺, ∈), where κ⁺ is the successor cardinal of κ, is a model of NBG.^{[lower-alpha 29]} NBG's class existence axioms are true in (L_κ, L_κ⁺, ∈). For example, the membership axiom holds since the class [math]\displaystyle{ E }[/math] is defined by: [math]\displaystyle{ E = \{x \in L_\kappa: (L_\kappa,\in) \models \exists u \ \exists v [x = (u, v) \land u \in v]\}. }[/math] So E ∈ 𝒫(L_κ). In his proof that GCH is true in L, Gödel proved that 𝒫(L_κ) ⊆ L_κ⁺.^[81] Therefore, E ∈ L_κ⁺, so the membership axiom is true in (L_κ, L_κ⁺, ∈). Likewise, the other class existence axioms are true. The axiom of global choice is true because L_κ is well-ordered by the restriction of Gödel's function (which maps the class of ordinals to the constructible sets) to the ordinals less than κ. Therefore, (L_κ, L_κ⁺, ∈) is a model of NBG.

Category theory

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.^[82] On whether an ontology including classes as well as sets is adequate for category theory, see Muller 2001.

Notes

References

Bibliography

• Adámek, Jiří; Herrlich, Horst; Strecker, George E. (1990), Abstract and Concrete Categories (The Joy of Cats) (1st ed.), New York: Wiley & Sons, ISBN 978-0-471-60922-3, http://katmat.math.uni-bremen.de/acc/ .
  • Adámek, Jiří; Herrlich, Horst; Strecker, George E. (2004), Abstract and Concrete Categories (The Joy of Cats) (Dover ed.), New York: Dover Publications, ISBN 978-0-486-46934-8, http://katmat.math.uni-bremen.de/acc/ .
• Bernays, Paul (1937), "A System of Axiomatic Set Theory—Part I", The Journal of Symbolic Logic 2 (1): 65–77, doi:10.2307/2268862 .
• Bernays, Paul (1941), "A System of Axiomatic Set Theory—Part II", The Journal of Symbolic Logic 6 (1): 1–17, doi:10.2307/2267281 .
• Bernays, Paul (1991), Axiomatic Set Theory (2nd Revised ed.), Dover Publications, ISBN 978-0-486-66637-2 .
• Bourbaki, Nicolas (2004), Elements of Mathematics: Theory of Sets, Springer, ISBN 978-3-540-22525-6, https://archive.org/details/springer_10.1007-978-3-642-59309-3 .
• Chuaqui, Rolando (1981), Axiomatic Set Theory: Impredicative Theories of Classes, North-Holland, ISBN 0-444-86178-5 .
• Cohen, Paul (1963), "The Independence of the Continuum Hypothesis", Proceedings of the National Academy of Sciences of the United States of America 50 (6): 1143–1148, doi:10.1073/pnas.50.6.1143, PMID 16578557, Bibcode: 1963PNAS...50.1143C .
• Cohen, Paul (1966), Set Theory and the Continuum Hypothesis, W. A. Benjamin .
  • Cohen, Paul (2008), Set Theory and the Continuum Hypothesis, Dover Publications, ISBN 978-0-486-46921-8, https://books.google.com/books?id=Z4NCAwAAQBAJ .
• Dawson, John W. (1997), Logical dilemmas: The life and work of Kurt Gödel, Wellesley, MA: AK Peters .
• Easton, William B. (1964), Powers of Regular Cardinals, Princeton University .
• Felgner, Ulrich (1971), "Comparison of the axioms of local and universal choice", Fundamenta Mathematicae 71: 43–62, doi:10.4064/fm-71-1-43-62, http://matwbn.icm.edu.pl/ksiazki/fm/fm71/fm7113.pdf .
• Ferreirós, José (2007), Labyrinth of Thought: A History of Set Theory and Its Role in Mathematical Thought (2nd revised ed.), Basel, Switzerland: Birkhäuser, ISBN 978-3-7643-8349-7 .
• Gödel, Kurt (1940), The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory (Revised ed.), Princeton University Press, ISBN 978-0-691-07927-1 .
  • Gödel, Kurt (2008), The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory, with a foreword by Laver, Richard (Paperback ed.), Ishi Press, ISBN 978-0-923891-53-4 .
• Gödel, Kurt (1986), Collected Works, Volume 1: Publications 1929–1936, Oxford University Press, ISBN 978-0-19-514720-9 .
• Gödel, Kurt (1990), Collected Works, Volume 2: Publications 1938–1974, Oxford University Press, ISBN 978-0-19-514721-6 .
• Gödel, Kurt (2003), Collected Works, Volume 4: Correspondence A–G, Oxford University Press, ISBN 978-0-19-850073-5 .
• Gray, Robert (1991), "Computer programs and mathematical proofs", The Mathematical Intelligencer 13 (4): 45–48, doi:10.1007/BF03028342 .
• Hallett, Michael (1984), Cantorian Set Theory and Limitation of Size (Hardcover ed.), Oxford: Clarendon Press, ISBN 978-0-19-853179-1 .
  • Hallett, Michael (1986), Cantorian Set Theory and Limitation of Size (Paperback ed.), Oxford: Clarendon Press, ISBN 978-0-19-853283-5 .
• Kanamori, Akihiro (2009b), The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings, Springer, ISBN 978-3-540-88867-3 .
• Kanamori, Akihiro (2009), "Bernays and Set Theory", Bulletin of Symbolic Logic 15 (1): 43–69, doi:10.2178/bsl/1231081769, http://math.bu.edu/people/aki/17a.pdf .
• Kanamori, Akihiro (2012), "In Praise of Replacement", Bulletin of Symbolic Logic 18 (1): 46–90, doi:10.2178/bsl/1327328439, http://math.bu.edu/people/aki/20.pdf .
• Kunen, Kenneth (1980), Set Theory: An Introduction to Independence Proofs (Hardcover ed.), North-Holland, ISBN 978-0-444-86839-8 .
  • Kunen, Kenneth (2012), Set Theory: An Introduction to Independence Proofs (Paperback ed.), North-Holland, ISBN 978-0-444-56402-3 .
• Mendelson, Elliott (1997), An Introduction to Mathematical Logic (4th ed.), London: Chapman and Hall/CRC, ISBN 978-0-412-80830-2 . - Pp. 225–86 contain the classic textbook treatment of NBG, showing how it does what we expect of set theory, by grounding relations, order theory, ordinal numbers, transfinite numbers, etc.
• Mirimanoff, Dmitry (1917), "Les antinomies de Russell et de Burali-Forti et le problème fondamental de la théorie des ensembles", L'Enseignement Mathématique 19: 37–52 .
• Montague, Richard (1961), "Semantic Closure and Non-Finite Axiomatizability I", in Buss, Samuel R., Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics, Pergamon Press, pp. 45–69 .
• Mostowski, Andrzej (1950), "Some impredicative definitions in the axiomatic set theory", Fundamenta Mathematicae 37: 111–124, doi:10.4064/fm-37-1-111-124, http://matwbn.icm.edu.pl/ksiazki/fm/fm37/fm37110.pdf .
• Muller, F. A. (1 September 2001), "Sets, classes, and categories", British Journal for the Philosophy of Science 52 (3): 539–73, doi:10.1093/bjps/52.3.539, http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF .
• Müller, Gurt, ed. (1976), Sets and Classes: On the Work of Paul Bernays, Studies in Logic and the Foundations of Mathematics Volume 84, Amsterdam: North Holland, ISBN 978-0-7204-2284-9 .
• Potter, Michael (2004), Set Theory and Its Philosophy: A Critical Introduction (Hardcover ed.), Oxford University Press, ISBN 978-0-19-926973-0 .
  • Potter, Michael (2004p), Set Theory and Its Philosophy: A Critical Introduction (Paperback ed.), Oxford University Press, ISBN 978-0-19-927041-5 .
• Pudlák, Pavel (1998), "The Lengths of Proofs", in Buss, Samuel R., Handbook of Proof Theory, Elsevier, pp. 547–637, ISBN 978-0-444-89840-1, http://users.math.cas.cz/~pudlak/length.pdf .
• Smullyan, Raymond M.; Fitting, Melvin (2010), Set Theory and the Continuum Problem, Dover, ISBN 978-0-486-47484-7 .
• Solovay, Robert M. (1990), "Introductory note to 1938, 1939, 1939a and 1940", Kurt Gödel Collected Works, Volume 2: Publications 1938–1974, Oxford University Press, pp. 1–25, ISBN 978-0-19-514721-6 .
• von Neumann, John (1923), "Zur Einführung der transfiniten Zahlen", Acta Litt. Acad. Sc. Szeged X. 1: 199–208, http://bbi-math.narod.ru/newmann/newmann.html .
  • English translation: van Heijenoort, Jean (2002a), "On the introduction of transfinite numbers", From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (Fourth Printing ed.), Harvard University Press, pp. 346–354, ISBN 978-0-674-32449-7, https://books.google.com/books?id=v4tBTBlU05sC&pg=PA346 .
  • English translation: van Heijenoort, Jean (2002b), "An axiomatization of set theory", From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (Fourth Printing ed.), Harvard University Press, pp. 393–413, ISBN 978-0-674-32449-7, https://books.google.com/books?id=v4tBTBlU05sC&pg=PA393 .
• von Neumann, John (1925), "Eine Axiomatisierung der Mengenlehre", Journal für die Reine und Angewandte Mathematik 154: 219–240, http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN243919689_0154&DMDID=DMDLOG_0025 .
• von Neumann, John (1928), "Die Axiomatisierung der Mengenlehre", Mathematische Zeitschrift 27: 669–752, doi:10.1007/bf01171122, http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN266833020_0027&DMDID=DMDLOG_0042 .
• von Neumann, John (1929), "Über eine Widerspruchsfreiheitsfrage in der axiomatischen Mengenlehre", Journal für die Reine und Angewandte Mathematik 160: 227–241, http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=PPN243919689_0160&DMDID=DMDLOG_0019 .

External links

• "von Neumann-Bernays-Gödel set theory". http://planetmath.org/?op=getobj&from=objects&id={{{id}}}. 
• Szudzik, Matthew. "von Neumann-Bernays-Gödel Set Theory". http://mathworld.wolfram.com/vonNeumann-Bernays-GoedelSetTheory.html. 

0.00 (0 votes) Original source: https://en.wikipedia.org/wiki/Von Neumann–Bernays–Gödel set theory. Read more