On the Unprovability of Circuit Size Bounds in Intuitionistic \(S^1_2\)
Abstract: We show that there is a constant \(k\) such that Buss’s intuitionistic theory \(\mathbf{IS}^1_2\) does not prove that SAT requires co-nondeterministic circuits of size at least \(n^k\). 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 \(\mathbf{NP} \subseteq \mathbf{coNSIZE}[n^k]\) is unprovable in \(\mathbf{IS}^1_2\).