On the Unprovability of Circuit Size Bounds in Intuitionistic ${\mathsf{S}}_2^1$

Lijie Chen, Jiatu Li, Igor C. Oliveira

We show that there is a constant $k$ such that Buss's intuitionistic theory ${\mathsf{IS}}_2^1$ does not prove that SAT requires co-nondeterministic circuits of size at least $n^k$.…