There have been a couple of recent questions, here and here, regarding the role of the axiom of choice in real-analytic results with applicability to general relativity. This lead me to look at some of the earlier discussion of choice on MathOverflow and Math Stack Exchange and I've gotten the impression that there isn't much general awareness of conservativity results that allow us to automatically remove appeals to choice from proofs of certain kinds of 'tangible' statements. I myself hadn't realized the fact that Shoenfield's absoluteness theorem implies that any $\Pi^1_4$ theorem of $\mathsf{ZFC}$ is already a theorem of $\mathsf{ZF}$ (partially because the Wikipedia article also seems to have not realized this) before I wrote an answer to one of the aforementioned questions. I claim in that answer that this actually covers a lot of 'ordinary mathematics.' For instance, I would suspect that the vast majority of theorems in, say, differential geometry are no worse than $\Pi^1_4$ and therefore are already provable in $\mathsf{ZF}$ despite the impression that some people have that it would be impossible to remove appeals to at least countable or dependent choice from their proofs.

Question 1. What notable theorems are projective (i.e., formalizable in second-order arithmetic) but are not known to be equivalent to a $\Pi^1_4$ statement?

As a logician myself, I'm not going to try to limit the discussion to theorems outside of logic (since this really isn't nearly as well-demarcated as some people seem to think it is), but I would be interested in seeing examples that don't feel like they involve logic directly.

I'm also interested in restrictions of more complicated theorems to countable objects (since, as is mentioned in the discussion here, set-theoretic shenanigans often arise from very general statements applied to uncountable objects).

Question 2. What projective theorems (of $\mathsf{ZFC}$) are known to be unprovable or seem likely to be unprovable in $\mathsf{ZF}$?

I think this second question gets to the spirit of questions like this in that it rules out morally arithmetic statements, such as encodings of consistency statements.

One thing I should say is that (assuming my impression isn't completely incorrect) I don't think this is actually a compelling argument to work in specifically $\mathsf{ZF}$ over and above $\mathsf{ZFC}$. The proofs you get by applying Shoenfield absoluteness (to properly $\Pi^1_4$ statements) rely on fairly technical set theory and still conceptually boil down to a lot of appeals to choice. One way of interpreting the result is that while choice may fail in a model of $\mathsf{ZF}$, there is still enough choice 'locally' to build an inner model of $\mathsf{ZFC}$ around your problem and solve it there.

  • 3
    $\begingroup$ Somewhat related: math.stackexchange.com/questions/3491349/… $\endgroup$ Sep 9 at 17:27
  • 4
    $\begingroup$ @NoahSchweber Let $\varphi(x)$ be a $\Sigma^1_3$ formula with no parameters. Suppose $\mathsf{ZFC}$ proves $\forall x \varphi(x)$. Then for any real $a$, $L[a] \models \varphi(a)$. Since $\Sigma^1_3$ formulas are upwards absolute, we have that $V \models \varphi(a)$. Since we can do this for any $a$, we have that $V \models \forall x \varphi(x)$. $\endgroup$ Sep 9 at 17:32
  • 2
    $\begingroup$ @TimothyChow Not exactly. I feel like my point is really this: The only 'constructive' theory on a lot of mathematicians' and physicists' radar is ZF. Assuming that you would be happier if results were provable in ZF alone and you aren't a set theorist, then I'd argue that the easiest course of action is to get a feel for the quantifier complexity of projective statements (which I don't think is really that hard) and liberally use absoluteness when you can. I think this is the best course because a) I think most mathematical statements that 'feel' tangible... $\endgroup$ Sep 9 at 18:38
  • 2
    $\begingroup$ ...are low enough on the projective hierarchy for absoluteness to be applicable, b) proofs using big objects are often conceptually simpler than careful proofs that stay inside the reals or at the very least having the option of resorting to a big object is useful (otherwise normal mathematicians wouldn't use things like dual spaces and Grothendieck universes), and c) working without choice or even just being careful about what choice you use can be a pain (which is why mainstream mathematicians largely gave up on trying to do it). $\endgroup$ Sep 9 at 18:38
  • 2
    $\begingroup$ @TimothyChow I do agree that learning how to spot projective quantifier complexity and learning how to code thing in second-order arithmetic are roughly equivalent, so you're right that it would be of comaprable difficulty. I just think that the convenience of having access to big objects is real and mathematicians have demonstrated that there is conceptual utility in using less tangible objects to prove things about more tangible objects. $\endgroup$ Sep 9 at 20:33

2 Answers 2


$\text{ZF}+ \text{AC}_{\omega}$ is not $\Sigma^1_4$-conservative over ZF and ZF + DC is not $\Sigma^1_4$-conservative over $\text{ZF}+ \text{AC}_{\omega}.$

An example of the former: the sentence $\omega_1 \neq \omega_{\omega}^L$ is a nontrivial $\Sigma^1_4$ consequence of countable choice. The complexity of $``\omega_1< \omega_{\omega}^L"$ is $\Sigma_3^{HC}$ (roughly, there exists $n < \omega$ and $\alpha<\omega_1$ such that for all countable $\beta > \alpha,$ there exists a ctm $M \models ZFC^- + V=L + ``|\beta|=\alpha=\omega_n"$). The complexity of $``\omega_1 > \omega_{\omega}^L"$ is $\Sigma_2^{HC}$ (there exists $\alpha<\omega_1$ such that for all ctm $M \models ZFC^- + V=L$ with $\alpha \in M,$ $M \models ``\alpha=\omega_{\omega}"$).

An example of the latter: in sections 9 and 10 of [1], the authors construct a symmetric extension of $L$ which satisfies countable choice but fails a certain instance of $\Pi^1_2$-DC. For any $\Pi^1_2$ formula $\varphi$ of two free real variables, $\varphi$-DC is the disjunction of the $\Sigma^1_4$ sentence $\psi_1$ asserting that there is a real $r_1$ such that for all reals $r_2,$ $\neg \varphi(r_1, r_2),$ and the $\Sigma^1_3$ sentence $\psi_2$ asserting that there is a sequence of reals $\langle r_i \rangle$ such that for all $n,$ $\varphi(r_i, r_{i+1}).$

[1] Friedman, Sy-David; Gitman, Victoria; Kanovei, Vladimir, A model of second-order arithmetic satisfying AC but not DC, J. Math. Log. 19, No. 1, Article ID 1850013, 39 p. (2019). ZBL1484.03067.


This is sort of an anti-answer, which I've accordingly made CW, but here goes:

Whether $\mathsf{ZFC}$ is projectively conservative over $\mathsf{ZF}$ seems open; see Joel's answer from a while ago (and to my knowledge nothing has changed). Moreover, it is known that $\mathsf{ZFC}$ is projectively conservative over $\mathsf{ZF+DC}$ (see the argument here, which I think is folklore) and $\mathsf{ZFC}$ is $\Pi^1_4$ conservative over $\mathsf{ZF}$.

To the best of my knowledge, there are no candidates for a counterexample to projective conservativity here. Personally I have no guess about whether $\mathsf{ZFC}$ is after all projectively conservative over $\mathsf{ZF}$.

  • $\begingroup$ So this would be an anti-answer to question 2 specifically, right? $\endgroup$ Sep 9 at 17:54
  • 12
    $\begingroup$ It's consistent with ZF that there is a singularization of $\omega_1$ that is $\Sigma_5$-definable over $H(\omega_1)$; this happens if one performs a symmetric collapse over $L$ making $\aleph_{\omega}$ become $\aleph_1$. ZFC proves that there is no $\Sigma_5$-definable singularization (since there is no singularization whatsoever). So ZFC is not projectively conservative over ZF, right? $\endgroup$ Sep 9 at 20:13
  • 2
    $\begingroup$ @GabeGoldberg That sounds great! I suggest you post an answer with a fuller account. $\endgroup$ Sep 9 at 21:14
  • 5
    $\begingroup$ @GabeGoldberg I'm guessing that relatedly one could give a model of ZF in which the reals are the union of a projectively definable sequence of countable sets. Is this right? $\endgroup$ Sep 9 at 21:44
  • 1
    $\begingroup$ @JoelDavidHamkins It looks like Elliot has already done a better job than I would have $\endgroup$ Sep 11 at 13:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.