Comprehension axiom who helps in the opposite direction 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.
 A: 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.
A: 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:

*

*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.


*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.


*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.
