Is NBG with a global selector a conservative extension of NBG with the axiom of global choice?

Question

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

---

Questions

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?

---

Bibliography

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

Answer 1

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.

Answer 2

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.