电路下界与有界理论的一致性

证明 $\mathsf{P}^\mathsf{NP}$ 中存在需要超线性规模布尔电路的问题，是复杂性理论的一大前沿。尽管对更大的复杂性类已知此类下界，现有结果仅表明相应问题在无穷多个输入长度上困难。例如，即便对 $\mathsf{MAEXP}$ 中的问题，证明几乎处处电路下界仍是开放问题。鉴于证明对所有大输入长度成立的下界这一著名困难，我们提出如下问题：能否证明一大类技术无法证明 $\mathsf{NP}$ 在无穷频繁意义下是易解的？受此及关于数学证明与计算之间相互作用的相关问题推动，我们从逻辑视角研究电路复杂性。除其他结果外，我们证明对任意参数 $k \geq 1$，理论与计算类对 $(T, \mathcal{C})$ 为 $T = \mathsf{T}^1_2$ 且 ${\mathcal C} = \mathsf{P}^\mathsf{NP}$、$T = \mathsf{S}^1_2$ 且 ${\mathcal C} = \mathsf{NP}$、$T = \mathsf{PV}$ 且 ${\mathcal C} = \mathsf{P}$ 之一时，理论 $T$ 与 ${\mathcal C} \not \subseteq \textit{i.o.}\mathrm{SIZE}(n^k)$ 是一致的。换言之，这些理论无法建立相应问题的无穷频繁电路上界。这值得关注，因为较弱的理论 $\mathsf{PV}$ 已能形式化复杂论证，例如 PCP 定理的证明。这些一致性陈述是无条件的，并改进了 [KO17] 和 [BM18] 关于与 $\mathsf{PV}$ 一致的下界的早期定理。