Given two logical systems, $L_1$ and $L_2$, in which every formula of $L_1$ is also a formula of $L_2$, $L_2$ is said to be a conservative extension of $L_1$ iff the set of theorems of $L_1$ are precisely the set of theorems of $L_2$ that are formulas of $L_1$.

Denote by $\text{ZFC}_{\sigma}$ the ZFC set theory enriched with a $1$-place function symbol '$\sigma$', called the global selector, and extended with the following axiom, called the axiom of global choice for ZFC.

For every non-empty set $z$, $\sigma(z)$ is a member of $z$.

According to [Fraenkel] (p. 73), $\text{ZFC}_{\sigma}$ is a conservative extension of ZFC.

Denote by NBG+ the NBG set theory extended with the following axiom, called the axiom of global choice for NBG.

There exists a function $\sigma$ whose domain contains all non-empty sets, and such that for every non-empty set $z$, $\sigma(z) \in z$.

(Note that the language of NBG+ is not enriched with a symbol $\sigma$.)

According to [Fraenkel] (p. 134), NBG+ is a conservative extension of ZFC.

Denote by $\text{NBG}_{\sigma}$ the NBG set theory enriched with a $1$-place function symbol '$\sigma$', called the global selector, and extended with the following axiom.

For every non-empty set $z$, $\sigma(z)$ is a member of $z$.


  1. Is $\text{NBG}_{\sigma}$ a conservative extension of NBG+?
  2. Is $\text{NBG}_{\sigma}$ a conservative extension of NBG?
  3. Is NBG+ a conservative extension of NBG?


[Fraenkel] Fraenkel, A. A., Bar-Hillel, Y., Levy, A. Foundations of Set Theory. 2nd Revised Edition. Elsevier. 1973

  • 3
    $\begingroup$ In $ZFC_\sigma$ do you include instances of selection/ replacement that contain $\sigma$? $\endgroup$ Jun 26, 2019 at 22:00
  • 3
    $\begingroup$ @EvanAad: So one can't use the $\sigma$ symbol in the formula in selection and replacement, or can one? (It doesn't clarify much when you respond to a clarifying question by essentially repeating the same unclear description I'm asking you to clarify ...) $\endgroup$ Jun 26, 2019 at 22:25
  • 3
    $\begingroup$ (And $\varnothing$ is not a symbol in the language of ZFC, which is a clear difference from when you say that $\sigma$ is a new symbol you are adding to the language). $\endgroup$ Jun 26, 2019 at 22:32
  • 3
    $\begingroup$ One point here is that it is almost trivially obvious that this addition of $\sigma$ produces a conservative extension when you're not adding new instances of selection/replacement. You can take any model of ZFC whatsoever and make it into a model of ZFC${}_\sigma$ by defining an appropriate interpretation $\sigma$. This does not involve adding any new sets or changing the relation between the sets you already have, so every sentence in the language of ZFC retains its truth value, and there is now only your one new axiom to satisfy. And it is just the same between NBG and NBG${}_\sigma$. $\endgroup$ Jun 26, 2019 at 23:10
  • 3
    $\begingroup$ In other words, you cannot use your new $\sigma$ symbol for anything meaningful in proofs as long as you don't allow it to appear inside the set builder notation. $\endgroup$ Jun 26, 2019 at 23:11

2 Answers 2


EDIT: There's an issue with defining NBG$_\sigma$: we have to decide whether the original NBG schemes are expanded to apply to formulas involving $\sigma$ too. Otherwise conservativity of NBG$_\sigma$ over NBG is trivial: take a given model of NBG and just "slap on" an arbitrary choice operation. And NBG+ is actually stronger, in terms of $\{\in\}$-theorems, than NBG$_\sigma$.

So - although per the comments below the OP, the weaker version of NBG$_\sigma$ is actually intended - I'm going to say a bit about the stronger version.

In my experience, NBG usually already contains global choice, so NBG=NBG+; but I'll write "NBG" for NBG without global choice below, to match the OP.

Any model $M$ of NBG+ can be turned into a model $\hat{M}$ of NBG$_\sigma$: fix some global choice (class) function $f\in M$ and just name it $\sigma$. Conversely, the reduct of any model of NBG$_\sigma$ to the smaller language of NBG+ is a model of NBG+. So NBG+ and NBG$_\sigma$ prove exactly the same sentences in their common language - that is, the answer to $(1)$ is yes. Note that this implies that $(2)$ and $(3)$ have the same answer.

Let's focus on $(3)$ to ignore the additional symbol. NBG+ already contains a new axiom in the language of NBG, so unless NBG already proves that axiom, the answer will be no.

So we want to find a model of NBG without a global well-ordering. This needs a bit of set theory, but it's doable. If $M$ is a model of ZFC, then we can turn it into a model $N$ of NBG by taking as our classes the definable-with-parameters subsets of $M$. This satisfies global choice iff $M$ has a definable(-with-parameters) well-ordering. And this doesn't necessarily hold. Proving this takes serious work, unfortunately: we show that there is a model of ZFC together with the axiom $$(*)\quad\mbox{"For every $x$, there is some $y$ not in $HOD(x)$."}$$ Here "$HOD(x)$" denotes the class of sets such that they, and each element of their transitive closure, is definable using only ordinals and $x$ as parameters. (HOD stands for "hereditarily ordinal definable," and $HOD(\emptyset)$ is abbreviated "$HOD$.") It's not at all obvious that $(*)$ is consistent with ZFC, or even expressible in ZFC - however, it turns out that both these things hold. Detailed proofs can be found in Kunen's old book.

  • 2
    $\begingroup$ It is not clear to me that "the reduct of any model of NBG${}_σ$ to the smaller language of NBG+ is a model of NBG+". Note that the new symbol $\sigma$ is defined to be a function symbol at the first-order-logic level, not a constant that names a class. So a model of NBG${}_\sigma$ might not contain any object that realizes the choice function. $\endgroup$ Jun 26, 2019 at 22:56
  • 1
    $\begingroup$ @NoahSchweber: That's what I had a kind of shouting match with the OP about. (For NBG I'm more used to the finite axiomatization presented by Mendelson, where it is clear that one would need an explicit new axiom to allow $\sigma$ in comprehensions -- but that new axiom would essentially be the ordinary axiom of global choice ...). $\endgroup$ Jun 26, 2019 at 23:28
  • 1
    $\begingroup$ @EvanAad No - see Godel's completeness theorem. Being true in every model of $\Gamma$ is the same as being syntactically provable from $\Gamma$. $\endgroup$ Jun 27, 2019 at 6:07
  • 1
    $\begingroup$ @EvanAad Yes - indeed, any first-order theory with a well-orderable number of axioms (so assuming choice, any theory whatsoever). $\endgroup$ Jun 27, 2019 at 6:19
  • 1
    $\begingroup$ @Evan: What is "a standard model"? A well-founded one? The existence of well-founded models of set theory has a far greater consistency strength than just "a model". Since NGB and ZFC are equiconsistent, there's no reason to believe that NBG admits a standard model if you meta-theory is just ZFC+Con(ZFC). $\endgroup$
    – Asaf Karagila
    Jun 27, 2019 at 7:18

I will address only question 1. I will take a proof-theoretic approach. I will assume that the axiomatization of the $\text{NBG}$ set theory is the one given here (accessed July 13, 2019), and that the underlying logical framework is first order logic together with the sequent calculus (as described here and here).

Let's consider a fourth theory, which we shall call $\text{NBG}_\tau'$, where $\tau$ is an arbitrary variable of first order logic that does not occur in any axiom of $\text{NBG}$ and that is different than $\sigma$ (note that $\sigma$ is a $1$-place function symbol, whereas $\tau$ is a variable). We define $\text{NBG}_{\tau}'$ by stipulating its set of axioms to be $A \cup \{\varphi\}$, where $A$ is $\text{NBG}$'s set of axioms, and $\varphi$ is the following axiom:

$\tau$ is a function, whose domain is the class of non-empty sets, and such that, for every non-empty set $y$, $\tau(y) \in y$.

Observing that $\text{NBG}_+$'s set of axioms (up to renaming of bound variables) is $A \cup \{\exists\tau(\varphi)\}$, it can be shown on proof-theoretical grounds (see here) that a wff is provable in $\text{NBG}_{\tau}'$ iff it is provable in $\text{NBG}_+$.

Note that $\text{NBG}_{\tau}'$ is similar to $\text{NBG}_{\sigma}$ except that in the former $\tau$ is not a function symbol but rather a set constant assumed to be a function. The question arises as to whether $\text{NBG}_{\sigma}$ and $\text{NBG}_{\tau}'$ are equivalent. We will attempt to answer this question, at least partially. Denote $\text{NBG}$'s set of axioms by $A$, and denote $\text{NBG}_{\sigma}$'s extra axiom by $\xi$.

  1. Every wff that is provable in $\text{NBG}_{\tau}'$ (or, equivalently, in $\text{NBG}_+$) is provable in $\text{NBG}_{\sigma}$. Here is a proof sketch. We wish to show that, for every wff $\psi$ such that $A\cup\{\varphi\}\vdash\psi$ is provable, $A\cup\{\xi\}\vdash\psi$ is provable. By the $(\text{Cut})$ inference rule, it suffices to show that $A\cup\{\xi\}\vdash\varphi$ is provable. Assuming $A\cup\{\xi\}$, define, by the axiom schema for class formation, the relation $\tau := \{(z, \sigma z)\ : z \neq \emptyset\}$, then show that $\varphi$ holds.

  2. We want to show that, for every wff $\psi$ such $A\cup\{\xi\}\vdash \psi$ is provable, there exists some wff $\psi'$ such that the following sequents are provable:

    • $A\cup\{\xi\}\vdash (\psi\iff\psi')$,
    • $A\cup\{\varphi\}\vdash\psi'$.

    I believe this can be shown, but my attempt to do so proved trickier than I expected, so I didn't follow it through.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .