In this post, when I talk about bounded arithmetic theories, 
I mean the theories of arithmetic according to "Logical Foundations of Proof Complexity", which capture the complexity classes between $AC^0$ 
and $PH$, and the theories capturing $PSPACE$ and $EXPTIME$ (see Sam 
Buss's PhD thesis ([Bounded Arithmetic](http://math.ucsd.edu/~sbuss/ResearchWeb/BAthesis/Buss_Thesis_OCR.pdf), Chapter 9) or Alan Skelley's PhD thesis, [Theories and proof systems for $PSPACE$ and the $EXP\text{-}Time$ Hierarchy](http://www.cs.toronto.edu/~alan/papers/alanophd.pdf)). 


According to some belief, it ought to be easier to separate bounded arithmetic theories than complexity classes. Is there any evidence which kind of supports this belief? 



Bounded Arithmetic vs Complexity Theory
If $T\_1$ and $T\_2$ are theories corresponding to complexity classes $C\_1$ and $C\_2$ (resp.), then separation of $C\_1$ from $C\_2$ from $C\_2$ implies separation of $T\_1$ from $T\_2$, but not necessarily vice versa. (This is already mentioned in T. Chow’s answer.) In fact, with details somewhat dependent on the pair of theories, generally separation of $T\_1$ from $T\_2$ tends to be equivalent to separation of $C\_1$ from $C\_2$ in *some model* of the weaker of the two theories, as opposed to separation of $C\_1$ from $C\_2$ in the standard model $\mathbb N$. Thus, in principle, separation of the theories is a weaker statement than separation of the corresponding complexity classes.


In practice, separation of theories appears essentially as hard as separation of complexity classes.


Most of the known unconditional separation results for theories of bounded arithmetic actually go the opposite way, i.e., they are based on separations of complexity classes: the two typical cases are separations of relativized theories, such as $S^i\_2(\alpha)\ne S^{i+1}\_2(\alpha)$ (which follow from separation of complexity classes with oracles), and separations of theories corresponding to very small complexity classes, such as $V^0\ne V^0[p]$ (which follows from $\mathrm{AC}^0\ne\mathrm{AC}^0[p]$).


The exceptions are separations of various “pathologically weak” theories. Primarily, this concerns variants of $\Sigma^b\_0$ induction, about which you can read more in <https://mathoverflow.net/a/228102>, including a list of references. Some of these results also apply to “very short” $\Sigma^b\_1$ induction (such as $\Sigma^b\_1$-LLLIND); for this see [6], and the paper S. Boughattas, J.-P. Ressayre: *Bootstrapping, part I*, Annals of Pure and Applied Logic 161 (2010), no. 4, pp. 511–533. Now, what makes these unconditional separations work is precisely the fact that these theories do **not** correspond to reasonable complexity classes, so this does not provide any evidence for the thesis in the question.


