Bounded Arithmetic vs Complexity Theory

Question

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, Chapter 9) or Alan Skelley's PhD thesis, Theories and proof systems for $PSPACE$ and the $EXP\text{-}Time$ Hierarchy).

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?

Answer 1

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.

Answer 2

The arithmetic theories you're talking about typically have the property that the provably total functions are precisely the functions in some familiar complexity class.

So suppose that the provably total functions in theory $T_1$ (respectively, $T_2$) are precisely the functions in complexity class $C_1$ (respectively, $C_2$). Then, if we can separate $C_1$ and $C_2$—i.e., if we can prove that $C_1\ne C_2$—it immediately follows that $T_1\ne T_2$, and so we have also separated $T_1$ and $T_2$. But the converse does not automatically follow: We could conceivably have $T_1 \ne T_2$ even if $C_1 = C_2$. In this sense, separating the theories should be "easier."

Of course, in the cases of most interest, we currently can't separate the theories either, so I don't think that there's a lot of evidence that separating the theories is that much easier in practice.