Von Neumann–Bernays–Gödel set theory

Encyclopedia : V : VO : VON : Von Neumann–Bernays–Gödel set theory

In foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiom system for set theory designed to yield the same results as Zermelo-Fraenkel set theory, together with the axiom of choice (ZFC), but with only a finite number of axioms, that is without axiom schemas.

First formulated by John von Neumann in the 1920s, it was, beginning in 1937, modified by Paul Bernays, and further simplified by Kurt Gödel in 1940.

Unlike ZFC, NBG has only finitely many axioms. As Richard Montague showed in 1961, it is not possible to find a finite number of axioms that is logically equivalent to ZFC; the language of NBG is thus one capable of talking about proper classes as well as sets, and a statement about sets is provable in NBG if and only if it is provable in ZFC (that is, NBG is a conservative extension of ZFC).

Contents

1 The theory
2 Axiomatization of NBG

2.1 Unpacking the axiom scheme of Class Comprehension

3 References

The theory

The defining aspect of the theory is the separation of class and set. A class can be very large — indeed, one can speak of "the class of all sets". However, there are structural limitations preventing one from speculating about "the class of all classes" or "the set of all sets".

The membership relation

[a \in s]

is only defined if [a] is a set and [s] is a set or a 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 any statement of the predicate calculus, with the membership relation. Notions of equality, pairing, subclass, and such, are thus matters of definitions and not of axioms — the definitions denote a particular abstraction of a formula.

The development of sets is carried out very similarly to ZF. There is a predicate "Rp" defined as follows:

[\mathrm(A,a) := \forall x(x \in A \iff x \in a)]

That is, a set a represents a class A if every element of a is an element of A, and vice versa. There are classes that do not have representations, such as the class of all sets that do not contain themselves. Such classes are known as proper classes.

The advantage of such a system is that it provides a scaffolding from which to speak about "large objects" without running the risk of paradox. In some developments of category theory, for instance, one denotes a large category as a category whose collection of objects and collection of morphisms can be represented by proper classes. On the other hand, a small category is a category in which the objects and morphisms "fit" in sets. Thus, we can easily speak of the "category of all small categories" without running into trouble. This would, of course, be a large category.

Axiomatization of NBG

In this section we present an axiomatization of NBG (actually, two different ones, the second a refinement of the first). Compare with the axiomatization of Morse-Kelley set theory.

We view NBG as a two-sorted theory, with small letters serving as set variables and capital letters serving as class variables. Statements of membership need to be of one of the forms [x \in y] or [x \in Y], and statements of equality may be of the form [x=y] or [X=Y]. By an abuse of notation, we write a=A for [(\forall x.x \in a \leftrightarrow x \in A)].

The theory can also be presented as a one-sorted theory, with the sets distinguished from the classes by definition: a class is a set if it is an element of another class.

The axioms now follow. We have capitalized the names of axioms concerning themselves primarily with classes.

axiom of Extensionality: [(\forall x.x \in A \leftrightarrow x \in B)\rightarrow A=B]: classes with the same elements are the same.
axiom of extensionality: [(\forall x.x \in a \leftrightarrow x \in b)\rightarrow a=b]: sets with the same elements are the same.
axiom (schema) of Class Comprehension: For any formula [\phi] containing no quantifiers over classes (it may contain class and set parameters), there is a class A such that for all x, [x \in A \leftrightarrow \phi]

If this axiom scheme is strengthened to allow all formulas (including those with quantification over classes) then it is no longer finitely axiomatizable, and the theory obtained is Morse-Kelley set theory.

axiom of pairing: For any sets x and y, there is a set [\] whose elements are exactly x and y.

Note that this axiom allows the definition of ordered pairs, and with Class Comprehension allows the implementation of relations on sets as classes (and the identification of certain class relations as functions, injections, and bijections from one class to another).

axiom of 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.

This axiom is due to von Neumann, and implements Separation, Replacement and Global Choice at a stroke. If desired, it can be weakened to "The range of any class function whose domain is included in a set is equal to a set"; this will remove the Choice (which can then be replaced with a more usual local form of Choice if desired). The full axiom of limitation of size implies the axiom of global choice because the class of ordinals is not a set, so there is a bijection from the ordinals to the universe.

axiom of union: For any set x, there is a set which contains exactly the elements of elements of x.
axiom of power set: For any set x, there is a set which contains exactly the subsets of x.
axiom of infinity: There is a set which contains the empty set as an element and contains [y \cup \] for each of its elements y.
axiom of Foundation (regularity): Each nonempty class is disjoint from one of its elements.

Unpacking the axiom scheme of Class Comprehension

An appealing feature of NBG, but one which makes its formal axiomatization a bit mysterious, is that its axiom schema of Class Comprehension is equivalent to the conjunction of a finite number of its instances. Here we develop such a finite axiomatization, but with no guarantee that it is exactly the same as one of the official axiomatizations.

We develop our axiomatization by considering the structure of formulas.

Axiom of Sets: for any set x, there is a class X such that x=X.

This axiom gives us something to start with (in combination with the axioms for set existence from the first axiomatization), and handles set parameters in formulas.

Note that if [A=\] and [B=\] then [\ = V-A] and [\ = A \cap B]. These are sufficient to handle all propositional connectives.

Axiom of Complement: For any class A, the complement [V-A = \] is a class.
Axiom of Intersection: For any classes A and B, the intersection [A \cap B = \] is a class.

Now we need to handle quantification. In order to handle multiple variables, we need to be able to represent relations. The pair [(a,b)] is defined as [\,\\}] as usual (and we note that since we assume the other axioms of NBG we have pairing).

Axiom of Products: For any classes A and B, the class [A \times B = \] is a class ([V \times A] is actually all that is needed).
Axiom of Converses: For any class R, the classes [Conv1(R) = \] and [Conv2(R) = \] exist.
Axiom of Association: For any class R, the classes [Assoc1(R) = \] and [Assoc2(R) = \] exist.

With these axioms, we can freely add dummy arguments and rearrange 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,\ldots,x_n)] as [(x_1,(x_2,\ldots,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.

Now observe that if [\] exists, then the set [\] is simply the range of the first set considered as a relation. The universal quantifier can be defined in terms of the existential quantifier and negation.

Axiom of Ranges: For any class R, the class [Rng(R) = \] exists. The previous axioms can be used to reorder arguments to bring any single argument to the front of the argument list to be quantified.

Now we need to attend to relations expressed by atomic formulas.

Axiom of Membership: The class [[in] = \] exists.
Axiom of the Diagonal: The class [[=] = \] exists.

The axiom of the diagonal along with addition of dummy arguments and rearrangement of arguments can be used to build a relation asserting the equality of any two of its arguments; this can be used to handle repeated variables.

The axioms of this section may replace the Axiom of Class Comprehension in the parent section.

References

von Neumann, J.: An Axiomatization of Set Theory, 1925, reprinted in English translation in van Heijenoort (ed.): From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Cambridge, Massachusetts, Harvard University Press 1967
Montague, R.: Semantic Closure and Non-Finite Axiomatizability I, in Infinitistic Methods, Proceedings of the Symposium on Foundations of Mathematics, (Warsaw, 2-9 September 1959). Oxford, England: Pergamon, pp. 45-69, 1961.

From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.