We show that there is a constant $k$ such that Buss's intuitionistic theory $\mathsf{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 $\mathsf{NP} \subseteq \mathsf{coNSIZE}[n^k]$ is unprovable in $\mathsf{IS}^1_2$.

翻译：我们证明存在常数$k$，使得Buss的直觉主义理论$\mathsf{IS}^1_2$无法证明SAT需要规模至少为$n^k$的共非确定性电路。据我们所知，这是有界算术中关于最坏情况固定多项式规模电路下界的首个无条件不可证明性结果。作为补充，我们进一步证明$\mathsf{NP} \subseteq \mathsf{coNSIZE}[n^k]$这一上界在$\mathsf{IS}^1_2$中同样不可证明。