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

To appear in Izvestiya of the RAN Abstract We show that if strong pseudorandom generators exist then the statement "ff encodes a circuit of size n(log * n) for SATISFIABILITY " is not refutable in S22 (ff). For refutation in S12 (ff), 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.