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.

8more comments