While there has been progress in establishing the unprovability of complexity statements in lower fragments of bounded arithmetic, understanding the limits of Je\v{r}\'abek's theory $APC_1$ (2007) and of higher levels of Buss's hierarchy $S^i_2$ (1986) has been a more elusive task. Even in the more restricted setting of Cook's theory PV (1975), known results often rely on a less natural formalization that encodes a complexity statement using a collection of sentences instead of a single sentence. This is done to reduce the quantifier complexity of the resulting sentences so that standard witnessing results can be invoked. In this work, we establish unprovability results for stronger theories and for sentences of higher quantifier complexity. In particular, we unconditionally show that $APC_1$ cannot prove strong complexity lower bounds separating the third level of the polynomial hierarchy. In more detail, we consider non-uniform average-case separations, and establish that $APC_1$ cannot prove a sentence stating that $\forall n \ge n_0\;\exists\,f_n \in \Pi_{3}$-$SIZE[n^d]$ that is $(1/n)$-far from every $\Sigma_{3}$-$SIZE[2^{n^{\delta}}]$ circuit. This is a consequence of a much more general result showing that, for every $i \geq 1$, strong separations for $\Pi_{i}$-$SIZE[poly(n)]$ versus $\Sigma_{i}$-$SIZE[2^{n^{\Omega(1)}}]$ cannot be proved in the theory $T_{PV}^i$ consisting of all true $\forall \Sigma^b_{i-1}$-sentences in the language of Cook's theory PV. Our argument employs a convenient game-theoretic witnessing result that can be applied to sentences of arbitrary quantifier complexity. We combine it with extensions of a technique introduced by Kraj\'i\v{c}ek (2011) that was recently employed by Pich and Santhanam (2021) to establish the unprovability of lower bounds in PV (i.e., the case $i=1$ above, but under a weaker formalization) and in a fragment of $APC_1$.

翻译：尽管在建立有界算术低层片段中复杂性陈述的不可证明性方面已取得进展，理解耶拉贝克理论 $APC_1$（2007）和巴斯层次 $S^i_2$（1986）更高层的局限性仍是一项更具挑战性的任务。即使在库克理论 PV（1975）这一更受限的设定中，已知结果往往依赖于一种不太自然的规范化方式：通过一组语句而非单个语句来编码复杂性断言。这样做是为了降低结果语句的量词复杂度，从而可以运用标准的见证结果。本研究为更强大的理论和更高量词复杂度的语句建立了不可证明性结果。具体而言，我们无条件证明 $APC_1$ 无法证明将多项式层次第三层区分开的强复杂性下界。更详细地说，我们考虑非均匀平均情况区分，并证明 $APC_1$ 无法证明以下语句：存在 $\forall n \ge n_0\;\exists\,f_n \in \Pi_{3}$-$SIZE[n^d]$ 使得该函数与任意 $\Sigma_{3}$-$SIZE[2^{n^{\delta}}]$ 电路的差距至少为 $1/n$。这是更广泛结论的推论：对于每个 $i \geq 1$，理论 $T_{PV}^i$（由库克理论 PV 语言中所有真 $\forall \Sigma^b_{i-1}$ 语句构成）无法证明 $\Pi_{i}$-$SIZE[poly(n)]$ 与 $\Sigma_{i}$-$SIZE[2^{n^{\Omega(1)}}]$ 之间的强分离。我们的论证采用了适用于任意量词复杂度语句的便捷博弈论见证结果，并结合了克拉伊切克（2011）引入的技术扩展——该技术近期被皮赫和桑塔南（2021）用于证明 PV（即上述 $i=1$ 情形，但采用更弱规范化）及 $APC_1$ 片段中下界的不可证明性。