How much conservative ZF+AC and ZF+DC are over ZF?

606 Views Asked by At

A logical theory $T_2$ is a (proof theoretic) conservative extension of a theory $T_1$ if the language of $T_2$ extends the language of $T_1$; every theorem of $T_1$ is a theorem of $T_2$; and any theorem of $T_2$ that is in the language of $T_1$ is already a theorem of $T_1$.

More generally, if $\Gamma$ is a set of formulas in the common language of $T_1$ and $T_2$, then $T_2$ is $\Gamma$-conservative over $T_1$ if every formula from $\Gamma$ provable in $T_2$ is also provable in $T_1$.

Question 1: How much conservative ZF+AC and ZF+DC are over ZF? In the other words, what are the largest known sets of formulas $\Gamma_1$, $\Gamma_2$ in the language of set theory such that

$\forall \varphi\in\Gamma_1~~~~~ZF+DC\vdash \varphi \Longleftrightarrow ZF\vdash \varphi$

$\forall \varphi\in\Gamma_2~~~~~ZF+AC\vdash \varphi \Longleftrightarrow ZF\vdash \varphi$

Question 2: It follows from Shoenfield's absoluteness theorem that restricted to the statements about natural numbers ZF+AC is $\Pi_{3}^1$ conservative over ZF. What can we say about $ZF+DC$ over $ZF$?

1

There are 1 best solutions below

1
On

I don't know if there is a very neat answer. In the case of $\sf ZF$ and $\sf ZFC$, you have the Levy absoluteness theorem which tells us that $\Delta_1$ statements are absolute between $V$ and $L$. I extended this in this note by introducing a new notion of "bounded quantifiers", and showing that the class of absolute statements is strictly larger than just that (it's not new, I just tried to give it some structure).

In the case of $\sf ZF+DC$ things are a bit different. We can probably push the conservativity of $\sf ZFC$ over $\sf ZF+DC$ a bit more in the same way the Levy absoluteness can be extended to $\Pi_1$ statements in that case (by using countable elementary submodels and the Shoenfield absoluteness theorem). I expect that such example can be used to give a statement which is not absolute between $\sf ZF$ and $\sf ZF+DC$ and has a relatively minimal complexity.