What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?

Question

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.

Answer 1

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

Answer 2

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