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