Consider NBG without choice. Denote this theory NBG'. It is fairly easy once one knows a bit of model theory to demonstrate that this theory is a conservative extension of ZF.

An outline of the traditional proof goes as follows:

Consider some sentence $\phi$ in the language of set theory, and suppose that NBG' $\vdash \phi$ (of course relativising everything to quantify over sets).

I claim that ZF $\vdash \phi$.

For consider some model $(M, \in_M)$ of ZF. We can construct the "model of classes" $(M', \in_{M'})$ as follows:

First, we define $M'$ to be the collection of all sets of the form $\{x \in M \mid M \models \psi(w_1, \ldots, w_n, x)\}$, where $\psi(w_1, \ldots, w_n, x)$ is some formula in the language of ZF and $w_1, \ldots, w_n$ are some elements of $M$.

We then define $S_1 \in_{M'} S_2$ to mean $\exists x \in S_2 (\{y \in M \mid y \in_M x\} = x)$.

It is easy to verify that $M'$ models all axioms of NBG'. Therefore, $M' \models \phi$ by the soundness theorem. We can verify from this statement that $M \models \phi$.

Since all models of ZF are models of $\phi$, we can conclude by the completeness theorem that ZF $\models \phi$.

Conversely, it can be easily shown that NBG' proves all axioms of ZF. So if ZF $\vdash \phi$, then NGB' $\vdash \phi$. $\square$

Of course, we see immediately from this statement that NBG + local choice is a conservative extension of ZFC. This is because $\phi$ is a theorem of NBG + local choice $\iff$ $choice \to \phi$ is a theorem of NBG' $\iff$ $choice \to \phi$ is a theorem of ZF $\iff$ $\phi$ is a theorem of ZFC.

Note that this proof relied on two facts: the soundness theorem for countable vocabularies, and the completeness theorem for countable vocabularies. Because both of these theorems can be formalised in second-order arithmetic, it is possible to formalise the above proof in second-order arithmetic (which is, of course, considerably weaker than ZF).

The question is: can we take the above proof and formalise it in first-order arithmetic?

It seems unlikely, since we cannot use a recursive notion of truth in first-order Peano arithmetic. I don't know how one could even formulate questions about "models" within Peano arithmetic.

If we cannot take the above proof and formalise it in first-order arithmetic, is there some other proof which is available to us? I attempted to proceed with the proof using Boolean categories as models instead of more traditional set-theoretic models, but I did not get anywhere and ran into pretty much the same issues.


1 Answer 1


$\mathsf{PA}$, and indeed much less, can prove this. Here is one way to do it (not necessarily the only one):

We can define in $\mathsf{PA}$ the notion of a "syntactic $\mathsf{ZFC}$ model;" this will be a $\Sigma^0_{17}$ (say) theory $T$ in the language of set theory + countably many new constant symbols $c_i$ ($i\in\mathbb{N}$) which is complete, contains $\mathsf{ZFC}$, and has the property that for every formula $\varphi(x)$ we have some $i$ such that $T\vdash\exists x\varphi(x)\rightarrow\varphi(c_i)$. $\mathsf{PA}$ can prove that $\mathsf{ZFC}$ is consistent iff there is a syntactic $\mathsf{ZFC}$ model, with the interesting direction amounting to your favorite basis theorem. Similarly we can define the notion of "syntactic $\mathsf{NBG}$ model," and prove the relevant result. The usual semantic relative consistency proof translates easily to a $\mathsf{PA}$-argument that if there exists a syntactic $\mathsf{ZFC}$ model then there exists a syntactic $\mathsf{NBG}$ model.

This is more-or-less a special case of the arithmetized completeness theorem, if memory serves.

EDIT: Here's another argument, which is less direct but perhaps more intuitive:

As you observe, the usual argument can be appropriately formalized in second-order arithmetic. In fact, the fragment $\mathsf{ACA_0}$ suffices for this (although some care is advisable since some seemingly-obvious statements about model theory go beyond $\mathsf{ACA_0}$, see here). But $\mathsf{ACA_0}$ is easily seen to be a conservative extension of $\mathsf{PA}$, in the strong model-theoretic sense, via basically the same argument as the one showing that $\mathsf{NBG}$ is a conservative extension of $\mathsf{PA}$! So - implicitly applying the completeness theorem - we're done.

The downside of this approach, of course, is that unlike the above argument it doesn't indicate a proof strategy inside $\mathsf{ACA_0}$ (and also doesn't help getting below $\mathsf{ACA}_0$, which the above argument does - at a glance, the above argument should work even down to the level of $\mathsf{I\Sigma_1}$). But it's still neat!

  • $\begingroup$ This is quite interesting. I was actually thinking in my mind that there was clearly an analogue to the NBG/ZFC dichotomy in the Peano arithmetic situation, but I did not know the weaker theory had a name. In this case, it’s pretty easy to take the specific proof in $ACA_0$ and translate it into a pure first-order Peano arithmetic argument, essentially taking the ZF “theorems about proper classes are metatheorems” approach. Also, there is a constructive metatheorem which allows us to take any relative consistency proof in PA and translate it into a Heyting Aritumetic proof of the same fact. $\endgroup$ Commented Mar 26, 2022 at 21:57
  • 1
    $\begingroup$ So I was hoping to use a Peano arithmetic proof of the relative consistency to get a Heyting arithmetic proof and extract from it a nice effective procedure to take an NBG proof and turn it into a ZFC proof (other than the “keep looking until you find a proof” method) and possibly find bounds on how much longer the shortest ZFC proof is than the shortest NBG proof. I guess I’ll look further into it and see what happens. $\endgroup$ Commented Mar 26, 2022 at 21:59
  • $\begingroup$ Sorry for spamming you, but I do want to point out that the proof goes something like this. First, augment both ZF + $\neg \phi$ and NBG’ + $\neg \phi$ to be Henkin theories. Then, explicitly construct an ultrafilter on the sentences of the ZF-derived Henkin theory, where a statement with Gödel number $n$ is in the ultrafilter iff its negation is not deducible from all sentences $<n$ in the filter (this works since sequences of bits can be encoded in PA). Use this to explicitly construct an ultrafilter on the Henkin theory derived from NBG’. Finally, conclude consistency of NBG’ + $\neg \phi$ $\endgroup$ Commented Mar 26, 2022 at 22:11
  • $\begingroup$ @MarkSaving OK, but that goes a bit beyond the scope of your original question. Is there a specific point you'd like me to address further in my answer? $\endgroup$ Commented May 2, 2022 at 1:31

You must log in to answer this question.

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