You are here
Homevon NeumannBernaysG\"odel set theory
Primary tabs
von NeumannBernaysGödel set theory
von NeumannBernaysGödel (commonly referred to as NBG or vNBG) set theory is an axiomatisation of set theory closely related to the more familiar ZermeloFraenkel with choice (ZFC) axiomatisation. The primary difference between ZFC and NBG is that NBG has proper classes among its objects. NBG and ZFC are very closely related and are in fact equiconsistent, NBG being a conservative extension of ZFC.
In NBG, the proper classes are differentiated from sets by the fact that they do not belong to other classes. Thus in NBG we have
$\mathbf{Set}(x)\leftrightarrow\exists y(x\in y)$ 
Another interesting fact about proper classes within NBG is the following limitation of size principle of von Neumann:
$\neg\mathbf{Set}(x)\leftrightarrowx=V$ 
where $V$ is the set theoretic universe. This principle can in fact replace in NBG essentially all set existence axioms with the exception of the powerset axiom (and obviously the axiom of infinity). Thus the classes that are proper in NBG are in a very clear sense big, while the sets are small.
The NBG set theory can be axiomatised in two different ways

Using a class comprehension axiom scheme, resulting in an infinite axiomatisation
In the latter alternative we take ZFC and relativise all of its axioms to sets, i.e. we replace every expression of form $\forall x\phi$ with $\forall x(Set(x)\rightarrow\phi)$ and $\exists x\phi$ with $\exists x(Set(x)\wedge\phi)$ and add the class comprehension scheme
If $\phi$ is a formula with a free variable $x$ with all its quantifiers restricted to sets, then the following is an axiom: $\exists A\forall x(x\in A\leftrightarrow\phi)$
Notice the important restriction to formulae with quantifiers restricted to sets in the scheme. This requirement makes the NBG proper classes predicative; you can’t prove the existence of a class the definition of which quantifies over all classes. This restriction is essential; if we loosen it we get a theory that is not conservative over ZFC. If we allow arbitrary formulae in the class comprehension axiom scheme we get what is called MorseKelley set theory. This theory is essentially stronger than ZFC or NBG, as it can prove their consistency (in addition to everything they already prove). In addition to these axioms, NBG also contains the global axiom of choice: there is a function which picks an element from each nonempty set. The global axiom of choice follows from the limitation of size principle. This is because we can prove, e.g. by means of the BuraliForti paradox, that the class of all ordinals is not a set, and hence there is a bijection between the class of ordinals and the class of all sets. We can use this bijection to pick an element from each nonempty set simply by picking the element with the least ordinal assigned to it by the bijection.
Another way to axiomatise NBG is to use the eight Gödel class construction functions. These functions correspond to the various ways in which one can build up formulae (restricted to sets!) with set parameters. The functions are finite in number and so are the resulting axioms governing their behaviour. In particular, since there is a class corresponding to any restricted formula, the intersection of any set and this class exists too (and is a set). Thus the comprehension scheme of ZFC can be replaced with a finite number of axioms, provided we allow for proper classes.
The device for turning NBG into a finitely axiomatised theory can be used for other theories too. For example, the theory $ACA_{0}$ which is a formalisation of $PA$ using set variables and the so called arithmetical comprehension scheme can be finitely axiomatised using this device.
It is easy to show that everything provable in ZF is also provable in NBG. It is also not too difficult to show that NBG without global choice is a conservative extension of ZFC. However, showing that NBG (including global choice) is a conservative extension of ZFC is considerably more difficult. This is equivalent to showing that NBG with global choice is conservative over NBG with only local choice. In order to do this one needs to use (class) forcing. This result is usually credited to Easton and Solovay.
Mathematics Subject Classification
03E30 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
Recent Activity
new question: Prove that for any sets A, B, and C, An(BUC)=(AnB)U(AnC) by St_Louis
Apr 20
new image: informationtheoreticdistributedmeasurementdds.png by rspuzio
new image: informationtheoreticdistributedmeasurement4.2 by rspuzio
new image: informationtheoreticdistributedmeasurement4.1 by rspuzio
new image: informationtheoreticdistributedmeasurement3.2 by rspuzio
new image: informationtheoreticdistributedmeasurement3.1 by rspuzio
new image: informationtheoreticdistributedmeasurement2.1 by rspuzio
Apr 19
new collection: On the InformationTheoretic Structure of Distributed Measurements by rspuzio
Apr 15
new question: Prove a formula is part of the Gentzen System by LadyAnne
Mar 30
new question: A problem about Euler's totient function by mbhatia
Corrections
umlaut by bbukh ✓
Not fixed by bbukh ✓
Axiom of Global Choice incorrectly formulated? by davidsikter ✓
commas by CWoo ✓
Comments
Related topics
Igor mentions in his notational corrections suggestion that there are a number of things mentioned in this entry that merit entries of their own. I'd like to hear suggestions as to what these should be.
The following mentioned I think should have entries of their own
 conservative extension
 principle of limitation of size
 GÃ¶del (or, actually, von Neumann) class construction functions
 the theorem that these are equivalent to the predicative
comprehension scheme
 predicative vs. impredicative
 MorseKelley set theory
 class forcing
I'll see if these are not covered elsewhere in the encyclopaedia, and if not start writing them.