Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic

We show that if strong pseudorandom generators exist then the statement "$\alpha$ encodes a circuit of size $n^{(\log^*n)}$ for SATISFIABILITY" is not refutable in $S_2^2(\alpha)$. For refutation in $S_2^1(\alpha)$, this is proven under the weaker assumption of the existence of generators secure against the attack by small depth circuits, and for another system which is strong enough to prove exponential lower bounds for constant-depth circuits, this is shown without using any unproven hardness assumptions.
These results can be also viewed as direct corollaries of interpolation-like theorems for certain “split versions” of classical systems of Bounded Arithmetic introduced in this paper.
Bibliography: 36 titles.