# “Hard” separation results in reverse mathematics (or similar)

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

-
This question left me confused, because of the non-example before the example, and the odd combination of examples that are easy to find but not natural. I would find it easier to think about in the following form: "here is an example of a phenomenon; does the phenomenon always occur?" –  Matt F. Jan 15 at 0:00
By the way, thanks for reading my paper! I'm actually in the process of returning the favor! I'll have to think about this a bit before weighing in... –  François G. Dorais Jan 15 at 1:09
Meanwhile, I'm a little bit puzzled about your questions Q1 and Q2.1. I feel like I know what you want but it's hard to make it precise. The issue is that Con(...) is a just a $\Pi^0_1$ statement, so in your non-example the weakest "natural" system that proves the consistency of $RT^2_2$ and $WKL$ is probably $I\Sigma^0_n$ for some $n$. Even if you mean satisfiability instead of consistency, something like $WKL_0 + I\Sigma^0_n$ still works. –  François G. Dorais Jan 15 at 1:20
@Francois: wow, thanks! (Which one?) As to your second comment, you're absolutely right - I ought to have restricted to systems of the form $RCA_0+$(some second-order comprehension); actually, I think I should rewrite this question, since on further reflection I think I'm really asking about $\omega$-models and comprehension schemes as opposed to induction schemes. I'm pressed for time at the moment, but I'll alter the question to make it more precise (and shorter/clearer) when I have the time. –  Noah S Jan 15 at 2:21
Regarding Q3, maybe SADS & SCAC work. Both are known to have $\omega$-models consisting entirely of low sets but it is also known that there is no low set that bounds the elements of an $\omega$-model of either one. Unfortunately, the recent separation of the two by Lerman, Solomon and Towsner does not (directly) give a model of SADS + ¬SCAC consisting entirely of low sets. (They get a model of ADS + ¬SCAC, which must contain a non-low set since ADS doesn't have a model consisting of low sets.) –  François G. Dorais Jan 15 at 2:21