Von Neumann–Bernays–Gödel set theory
[1] Paul Bernays reformulated von Neumann's theory by taking class and set as primitive notions.
[2] Kurt Gödel simplified Bernays' theory for his relative consistency proof of the axiom of choice and the generalized continuum hypothesis.
[non-primary source needed] Bernays used many-sorted logic with two sorts: classes and sets.
Elliott Mendelson modified Gödel's approach by having everything be a class and defining the set predicate
Bernays' two-sorted approach may appear more natural at first, but it creates a more complex theory.
[2] This redundancy is required by many-sorted logic because variables of different sorts range over disjoint subdomains of the domain of discourse.
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.
It allows us to write: The following axioms and definitions are needed for the proof of the class existence theorem.
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.
However, since the class existence theorem is stated for subscripted variables, this formula does not have the form expected by the induction hypothesis.
A recursive computer program succinctly captures the construction of a class from a given formula.
However, the proof is needed to prove that the class constructed by the program satisfies the given formula and is built using the axioms.
can be transformed into an equivalent formula satisfying the hypothesis of the class existence theorem.
, and may contain relations, special classes, and operations defined by formulas that quantify only over sets.
The axioms of pairing and regularity, which were needed for the proof of the class existence theorem, have been given above.
[l] The class concept allows NBG to have a stronger axiom of choice than ZFC.
[39] Von Neumann based his axiom system on two domains of primitive objects: functions and arguments.
Von Neumann defined classes and sets using functions and argument-functions that take only two values, A and B.
In 1929, Paul Bernays started modifying von Neumann's new axiom system by taking classes and sets as primitives.
[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.
[36] Gödel simplified Bernays' theory by making every set a class, which allowed him to use just one sort and one membership primitive.
[62][v] Gödel used his axioms in his 1940 monograph on the relative consistency of global choice and the generalized continuum hypothesis.
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.[aa] One consequence of conservative extension is that ZFC and NBG are equiconsistent.
This completely resolves von Neumann's concern about the relative consistency of this powerful axiom since ZFC is within the Cantorian framework.
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.
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.
Then: The ontology of NBG provides scaffolding for speaking about "large objects" without risking paradox.
An ontological extension that enables us to talk formally about such a "category" is the conglomerate, which is a collection of classes.
[83] On whether an ontology including classes as well as sets is adequate for category theory, see Muller 2001.
