Talk:Von Neumann–Bernays–Gödel set theory

Rewrote History section

I expanded and rewrote the History section. One goal was to show how von Neumann's work grew out of previous work in set theory, and to indicate the innovations he was making. On Bernays' work, I mention that his working with sets and classes follows existing traditions in set theory and logic. Finally, I added a few more details on Bernays' and Gödel's work.

I also corrected an error in the old History section: Bernays did not discover that the axiom system could be finitely axiomatize—von Neumann's original system only used finitely many axioms. See my discussion in Finite axiomatization.--RJGray (talk) 21:01, 12 April 2013 (UTC)

Article contradicting itself

In the Model theory section the article says:

Def(V_κ) is an intended model of NBG;

and later:

Note that Def(V_κ) is not necessarily a model of NBG, since Limitation of Size might fail.

So is Def(V_κ) a model of NBG, or not? - Mike Rosoft (talk) 06:58, 28 August 2016 (UTC)

Separately, I have always thought that MK and NBG have the same intended models. Of course NBG is not as strong as MK, but they are both meant to describe the same thing. In the same way, the intended model of ZF is the same as the intended model of ZFC, and the intended models of ${\mathsf {ACA}}_{0}$ has the full powerset of the naturals, not just the arithmetical sets. Sources for NBG are hard to come by, but has anyone published comments on the intended models of NBG? — Carl (CBM · talk) 11:30, 28 August 2016 (UTC)

If the axiom of limitation of size and thus implicitly the axiom of global choice is included in NBG, then it is not clear to me that it is a conservative extension of ZFC. I think that the remark about Def(V_κ) is meant to be applied to the conservative version of NBG, i.e. using replacement and ordinary choice. If one extends the scope of Def to include a global choice function on V_κ - { {} } as a parameter in formulas for classes, then I think that it would yield the axiom of limitation of size. JRSpriggs (talk) 14:44, 28 August 2016 (UTC)

I'm not sure about Def(V_κ), but NBG is definitely a conservative extension of ZFC, which means that they have the same theorems about sets. Global choice, which is equivalent to the class of all sets having a well-ordering, is a statement about classes so it cannot be stated in ZFC. Since global choice cannot be stated in ZFC, it doesn't take part in whether NBG is a conservative extension of ZFC. Here's what planetmath says (in its last paragraph) about the difficulty of proving this result: "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." (NOTE: In Labyrinth of Thought by José Ferreirós, this result is credited to Kripke, Cohen, and Solovay, working independently. See page 381, footnote 2.) RJGray (talk) 20:45, 28 August 2016 (UTC)

For natural models of NBG, see Zermelo's models and the axiom of limitation of size. RJGray (talk) 22:02, 28 August 2016 (UTC)

Those are what I would think of as the intended set models - which is to say that the collection of sets is intended to be of the form V_κ for some κ and the collection of classes is intended to be the powerset of V_κ. Using only definable sets should give some model, but not one of the intended models. So I am not sure where the text of the article here gets the idea about definable sets. — Carl (CBM · talk) 23:02, 28 August 2016 (UTC)

I've looked into it a bit further. First, the MK article has the same "Model Theory" subsection minus the note saying that Limitation of Size might fail. Second, perhaps the error is that Limitation of Size does not fail in Def(V_κ). If Def(V_κ) is exactly the same as the one that Gödel constructs in his 1940 monograph, then Limitation of Size holds. In this case, you start with a natural model V_κ of NBG where κ is a strongly inaccessible cardinal. Gödel uses transfinite recursion to define a function F(α) that builds one set for each ordinal. A set is constructible if it is an F(α) for some α < κ. Gödel states: "A class A is constructible if all its elements are constructible sets and if the intersection of A with any constructible set is also a constructible set." (Quote follows 9.4 in his monograph.) If this produces the same sets and classes as Def(V_κ), then Gödel's construction implies that Limitation of Size does hold. By the way, since F(α) builds all the sets in L, F(α) is an explicitly defined one-to-one correspondence from the class of ordinals to the class of all sets. So it appears that F(α) is an example of a class in Def(V_κ). So perhaps all we need to remove is the note saying that Limitation of Size might fail. Of course, we may want to reference Gödel's monograph. --RJGray (talk) 17:31, 29 August 2016 (UTC)

Perhaps it would be more accurate to say "Def(V_κ) is a model of NBG;" and perhaps also leave "intended model" off the others, too. I don't think von Neumann and Bernays were thinking in terms of this model when they developed NBG. Also, Zermelo definitely wasn't thinking of V_κ when he started writing his 1908 axioms (he didn't define strongly inaccessible cardinals until 1930). Zermelo was thinking of the domain of all sets. As for Morse and Kelly, I think they just wanted to add more classes. So for historical accuracy, perhaps we shouldn't get into "intended models" since in set theory these models came after the axiomatization. RJGray (talk) 18:13, 29 August 2016 (UTC)

The suggestion that the axiom of limitation might fail was added by 131.220.184.100 (talk · contribs · WHOIS) on 15 February 2016‎. It is his only contribution.

I think that the intention of NBG was that classes would represent just those collections of sets which could be defined by a formula in the language of ZFC which uses parameters which are sets. That is, those formulas which might be used in constructing instances of the axiom of separation or the axiom of replacement. Just what one needs to go from ZFC plus class comprehension to the finitely axiomatized version of NBG. JRSpriggs (talk) 03:48, 30 August 2016 (UTC)

I agree with JRSpriggs and find his explanation much simpler than my digression into Gödel's work. In fact, there may be models of set theory having classes in Def(V_κ) that are not constructible. As for whether the axiom of limitation of size holds for Def(V_κ), it seems that all that is needed is a proof that uses transfinite recursion on V_α to build a 1-1 correspondence between V_κ and κ. Since such a proof only quantifies over sets in V_κ, this correspondence would be in Def(V_κ). The current proof in Zermelo's models and the axiom of limitation of size only does calculations and uses proof by contradiction at one point.

My recommendation is to remove the erroneous statement saying that Limitation of Size might fail. Perhaps it could be replaced sometime by a note saying that a one-to-one correspondence can be built between V_κ and κ, and this correspondence is in Def(V_κ). Of course, we then need to find a reference for this fact or supply a proof ourselves. As for "intended models," JRSpriggs' comment is correct. Please ignore my previous comment on "intended models." The "intended models" mentioned may not have been intended models historically, but history is not important in this case if they are what mathematicians now view as intended models. RJGray (talk) 19:49, 30 August 2016 (UTC)

To RJGray: Thanks for your understanding of the intention. However, the limitation of size is not so simple. If we had global choice, we could choose a bijection from each V_α+1-V_α to an ordinal. Then, given a proper class C, we could send each element of C of rank α to the sum of the lower ordinals plus the image of this element. Compress out the holes to get a bijection between C and Ord (actually Κ). Then map backwards from Ord to the proper class V_Κ thus giving the axiom of limitation of size in V_Κ. But this requires global choice, ordinary choice is not enough. JRSpriggs (talk) 23:27, 30 August 2016 (UTC)

To JRSpriggs: Thanks for the correction. Before I stated that all we need is a proof that uses transfinite recursion on V_α to build a 1-1 correspondence between V_κ and κ, I should have tried to build one myself. After reading your remark, I did try to build one and immediately learned that, as you said, I need global choice to choose a bijection from each V_α+1-V_α to an ordinal.

This still leaves the problem of the current contradiction. The statement "Def(V_κ) is an intended model of NBG" is false since NBG by definition includes global choice. The best we can say is that "Def(V_κ) is an intended model of NBG – global choice + local choice." What about an intended model of NBG? I see only two candidates, if we want to limit ourselves to models that don't satisfy MK, the only one I see is Gödel's 1940 construction applied to Def(V_κ), which could be denoted by L(Def(V_κ)). However, for me, this doesn't seem to be an intended model. We could also say that "V_κ+1 is an intended model of NBG and MK." Zermelo treated V_κ+1 as an intended model of NBG in 1930. Also, there's no reason to require an intended model (also known as a standard model) to only satisfy the axioms of the theory. For example, the standard model of arithmetic satisfies more than the axioms of Peano arithmetic; for example, it also satisfies the Paris–Harrington theorem. RJGray (talk) 16:02, 31 August 2016 (UTC)

To JRSpriggs: Excellent work! I like the way you described Def(V_κ) as the intended model of an existing set theory. --RJGray (talk) 15:48, 2 September 2016 (UTC)

Rewrite of NBG article

Four and a half years ago, in the last paragraph of #Two sorted theory, I wrote: "We are still left with the question of why this Wikipedia article is giving an exposition of NBG in two-sorted logic. As Carl points out, Mendelson's book, which is referenced by this article, treats NBG with a single sort. Personally, I would like to see an exposition that is closer to Gödel's and Mendelson's. I think it would be a more accurate representation of NBG and would be simpler for readers not familiar with many-sorted logic. Also, we can then remove Rp(A,a) ("set a represents class A"), which is only mentioned once in the Ontology section, and also remove the abuse of notation a=A, which means the same as Rp(A,a) and which is only used three times in the Axiomatizating NBG section."

Since a rewrite has not appeared, I decided to do one. Before I go into details, I would like to thank Jochen Burghardt for all his help on the rewrite. He read through a couple of editions of this rewrite and made many excellent suggestions (including the extension lemma used in the proof of the class existence theoem). He also pointed out some errors. His work not only led to a more accurate article, but also to a more readable, comprehensive, and visually appealing article. He also suggested and implemented the diagram on the History page that gives the history of the approaches that led to NBG. This diagram is a compact representation of the evolution of NBG.

My approach to writing the article was to not only look at Gödel's 1940 monograph and the original Wikipedia article, but also the French Wikipédia article (fr:Théorie des ensembles de von Neumann-Bernays-Gödel) and the German Wikipedia article (de:Neumann-Bernays-Gödel-Mengenlehre). Both the French and German articles use a single sort. The German article is short and follows Mendelson. The French one is much longer and references both Gödel and Mendelson. Also, it has a proof of what Mendelson calls the class existence theorem, which shows how to build classes for any given formula. The French proof is nearly complete as far as atomic formulas are concerned, but it just mentions the axioms used for the inductive part of the proof. I have given the details.

What I like best about the original Wikipedia article is that the editor(s) gave a proof of the very important class existence theorem. However, concerning the axiomatization, the article states: "The finite axiomatization presented below does not necessarily resemble exactly any NBG axiomatization in print."

I believe that it's best to follow Gödel's axiomatization and proof closely enough so that readers who get interested in the original proof will find that the proof in the Wikipedia article prepares them to read the original proof. I made three small modifications that simplify Gödel's proof for Wikipedia readers.

The first modification is a small change to one of Gödel's axioms. (I've converted Gödel's axiom to use the standard definition of n-tuples with new components on the right rather than his definition with new components on left):

$\forall A\,\exists B\,\forall x\,\forall y\,[(x,y)\in B\iff x\in A]$

In words: If $A$ is a class, there is a class $B$ whose ordered pairs have the property that their first component is a member of $A.$ Gödel's axiom only specifies the ordered pairs of $B.$ It may contain members that are not ordered pairs. So the first modification is to go back to the axiom of Bernays that Gödel modified:

$\forall A\,\exists B\,\forall u\,[u\in B\iff \exists x\,\exists y\,(u=(x,y)\land x\in A)]$

In words: If $A$ is a class, then $A\times V$ is also a class. Bernays' axiom is stronger because it specifies all the members of $B.$ It allows the proof of the class existence theorem to produce unique classes at the end of the basis and inductive steps of the class existence theorem's proof. In a footnote, I explain the difference between the proof in the rewritten article and Gödel's proof, and I point out how his approach allows him to use his weaker axiom.

Using Bernays' axiom along with a second modification—proving the theorem immediately for class variables rather than for "symbols for special classes"—reduces Gödel's four-theorem approach to his theorem M4 (he proves theorems M1, M2, M3, and M4) down to proving two theorems.

The third modification concerns bound variables. In the case of the existential quantifier, I found Gödel's inductive proof somewhat hard to explain because he introduces a non-subscripted variable in the formula for the inductive hypothesis. This formula does not have the form expected by the induction hypothesis since the class existence theorem is stated for subscripted variables. To get formulas with subscripted variables, just replace the bound variables by subscripted variables that continue the numbering of the free set variables through the nested quantifiers. Since bound variables are free for part of the induction, this guarantees that, when they are free, they are treated the same as the original free variables.

These modifications lead to a short computer program that succinctly captures what is happening for readers who know some elementary programming. Output from this program illustrates how the construction of a class mirrors the construction of the formula defining the class. I included this output because the original article states: "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." So I'm attempting to lift some of this mystery; readers can tell me whether I succeeded.

The subsections Axiom schema versus class existence theorem and Classes and sets contain material borrowed from the French article. The History section comes from the original article (I added some material here and also Jochen's diagram has been added). The ZFC, NBG, and MK section contains material from the original article's Discussion section together with material from the French article (I also added to this material). The Models subsection comes from the original article's Model theory section with a couple of additions. The Category theory section comes from the original article's Category theory section with a little rewording.

I used Gödel's definition of the formulas used in the class existence theorem—namely, those formulas that quantify only over sets. I avoid the term "predicative" for two reasons: (1) Gödel's definition is simpler and (2) the formulas are not completely predicative but only predicative for proper classes, so the reference to Wikipedia's Impredicativity article is confusing. The Wikipedia reference says: "Roughly speaking, a definition is said to be impredicative if it invokes (mentions or quantifies over) the set being defined." When a formula that quantifies only over sets is used by class comprehension to produce a class that is a set, this set is impredicatively defined because the formula quantifies over all the sets including the set being defined. NBG has to allow this since ZFC allows impredicative definition of sets. So quantifying only over sets only means that proper classes are defined predicatively. By the way, the Impredicativity article states "There is no generally accepted precise definition of what it means to be predicative or impredicative: many different authors have given different but related definitions of what the words mean."

In the Models subsection, I use the term "model" rather than "intended model." For Peano arithmetic, an intended model exists, but it's hard to justify this term for models of set theory. When Zermelo and von Neumann wrote down their axioms, they intended that their axioms would characterize the universe of sets. Of course, their axiom systems only approximately characterize the universe of sets since, for example, they don't decide the continuum hypothesis.

In 1930, Zermelo was the first to build the models $V_{\kappa }$ for $\kappa$ strongly inaccessible (see Zermelo's models and the axiom of limitation of size). He didn't consider these models as "intended models" of set theory. Instead, he used this sequence of models to explain that the paradoxes "depend solely on confusing set theory itself … with individual models representing it. What appears as an 'ultrafinite non- or super-set' in one model is, in the succeeding model, a perfectly good, valid set with both a cardinal number and an ordinal type, and is itself a foundation stone for the construction of a new domain [model]."

I hope that readers will find the rewrite informative and interesting. --RJGray (talk) 16:40, 13 December 2017 (UTC)

The first version you gave of the axiom is equivalent to $\forall A\exists B\,(\,B\cap (V\times V)\,=\,A\times V\,)$. JRSpriggs (talk) 06:32, 14 December 2017 (UTC)

Problem with axiom of pairing and ordered pairs?

In the axiom of pairing, is there an implicit assumption that x and y are distinct? Or is it that the singleton set, which is used in the definition of ordered pairs, is what we get when x=y? Also, is the singleton set necessary or we could instead use {x,{x,y}} as an alternative definition for ordered pairs? I feel that some clarifications are needed here. Cgratie (talk) 10:02, 4 October 2018 (UTC)

No, nothing is implicitly assumed. Just read the formulas literally. {x, x} = {x}.

See Ordered pair#Variants. One could use other definitions of order pair, but they are generally considered inferior for one reason or another. JRSpriggs (talk) 01:20, 5 October 2018 (UTC)

Shorter and more elegant proofs in NBG vs ZFC

Let's review the facts:

• Every axiom in ZFC is a theorem or axiom of NBG
• Every proof in ZFC is a proof in NBG
• Some theorems of ZFC have drastically shorter proofs in NBG (per Pudlak 1998)

The only way a ZFC theorem can have a longer proof in NBG vs ZFC is if you use some sort of "cumulative proof" metric that penalizes using ZFC axioms in NBG because they are theorems. But in practical mathematics nobody cares whether the result they are using is a theorem or an axiom. "Shorter" refers to the textual length of the proof and it can be quite short if a powerful theorem is used. Since every theorem of ZFC is a theorem of NBG there is no way the shortest proof in NBG can be shorter than that in ZFC.

So I think the current statement

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).

should be

Even though NBG is a conservative extension of ZFC, a theorem may have a shorter and more elegant proof in NBG than in ZFC.

Mathnerd314159 (talk) 23:10, 8 October 2022 (UTC)