Trading Choice for Comprehension (or Replacement)

Question

This question is basically a request for clarification about a remark made by Sam Sanders in a comment to another question: IIUC what he's saying, there are statements that can be proved either with a small amount of Choice (like, countable choice) and then in a very weak framework from the Comprehension point of view (e.g., $\mathsf{WKL}_0$), or without Choice but then with a strong amount of Comprehension, but not without Choice and with weak Comprehension.

I'd like to know more about such statements, what the intuition between this “Choice for Comprehension” tradeoff is, and how this is proved (or where I might learn more about them).

Please be liberal in understanding the question: classical reverse math, constructive¹ reverse math, set theory, anything in the direction of “trading Choice for some non-choicy set-building operation” is interesting. Are there interesting² statements that can be proved in weak subsystems of $\mathsf{ZFC}$ (like $\mathsf{KPC}$), or in full $\mathsf{ZF}$, but not in their intersection (like $\mathsf{KP}$), for example?

1. I am aware of some things that go slightly in that direction, like the equality of Cauchy and Dedekind reals can be proved in $\mathsf{IZF}$ with Countable Choice or in classical $\mathsf{ZF}$ (without any Choice). But this is a “Choice for Omniscience” tradeoff which is a bit different from what I'm asking.

2. Please don't point out that the logical disjunction between the axiom of choice and some strong comprehension/replacement axiom works, or any such obviously artificial example.

Answer 1

In second-order number theory, one typically presumes induction on the numbers for the classes of numbers that are available. And so comprehension gives you more classes, hence more induction, but induction enables choice, since you can now pick the least instance. In this sense, in the arithmetic context comprehension implies these corresponding instances of "choice".

Answer 2

Most of the examples I know can be found in [1,2] and are joint work with Dag Normann. The prettiest examples we have are perhaps the following:

Let RCA$_0^\omega$ be Kohlenbach's base theory of RM and let QF-AC$^{0,1}$ be countable choice for quantifier-free formulas (allowing any parameters); the latter is not provable in ZF (see [0] for all this). We assume that sets of reals $X\subset\mathbb{R}$ are given by their characteristic functions $\mathbb{1}_X$, well-known from measure and probability theory. A closed set is just a set that is closed, i.e. no additional representation.

On one hand, RCA$_0^\omega$+QF-AC$^{0,1}$ proves that the following are equivalent:

1. Weak Koenig's lemma as in WKL$_0$,

2. For a closed set $C\subset [0,1]$ and sequences $(a_n)_{n \in \mathbb{N}}$ and $(b_n)_{n \in \mathbb{N}}$ such that $\cup_n (a_n, b_n)$ covers $C$, there $n_0$ such that $\cup_{n\leq n_0} (a_n, b_n)$ also covers $C$.

3. A regulated function on the unit interval is bounded.

On the other hand, the system Z$_2^\omega$ cannot prove 2) and 3). Here, the system Z$_2^\omega$ is RCA$_0^\omega$ plus the existence of functionals S$_k^2$ that decide $\Pi_k^1$-formulas.

Finally, the system Z$_2^\Omega$ can prove 2) and 3). Here, the system Z$_2^\Omega$ is RCA$_0^\omega$ plus the existence of Kleene's $\exists^4$. The systems Z$_2^\Omega$, Z$_2^\omega$, and Z$_2$ all prove the same second-order sentences.

We qualify the above observations as 'statements 2) and 3) exhibit the Pincherle phenomenon' as a theorem by Pincherle was the first example of this behaviour.

Regarding intuition, the previous observations express the following: third-order objects like closed sets (without representation) and regulated functions are 'truly third-order' and cannot be handled via second-order means only. This means that basic properties of such objects can only be established via some 'truly third-order' axioms, like $\exists^4$ and countable choice as in QF-AC$^{0,1}$.

By contrast, there are third-order objects (continuous functions, Baire 1 functions, quasi-continuous functions) that can be handled using secon-order axioms (only); I call those 'second-order-ish'. In particular, all properties of such objects can be established in the system RCA$_0^\omega$ + Z$_2$. Usually, the Big Five suffice, as established in [3], leading to many new equivalences that prop up the 'Big Five' phenomenon of RM.

Finally, some esoteric speculation: the difference between 1st and 2nd order objects is rather concrete and set in stone. However, the difference between 2nd order and 3rd order objects is more blurry as there are (real) function classes that can be studied (say assuming RCA$_0^\omega$) using only second-order axioms.

References

[0] Ulrich Kohlenbach, Higher order reverse mathematics, Reverse mathematics 2001, Lect. Notes Log., vol. 21, ASL, 2005, pp. 281–295.

[1] Dag Normann and Sam Sanders, Pincherle’s theorem in reverse mathematics and computability theory, Ann. Pure Appl. Logic 171 (2020), no. 5, 102788, 41.

[2] ____, The Axiom of Choice in Computability Theory and Reverse Mathematics, Journal of Logic and Computation 31 (2021), no. 1, 297-325.

[3]_____, The Biggest Five of Reverse Mathematics, Journal for Mathematical Logic, doi: https://doi.org/10.1142/S0219061324500077 (2023), pp. 56.