*This is a fairly broad question. In particular, I specify 5 questions (Q1, Q2.1, Q2.2, Q3, Q4) which for me all fall under one umbrella. Since this is unreasonably broad, I'm really interested in an answer to any of them; I mention all of them largely to wave around what I think is an interesting umbrella.*

EDIT: I've replaced every instance of the predicate "$Con$" (consistency) with "$Sat$" (satisfiability); these are of course not equivalent over $RCA_0$, even though they are classically equivalent.

Reverse mathematics studies the relative strength of theorems (in the language of second-order arithmetic) over the base theory $RCA_0$ which roughly corresponds to "computable" mathematics. A *separation* in reverse mathematics is a result of the form $$ RCA_0+A\not\models B, $$ where usually $ RCA_0+B\models A$; or equivalently $$Sat(RCA_0+A+\neg B).$$ In light of this latter form, it's easy to find true statements $A$ and $B$ such that $RCA_0+B\models A$ but $Sat(RCA_0+A+\neg B)$ cannot be proven from $RCA_0+Sat(RCA_0 + B)$; that is, the separation result is much harder to prove than the two statements being separated. This is what I mean by a "hard" separation.

However, I know of no natural examples of this phenomenon. So my first question is:

(Q1) Are there natural theorems $A, B$ such that $Sat(RCA_0+A+\neg B)$ is not known to be provable in the weakest natural (from the point of view of reverse mathematics) axiom system which proves $A+B+Sat(RCA_0+B)$?

A non-example: the result $WKL_0\not\models RT^2_2$ *can* be proved in $ACA_0$, which is the weakest natural system above $WKL_0$ which proves the satisfiability of both $WKL_0$ and $RT^2_2$.

The only candidate for a positive answer to (Q1) that I know of is the result (due to Francois Dorais and Jared Corduan; see http://arxiv.org/abs/1111.1367 and http://dorais.org/archives/827) separating Weak Ramsey's Theorem and Hyper-Weak Ramsey's Theorem for pairs. The result uses a technique, "envelope forcing," which seems technically complicated enough to require a strong system; however, although I have only glanced at this paper, it seems probable that the proof does in fact go through (perhaps modified) in $ACA_0$ and that $ACA_0$ is the weakest natural system proving Weak Ramsey's Theorem for Pairs and the satisfiability of Weak Ramsey's Theorem for Pairs. (Maybe Francois will weigh in on this?)

A similar question exists for $\omega$-models:

(Q2.1) Are there natural theorems $A, B$ such that "$RCA_0+A+\neg B$ has an $\omega$-model" is not known to be provable in the weakest natural (from the point of view of reverse mathematics) axiom system which proves $A+B+Sat(RCA_0+B)$?

And a slightly stronger version:

(Q2.2) Are there natural theorems $A, B$ such that "$RCA_0+A+\neg B$ has an $\omega$-model" is not known to be satisfied in every $\omega$-model of the weakest natural axiom system which proves $A+B$?

In natural cases, I suspect these are not really different from (Q1), but one never knows.

We can also switch all the way from proofs to "nice" models. From a computability-theoretic perspective, the fact corresponding to the non-example of $WKL_0$ and $RT^2_2$ is that there is an $\omega$-model of $WKL_0+\neg RT^2_2$ consisting of $\Delta_2^0$ sets. The "relativized" version of this observation is that for any set $X\subseteq\omega$, there is an $\omega$-model of $WKL_0+\neg RT^2_2$ containing $X$ and consisting of sets which are all $\Delta^0_2$ in $X$; that is, bounded in any $\omega$-model of $ACA_0$ containing $X$. (Note that this does *not* automatically imply that every $\omega$-model of $ACA_0$ satisfies "$WKL_0+\neg RT^2_2$ has an $\omega$-model, although this is true; the obstacle is that in principle these bounded models could be very complicated to describe.) From this perspective, it is natural to ask:

(Q3) Are there natural theorems $A, B$, and a natural theory $T$ such that it is not known to be the case that for every $X\subseteq\omega$ and every $\omega$-model $\mathcal{M}$ of $T$ containing $X$, there is a set $Y\in \mathcal{M}$ and an $\omega$-model $\mathcal{N}$ of $A+\neg B$ with each set in $\mathcal{N}$ Turing below $Y$?

Personally, I think it is this question which is most compelling, but I am biased.

Finally, note that there's nothing special about $RCA_0$ here; the same sorts of questions can be asked over any base theory. Some natural base theories (at least for me) include:

$ZFC$ (or $ZF$), or $ZFC$ ($ZF$) without Replacement, or without Powerset, etc.;

$KP$ or $KPU$, the theories of admissible sets;

Any of the theories in Buss' constellation of bounded arithmetic (e.g., $S_2^2$);

Alternative set theories, such as $NF$.

So:

(Q4) Are there natural separation results over one of these (or some other) base theory which are not known to be provable just using the base theory and the consistency and truth of both statements involved? (And similarly for the analogues of Q2.1, Q2.2, and Q3.)