On the Unprovability of Circuit Size Bounds in Intuitionistic S¹₂

We show that there is a constant k such that Buss's intuitionistic theory IS¹₂ does not prove that SAT requires co-nondeterministic circuits of size at least nᵏ. To our knowledge, this is the first unconditional unprovability result in bounded arithmetic in the context of worst-case fixed-polynomial size circuit lower bounds. We complement this result by showing that the upper bound NP ⊆ coNSIZE[nᵏ] is unprovable in IS¹₂.