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\).

Recommended citation: Lijie Chen, Jiatu Li, Igor C. Oliveira. On the Unprovability of Circuit Size Bounds in Intuitionistic $S^1_2$. LMCS, 2025, Volume 21, Issue 3.
Download Paper | Download Bibtex