理论间 p-模拟的一种刻画方案

本文提出了一种刻画方案,用于判定一个公理化理论作为重言式的证明系统何时对另一个理论进行 $p$-模拟,具体通过以下两点加以说明:(i) 若 c.e. 理论 $\mathcal{S}$ 高效解释 $\mathcal{S}{+}\phi$,则 $\mathcal{S}$ 对 $\mathcal{S}{+}\phi$ 进行 $p$-模拟(Jeřábek 在 Pudlák17 中证明了模拟关系),因为该解释将一个所有行均为定理的 $\mathcal{S}{+}\phi$-证明映射为一个 $\mathcal{S}$-证明;(ii) $\mathcal{S}$ 证明"$\mathcal{S}$ 高效解释 $\mathcal{S}{+}\phi$"当且仅当 $\mathcal{S}$ 证明"$\mathcal{S}$ 对 $\mathcal{S}{+}\phi$ 进行 $p$-模拟"(若如此,则 $\mathcal{S}$ 已能证明 $\mathcal{S}{+}\phi$ 的所有 $\Pi_1$ 定理)。为探究该框架是否有可能解决其他开放性问题,本文提出了比"不存在最优证明系统"更强的猜想,这些猜想蕴含 Feige 假设、单向函数的存在性以及电路下界。