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

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Mathematics (Rated C-class, Mid-priority)
WikiProject Mathematics
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
C Class
Mid Priority
 Field: Foundations, logic, and set theory

Duplicate article[edit]

I accidently started a duplicate:

I was planning a full exposition of the system... should I move stuff over to here?


Yes, there should be just one article, at least at first. Later there might be a need for seperate articles. Paul August 20:10, Mar 9, 2005 (UTC)

Proposed new name: "Von Neumann-Bernays-Gödel set theory"[edit]

I think that a better name for this article would be: "Von Neumann-Bernays-Gödel set theory". I will move it there, and fix all the links unless someone objects. Paul August 16:45, Mar 11, 2005 (UTC)

This was my intent also, I will do it. MarSch 14:51, 19 Apr 2005 (UTC)

Is there any particular reason why this article, along with Zermelo–Fraenkel set theory and Shimura–Taniyama theorem, all use the "–" character in the article name, which has to be percent-escaped in the URL as "%E2%80%93", rather than a simple ASCII "-" which would not need escaping? Is this some rogue standard of the mathematical literature of which I am unaware, or perhaps just an artifact of the character set being used by the person(s) who last moved them? Finally, would it not make more sense to move them all back to the forms that are perhaps more likely to be typed directly without special character sets. Presently those three, at least, exist as redirects to the article versions with the Unicode dashes. I'd appreciate it if someone could clue me in. --KGF0 ( T | C ) 07:52, 25 October 2006 (UTC)

For some reason (which I do not understand), some people are on a campaign to replace all hyphens by ndashes. I concluded that "resistance is useless". Sorry. JRSpriggs 10:09, 25 October 2006 (UTC)
Ah, thanks. I found the rationale in WP:MOS: "it is used in compound adjectives referring to multiple people, so as to clarify that for example the name of the Poincaré–Birkhoff–Witt theorem refers to three people while the Birch–Swinnerton-Dyer conjecture refers to two (one of them called Swinnerton-Dyer)." Obnoxious to some degree, but sensible in a pedantic sort of way. --KGF0 ( T | C ) 12:25, 25 October 2006 (UTC)
Yes, I see "The hyphen (-) is used to form compound words. The en-dash (–) is used to specify numeric ranges. The em-dash (—) can be used to link clauses of a sentence. Other dashes, notably the double-hyphen (--), should be avoided.". Frankly, I think that that is nit-picking. As a work around for your problem, in some cases I can copy the text or title with cut-and-paste (control-c followed by control-v) rather than having to type in that mess. I also keep a list of frequently used links on my talk page. JRSpriggs 06:10, 26 October 2006 (UTC)
Why should you ever need to type it? There's a redirect from the hyphens version. If there's not a redirect from the version you like to type, well, add it. Redirects are almost free; as long as the target is unambiguous, and the redirect isn't tendentious in some way, no one should mind. --Trovatore 07:37, 26 October 2006 (UTC)
Also I often use the category system to navigate among articles. This only requires one to point and click rather than type in the name of the article. JRSpriggs 07:46, 27 October 2006 (UTC)


I got this message after editing:

Warning: gzuncompress(): data error in /usr/local/apache/common-local/php-1.4/includes/memcached-client.php on line 868

am reporting it. MarSch 15:53, 19 Apr 2005 (UTC)


I added axiomatization in the spirit of the article on Morse-Kelley set theory Randall Holmes 19:40, 22 December 2005 (UTC)

alternative axioms for NBGo aka vNBGU[edit]

I can't find my copy of Set Theory for the Mathematician (Jean E. Rubin), but I found Equivalents of the Axiom of Choice II (H. Rubin and J.E. Rubin)

I'll try to copy the axioms used there, but representing it as a two-sorted theory is difficult....

Primitive terms are Cl (or Class) and/or Atom and the element relation, ∈.

A1: Characterization of Atoms
D1: Definition of Set
A2 = Axiom of Extensionality
A3 = Empty Set Axiom
A4 = Class Construction Schema
A5 = Power Set Axiom
A6 = Union Axiom
A7 = Pairing Axiom
A8 = Axiom of Replacement
A9 = Axiom of Infinity
A'10 = Axiom of Foundation
If X is a non-empty class, all of whose members are sets (not urelemnts), then there is a element u of X such that

(Choice is not assumed in that book, for obvious reasons, but corresponding axioms including)

Set Choice: If x is a set of pairwise-disjoint non-empty sets, there is a choice set c such that if y ∈ x then
Class Choice 1: If X is a class of disjoint non-empty sets, there is a choice class C such that if y ∈ x then
Class Choice 1a: There is a function F on the class of all non-empty sets such that F(x) &isin x;
Class Choice 2: For any (binary) relation R there is a function F ⊆ R with the same domain.

and the strongest form

Class Trichotomy: Any two proper classes are equipollent. (Or any proper class is equipollent to V.)
or the equivalent V (the universe) is equipollent to On.

Arthur Rubin | (talk) 23:27, 24 January 2006 (UTC)

Also, Separation (If y is a Class, and y ⊆ x, and x is a set, then y is a set) follows:

Proof: if y is empty, then y is the empty set. Otherwise, let z be an element of y, and construct

"Clearly", domain(F)=x and range(F)=y. Arthur Rubin | (talk) 23:28, 24 January 2006 (UTC)

comparative axiomatization[edit]

Thanks to Arthur Rubin for posting his mother's axiom set; I wrote mine more or less off the top of my head (though it is equivalent to standard formulations!)

Here are the obvious correspondences:

  • A1 has no analogue in my set (because I assume full extensionality; I'm not allergic to atoms, though).
  • A2 is my Extensionality and extensionality as modified by the absence of atoms (of course, Rubin's theory is one-sorted, something I'm also not allergic to).
  • A3 is redundant in my set of axioms; I'm not sure if it is in Rubin's.
  • A4 is the same as my Class Comprehension.
  • A5 is the same as my power set.
  • A6 is the same as my union.
  • A7 is the same as my pairing.
  • A8 is a consequence of my Limitation of Size; a weaker form of Limitation of Size asserting that a class function with a set domain also has a set range would be equivalent to A8 (my current version says "injection", which is not appropriate in the absence of choice; I'll change that).
  • A9 is probably the same as my infinity (I haven't looked at Rubin's axiom in the book yet).
  • A10 is again probably the same as my Foundation (I need to look).

Limitation of Size also entails global choice, which is not an axiom in Rubin, but which she probably did consider (I'll look).

I have no objection to Rubin's axioms, as long as von Neumann's very powerful axiom (with its strong historical claim to connection with this theory) is discussed. Also, a full analysis of the class comprehension axiom into a finite subscheme (as I present here) is nice, and is not found in Rubin (she lists a finite subscheme but does not motivate it).

Do note that some people seem to care about having a two-sorted theory (or at least "two-sorted language" (I'm not one of them, but I wrote it with them in mind). Randall Holmes 00:59, 25 January 2006 (UTC)

Rubin's notation strikes me as somewhat old-fashioned; I would write some of it differently. Randall Holmes 00:48, 25 January 2006 (UTC)

latest modifications[edit]

I changed the weak form of Limitation of Size so that it agrees with Rubin's A8. This is better in the absence of Choice than the form I gave originally. Randall Holmes 00:56, 25 January 2006 (UTC)

I do have a copy...[edit]

I do have a copy of Rubin, Set Theory for the Mathematician, at my fingertips. Do you want anything in particular? Randall Holmes 07:13, 25 January 2006 (UTC)

I finally found it. It's behind a picture of my mother (!) Arthur Rubin | (talk) 14:54, 25 January 2006 (UTC)

comment in edit summary is wrong[edit]

the fix I just made to the weaker form of Limitation of Size is not needed; Infinity by itself implies that the empty set is a set (since it is an element of the provided set). Randall Holmes 17:02, 25 January 2006 (UTC)

Sci.math and edits[edit]

There's a thread on this article on sci.math/sci.logic which complains about it; that seems to have led to an edit and reversion. Maybe it would help if people explained their reasons here. Gene Ward Smith 22:50, 7 May 2006 (UTC)

NBG or NGB?[edit]

I think, among mathematicians this theory is called "NGB" rather than "NBG". But it is not quite important, I admit. 21:14, 16 August 2007 (UTC)

My late mother used vNBG or NBG. Do you have a particular mathematician in mind? — Arthur Rubin | (talk) 23:30, 16 August 2007 (UTC)

Oh no. It was a fatal error, sorry. I looked after it and rather NBG, really. Consider it as I haven't said anything. 15:15, 17 August 2007 (UTC)

No problem. I've done worse. — Arthur Rubin | (talk) 15:46, 17 August 2007 (UTC)

Axiom of the diagonal?[edit]

I am not sure that the axiom of the diagonal is strictly necessary, it follows from the other axioms. This is because:

Then we can break down the formula on the right into a ppf (we can replace = using extensionality and the truth table for equivalence, "for all" by "not exists not", and implies by also using its own truth table). We can then prove that this class exists by using the axioms of ranges, intersection, complement and membership. Kidburla2002 20:40, 9 September 2007 (UTC)

I think you need to go into more detail to break that out, but it doesn't really matter. We're not looking for a minimal axiomitization here. — Arthur Rubin | (talk) 23:05, 9 September 2007 (UTC)

conservative extension?[edit]

  • NBG (as written) is a conservative extension of ZFC (at least I think it is think; strong global choice, which follows from "limitation of size", may have a consequences of a choice schema which don't follow from set-choice.)
  • NBG (+ separation (which follows from "empty set" and replacement) - "limitation of size") is a conservative extension of ZF.
  • NBGU (modified to include urelements, as possibly a 3-typed theory) may be a conservative extension of ZFU+AC
  • NBGU (with the appropriate separation modifications ) may be a conservative extension of ZFU.

If we can find sources for the above statements, perhaps they should all be in the article? — Arthur Rubin | (talk) 18:43, 12 October 2007 (UTC)

reverse assoc2?[edit]

Isn't the reverse of assoc2 required, rather than the version given in the article, in order to return the argument list to standard form? Example: (1,(2,(3,(4,(5,(6,7)))))) A1-> ((1,2),(3,(4,(5,(6,7))))) A1-> (((1,2),3),(4,(5,(6,7)))) C2-> (4,( ((1,2),3) , (5,(6,7)) )). Now, using A2, we get: A2-> (4,( ( ((1,2),3) , 5 ),(6,7)) A2-> (4,(((((1,2),3),5),6),7) whereas using reverse A2, or A2*, we get: A2*-> (4,( (1,2) , (3,(5,(6,7))) )) A2*-> (4,(1,(2,(3,(5,(6,7)))))). (talk) 22:39, 28 January 2008 (UTC)

Receiving no comment, I edited said axiom, and my edit was undone. Any explanation? (talk) 20:25, 23 February 2008 (UTC)
I did not want to take the time to examine your question until you made an issue of it by actually editing the article. After reading and understanding the explanatory paragraph after axiom Assoc2, I realized that the original version was correct and your "correction" was wrong. So I changed it back. Your example above has A2 and A2* reversed as far as what their effects are. Assoc2 has to move the middle term back from being associated with the term on the left to being associated (as it originally was) with the term on the right, and that is what it does. JRSpriggs (talk) 07:37, 24 February 2008 (UTC)
I re-checked, and you are correct. My bad. (talk) 19:56, 24 February 2008 (UTC)

Two sorted theory[edit]

Does anyone know why NBG is axiomatized as a two-sorted theory here? I have only ever seen it axiomatize as a one-sorted theory (classes). Certainly Mendelson does it that way. Who axiomatizes NBG in the way done here? That's a genuine question, I'm not used to it. — Carl (CBM · talk) 10:50, 21 April 2011 (UTC)

Carl, in Gödel's article about the relative consistency of AC and GCH he also presents the theory as a two-sorted one. Perhaps this is the reason for doing so here? Godelian (talk) 20:24, 20 August 2011 (UTC)

As part of my history rewrite, I ran into material about sorts and NBG. I found that Bernays discusses his system as a two-sorted system, and then discusses how Gödel and others turned it into a one-sorted system (Bernays, Axiomatic Set Theory, p. 41):

"The two kinds of individuals [sets and classes], as well known, can on principle be reduced to only one kind, so that we come back to a one-sorted system. Here in particular this can be done in a special simple way, namely by taking as sets, those classes which satisfy the condition to be an element of a class. This method was applied by Tarski, Mostowski and Gödel; it occurs also in Quine's mathematical logic."

Also, Kanamori's article Bernays and Set Theory (PDF)  on page 6 mentions that Bernays uses two sorts. On page 14, while discussing the differences between Gödel's and Bernays' systems, Kanamori states: "The most conspicuous change is that Gödel has one sort, class, and one membership relation and introduces a predicate for set-hood."

Another way to see that Gödel's system is one-sorted is to note that one feature of a many-sorted theory is that the sorts are disjoint. This is made clear in the section Many-sorted logic in the article First-order logic. It gives an example of turning a two-sorted logic into a single-sorted logic:

"For example, if there are two sorts, one adds predicate symbols and and the axiom
Then the elements satisfying are thought of as elements of the first sort, and elements satisfying as elements of the second sort. One can quantify over each sort by using the corresponding predicate symbol to limit the range of quantification. For example, to say there is an element of the first sort satisfying formula φ(x), one writes

Since all of Gödel's sets are classes, his sets and classes are not disjoint, so they cannot be sorts. However, Gödel does use uppercase letters for classes and lowercase letters for sets, so it's easy to get the impression that his logic is two-sorted. Mendelson clarifies this in his book on page 161 ("M(X)" means "X is a set"):

"Let us introduce small letters x1, x2, … as special restricted variables for sets. In other words, (x1)(A(x1) stands for (X)(M(X) ⊃ A(X)), i.e., A holds for all sets; (Ex1)(A(x1) stands for (EX)(M(X) ∧ A(X)), i.e., A holds for some set."

I don't know why Gödel doesn't mention this method of restricting variables. In his monograph, he made "the convention" that the range of uppercase variables consists of all classes, and the range of lowercase variables consists of all sets (p. 3). Since he was writing a research monograph and since the section on "Many-sorted logic" indicates this is the standard way to restrict variables, perhaps he expected his readers to understand this.

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.--RJGray (talk) 21:07, 12 April 2013 (UTC)

Finite axiomatization[edit]

The article gives Gödel the credits for finite axiomatization, but it was actually Bernays who discovered it, according to Jesús Mosterín (2nd) edition of "Kurt Gödel - Obras completas". Please verify and correct since this seems to be an important mistake! Godelian (talk) 20:14, 20 August 2011 (UTC)

I have checked another source and confirmed that indeed it is Bernays who is responsible for finite axiomatization (see "Axiomatic set theory" by P. Bernays, with a historical introduction written by Fraenkel). This is explained in the historical notes (pp. 31). I have thus changed the corresponding paragraph in the article accordingly. Godelian (talk) 23:34, 20 August 2011 (UTC)

I'd like to thank Godelian for mentioning Fraenkel's historical introduction in Bernays' book. It was helpful for my rewrite of the history section, and I reference it in one of my notes.

Concerning axiom schemas: In his historical introduction, Fraenkel analyzes the weaknesses of Z (Zermelo set theory) on p. 31-32. On p. 32, he talks about getting rid of axiom schemas and gives credit to von Neumann for doing this:

"A further weakness of Z is that the Axiom of Subsets (No. 3) constitutes not a proper axiom but an axiom schema (p. 12/13), and the same applies to the Axiom of Substitution (No. 5). It would be preferable to get rid of axiom schemata, …"

His next paragraph states:

"All these tasks [one of which is 'to get rid of axiom schemata'] are accomplished in von Neumann's foundations of set theory ([1925, 1928, 1929], …"

I've checked von Neumann's axiom system, which appears in Jean van Heijenoort, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, p. 399-401. Von Neumann has 19 axioms and no axiom schemas (by the way, Bernays has 20 axioms and Gödel has 18). Von Neumann gives his functional equivalent to NBG's axiom schema of Class Comprehension on the top of page 400, and sketches how to derive it from his axioms.

I also noticed that von Neumann defines xa as [a, x] ≠ A, which is written in standard function notation as: a(x) ≠ A. What does "≠ A" mean? A is an argument that von Neumann uses in his axioms and "≠ A" gives him a functional way of saying xa. Using this definition, I was able to derive the 8 class existence axioms in Gödel's 1940 monograph (p. 5) from von Neumann's axioms.

Finally, I checked José Ferreirós' Labyrinth of Thought: A History of Set Theory and Its Role in Mathematical Thought. He says:

"… NBG proceeds with finitely many axioms because classes play the role of 'definite properties' or first-order conditions in ZFC, and there are finitely many axioms for 'construction' of classes. Once again, this feature was already visible in von Neumann's original presentation, but it became clearer with Bernays and Gödel."

I find the end of this quote interesting because it could explain why some people may think finite axiomatization originated in Bernays' work. It took me several tries to get into von Neumann's work—his functional viewpoint definitely makes his work harder to understand than Bernays' work. However, he does deserve the credit for the finite axiomatization of set theory, so I made this correction in my rewrite of the History section.--RJGray (talk) 21:06, 12 April 2013 (UTC)

Rewrote History section[edit]

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[edit]

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