一句话：证明 IS^1_2 无法证明 SAT 的固定多项式 co-nondeterministic 电路下界，并给出对应上界不可证明性。
本文研究有界算术中电路复杂性下界的可证明性。作者证明存在常数 k，使得 Buss 的直觉主义有界算术 IS^1_2 不能证明 SAT 需要至少 n^k 大小的 co-nondeterministic 电路；据其所知，这是最坏情况固定多项式电路下界背景下首个有界算术中的无条件不可证明性结果。作为补充，他们还证明上界 NP ⊆ coNSIZE[n^k] 在 IS^1_2 中不可证明。为建立主结果，作者获得了关于反驳器（refuter）的新的无条件下界，特别地证明下界 NP ⊄ i.o.-coNP/poly 不存在高效反驳器，部分回答了 Atserias (2006) 提出的问题。
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$. In order to establish our main result, we obtain new unconditional lower bounds against refuters that might be of independent interest. In particular, we show that there is no efficient refuter for the lower bound $\mathsf{NP} \nsubseteq \mathsf{i.o.}\text{-}\mathsf{coNP}/\mathsf{poly}$, addressing in part a question raised by Atserias (2006).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ChenLO25,
title = {On the Unprovability of Circuit Size Bounds in Intuitionistic $\mathsf{S}^1_2$},
author = {Lijie Chen and Jiatu Li and Igor C. Oliveira},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:26)2025}
}