有界分支逻辑的证明复杂性

我们研究基本传递模态逻辑（K4、S4、GL 等）扩充以有界分支公理 $\mathbf{BB}_k$ 后的扩展 Frege（EF）系统的证明复杂性。首先，我们研究这些逻辑的 EF 系统中析取性质及更一般的扩展规则的可行性：表明相应的判定问题可归约到全 coNP 搜索问题（或等价地，在二元情形下为不相交 NP 对）；更确切地说，扩展规则的判定问题等价于经典 EF 系统插值的一个特定特例。接着，我们利用该刻画证明，在弱于 $\mathrm{PSPACE \ne NP}$ 的某些假设下，对于所有包含于 $\mathbf{S4.2GrzBB_2}$ 或 $\mathbf{GL.2BB_2}$ 的传递逻辑，EF 与替换 Frege（SF）系统间存在超多项式（或在更强假设下为指数级）分离。我们还证明了超直觉逻辑中的类似结果：刻画了 Gabbay–de Jongh 逻辑 $\mathbf T_k$ 的 EF 系统中多结论 Visser 规则的判定复杂度，并展示了对于所有包含于 $\mathbf{T_2 + KC}$ 的中间逻辑，EF 与 SF 间有条件分离。