关于直觉主义 $\mathsf{S}^1_2$ 中电路规模下界的不可证性

我们证明存在常数 $k$，使得 Buss 的直觉主义理论 $\mathsf{IS}^1_2$ 不能证明 SAT 需要至少为 $n^k$ 的 co-非决定性电路。就我们所知，这是有界算术中关于最坏情况固定多项式规模电路下界的第一项无条件不可证性结果。我们补充说明，上界 $\mathsf{NP} \subseteq \mathsf{coNSIZE}[n^k]$ 在 $\mathsf{IS}^1_2$ 中也是不可证明的。为建立我们的主要结果，我们获得了对反驳者的新的无条件下界，这些结果或许在独立兴趣方面也有价值。特别是，我们证明不存在高效反驳者可以反驳下界 $\mathsf{NP} \nsubseteq \mathsf{i.o.}\text{-}\mathsf{coNP}/\mathsf{poly}$，部分回应了 Atserias（2006）提出的问题。