5
$\begingroup$

Let $\mathrm{NBG}^-$ be $\mathrm{NBG}$ minus the Axiom of Choice for Classes (including sets)). Further let $\mathrm{DC}$ be the Axiom of Dependent Choice for sets and $\mathrm{DC}^\omega$ be Bernays class form of the Axiom of Dependent Choice.

It has long been known that $\mathrm{NBG}^{-} + \mathrm{DC}$ is a conservative extension of $\mathrm{ZF} + \mathrm{DC}$. Is this a folk theorem or is there a reference for it? Similar question for $\mathrm{NBG}^- + \mathrm{DC}^\omega$ in place of $\mathrm{NBG}^- + \mathrm{DC}$.

Edit (5/3/22)

In his Choice Functions of Sets and Classes (in Sets and Classes, edited by G. H. Müller, North -Holland, 1976, pp. 217-255), Ulrich Felgner shows that in ${\rm NBG}^-$, DC is equivalent to $\mathrm{DC}^\omega$ (though they are not equivalent in the absence of the Axiom of Foundation). As such, the question of folk theorem vs reference reduces to a question about $\mathrm{NBG}^- + \mathrm{DC}$.

For a statement of $\mathrm{DC}^\omega$, see the comments.

$\endgroup$
7
  • $\begingroup$ What exactly do you mean by "class form of DC"? $\endgroup$
    – Asaf Karagila
    Commented May 2, 2022 at 22:54
  • $\begingroup$ Bernays gives a class form on p. 52 of his paper “A System of Axiomatic Set Theory” in "Sets and Classes" edited by G. H. Muller. I'll dig it out, write it up and post it. $\endgroup$ Commented May 2, 2022 at 23:05
  • 1
    $\begingroup$ Maybe it's the late hour, but isn't the class form just a consequence of the set form here? All we need is to show that given $a\in A$, there is a set $A'\subseteq A$ such that $a\in A'$ and $C'=C\cap(A'\times A')$ satisfies the properties for applying DC. And that's a fairly straightforward application of Replacement. $\endgroup$
    – Asaf Karagila
    Commented May 2, 2022 at 23:22
  • 1
    $\begingroup$ @Asaf Karagila. Yes, that seems correct. Still the question of the reference for sets remains. $\endgroup$ Commented May 2, 2022 at 23:25
  • 1
    $\begingroup$ Sure. As such, are you suggesting it's likely a folk theorem? $\endgroup$ Commented May 2, 2022 at 23:39

1 Answer 1

1
$\begingroup$

It appears the result is a consequence of a general result of Joseph Shoenfield (A relative consistency proof, J. Symbolic Logic 19 (1954), 21–28) which, in turn, is an improvement of results of Novack and, especially, Mostowski (as reported in Non-Standard Models for Formal Logic, J. B. Rosser and H. Wang, J. Symbolic Logic 15 (1950), 113–129).

Shoenfield Shows:

Let C be an axiom system formalized within the first order predicate calculus and let C′ be a predicative extension of C, so that for each predicate at C there is a corresponding class in C′. (i) C′ is consistent if and only if C is consistent; (ii) every theorem of C′ which can be stated in C is a theorem of C.

$\endgroup$

You must log in to answer this question.

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