18

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.

James Hanson
  • 10,311
  • 3
    Somewhat related: https://math.stackexchange.com/questions/3491349/projective-conservativity-of-choice – Noah Schweber Sep 09 '23 at 17:27
  • I'm actually slightly confused; how do you get full $\Pi^1_4$ absoluteness between $\mathsf{ZFC}$ and $\mathsf{ZF}$? The best I can see is $\Pi^1_3$ (or does "explicitly given $\Pi^1_4$" mean something subtle?). – Noah Schweber Sep 09 '23 at 17:29
  • 4
    @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)$. – James Hanson Sep 09 '23 at 17:32
  • Ah, yes. Silly moment. Meanwhile, if $\mathsf{ZFC}$ proves a $\Sigma^1_4$ sentence $\exists r\varphi$ (with $\varphi$ being $\Pi^1_3$), we do get in each $L[a]$ a real $b$ which $L[a]$ thinks satisfies $\varphi$, but we can't a priori lift any of those up to $V$ since $\varphi$ is too complicated. I think I was getting my directions of absoluteness confused. – Noah Schweber Sep 09 '23 at 17:39
  • 1
    So one is using slightly less than ZFC provability of the $\Pi^1_4$ assertion $\forall x\varphi(x)$, since it suffices that $\varphi(a)$ holds in every $L[a]$. – Joel David Hamkins Sep 09 '23 at 17:49
  • 1
    @JamesHanson Can we rephrase your philosophical point as follows? Some who is worried about AC and who really only cares about "tangible" statements would be well-advised to use second-order arithmetic (rather than set theory) as a foundation. Doing so would eliminate all concerns about AC from the get-go; there would be no need to spend half of one's life tediously checking whether this or that result uses AC. – Timothy Chow Sep 09 '23 at 18:22
  • 2
    @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... – James Hanson Sep 09 '23 at 18:38
  • 2
    ...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). – James Hanson Sep 09 '23 at 18:38
  • 1
    @JamesHanson I see. It doesn't strike me as easier to train oneself to determine quantifier complexity than to learn something about reverse mathematics and subsystems of second-order arithmetic, and the latter has the advantage that you can tap into an entire community of people who are dedicated to answering questions of this type. But I suppose it could seem easier to some people. – Timothy Chow Sep 09 '23 at 19:41
  • 2
    @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. – James Hanson Sep 09 '23 at 20:33
  • @TimothyChow Incidentally, do you know of any example regarding question 1 that have been studied in the context of reverse math? – James Hanson Sep 09 '23 at 20:37
  • @JamesHanson Unfortunately, I don't know of any examples. – Timothy Chow Sep 10 '23 at 02:47
  • 1
    https://arxiv.org/abs/2204.00247 and https://arxiv.org/abs/1402.3048 seem related. – Asaf Karagila Sep 12 '23 at 20:05

2 Answers2

22

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

Elliot Glazer
  • 4,017
11

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

Noah Schweber
  • 18,932
  • So this would be an anti-answer to question 2 specifically, right? – James Hanson Sep 09 '23 at 17:54
  • @JamesHanson Yes, it's a partial anti-answer. – Noah Schweber Sep 09 '23 at 17:54
  • Maybe another partial anti-answer would go something like this: If we allow ourselves to assume projective determinacy (PD), then (I believe) there are no known "natural" unprovable statements in second-order arithmetic. This would seem to narrow the space of possible candidates considerably. – Timothy Chow Sep 09 '23 at 18:09
  • See also here https://mathoverflow.net/a/8392/1946 for the projective conservativity of ZFC over ZF+DC. – Joel David Hamkins Sep 09 '23 at 18:31
  • 12
    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? – Gabe Goldberg Sep 09 '23 at 20:13
  • 2
    @GabeGoldberg That sounds great! I suggest you post an answer with a fuller account. – Joel David Hamkins Sep 09 '23 at 21:14
  • 5
    @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? – James Hanson Sep 09 '23 at 21:44
  • 1
    @JoelDavidHamkins It looks like Elliot has already done a better job than I would have – Gabe Goldberg Sep 11 '23 at 13:15