Comprehension axiom that helps in the opposite direction

Question

Usually, having more comprehension axiom means the more you can prove. We wonder if the converse can be the case.

Is there a natural problem $\mathsf{P}$ so that $\mathsf{P}+\neg(\Gamma-\mathsf{ComprehensionAxiom})$ implies $\mathsf{Q}$, but $\mathsf{P}$ does not implies $\mathsf{Q}$.

Also I'd like to exclude some trivial case such as $\mathsf{Q}$ is $\neg(\Gamma-\mathsf{ComprehensionAxiom})$. We can accept $\mathsf{Q}$ to be some Comprehension Axiom, but not the negation of them. The implication is not necessary over $\mathsf{RCA}$ and $\Gamma$ can be any set of formulas.

Answer 1

David Belanger's work is relevant.

The principle $\mathsf{WKL_0}$ (= "Every infinite subtree of $2^{<\omega}$ has an infinite path") is not literally a comprehension principle, so its negation can be used as a choice of $\mathsf{Q}$. Belanger showed that over $\mathsf{RCA_0}$, the principle $(\star)\equiv$ "There is a complete theory with finitely many models and a single nonprincipal type" is equivalent to $\mathsf{ACA_0\vee\neg WKL_0}$. Consequently, if we take as our base theory $\mathsf{RCA_0+(\star)}$, we get $\neg\mathsf{ACA_0}\implies\mathsf{Q}$.

What if we do want to consider $\mathsf{WKL_0}$ as a kind of comprehension principle (it's one of the "Big Five" after all), so that we can't set $\mathsf{Q}=\neg\mathsf{WKL_0}$? Well, in this case another result of Belanger is relevant: that a rather complicated model-theoretic principle (see Theorem 2.23 here), which I'll refer to as $(\dagger)$ here, implies over $\mathsf{RCA_0}$ the disjunction $\mathsf{WKL_0\vee I\Sigma_2}$. Consequently, over $\mathsf{RCA_0}$ the negation of $\mathsf{WKL_0}$ (which we're now considering a comprehension principle!), plus the principle $(\dagger)$, implies $\mathsf{I\Sigma_2}$ - which is not itself a consequence of $\mathsf{RCA_0}+(\dagger)$ so this is nontrivial.

Answer 2

There are many such examples in higher-order Reverse Mathematics. I discuss a couple and indicate a relevant paper of mine related to David's. As usual, let RCA$_0^\omega$ be Kohlenbach's base theory which is conservative over RCA$_0$.

First of all, here are some examples:

1. RCA$_0^\omega$ (and much stronger systems) cannot prove the Lindeloef lemma for uncountable coverings as follows:

For any $\Psi:\mathbb{R}\rightarrow \mathbb{R}^+$, there is a sequence $x_0, x_1,x_2, \dots$ of reals such that $\cup_{n\in \mathbb{N}}B(x_n, \Psi(x_n))$ covers $\mathbb{R}$.

However, RCA$_0^\omega + \neg$ACA$_0$ can prove the previous statement.

2. RCA$_0^\omega +$ WKL (and much stronger systems) cannot prove the Heine-Borel theorem for uncountable coverings as follows:

For any $\Psi:[0,1]\rightarrow \mathbb{R}^+$, there is a finite sequence $x_0, \dots, x_k$ of reals in $[0,1]$ such that $\cup_{n\leq k}B(x_n, \Psi(x_n))$ covers $[0,1]$.

However, RCA$_0^\omega + $ WKL $+ \neg$ACA$_0$ can prove the previous statement.

3. RCA$_0^\omega +$ WKL (and much stronger systems) cannot prove the (essence of the) Vitali covering theorem for uncountable coverings as follows:

For any $\Psi:[0,1]\rightarrow \mathbb{R}^+$ and $\epsilon>0$, there is a finite sequence $x_{0}, \dots, x_k$ of reals in $[0,1]$ such that $\cup_{n\leq k}B(x_n, \Psi(x_n))$ has measure at least $1-\epsilon$.

However, RCA$_0^\omega + $ WKL $+ \neg$ACA$_0$ can prove the previous statement. (It is an interesting question whether WWKL also suffices.)

There are many many more such examples.

Secondly, since Noah mentions David Belanger's paper, I should mention my "follow-up" paper which appeared in the NDJFL (and arxiv):

Sam Sanders, Splittings and disjunctions in Reverse Mathematics, Notre Dame J. Formal Logic 61(1): 51-74 (January 2020). DOI: 10.1215/00294527-2019-0032.

One will find many examples based on the results that paper (directly or indirectly).

Thirdly, for those who wish to know more: let $(\exists^2)$ be Kleene's arithmetical quantifier, i.e.

$$ (\exists E^2)(\forall f^1)\big((\exists n^0)(f(n)=0)\leftrightarrow E(f)=0 \big). $$

It is well-known that RCA$_0^\omega + (\exists^2)$ is conservative over ACA$_0$. One generally refers to $E^2$ as in $(\exists^2)$ as a `comprehension functional', for obvious reasons.

As shown by Kohlenbach (by formalising so-called Grilliot's trick in the base theory), $(\exists^2)$ is equivalent over the base theory to

there exists an $\mathbb{R}\rightarrow \mathbb{R}$-function that is not everywhere (epsilon-delta) continuous.

Clearly, $(\exists^2)\rightarrow$ACA$_0$ and contraposition tells us that $\neg$ACA$_0$ implies Brouwer's theorem in that all functions on the reals are continuous. In this light, the above items go through.