命题证明系统的最优性

p-最优系统像一种通用证明字节码：任何合理、可高效核验的证明语言都能编译进来，编译时间和体积膨胀至多为多项式。它不要求在每个公式上拥有绝对最短的证明；多项式因子的差距被视为同一复杂度尺度。也不要求一个翻译器自动识别所有源语言，系统 $Q$ 可以作为编译器设计时的固定参数。

最容易混淆的是“有限合并”与“统摄全部系统”。给定有限多个系统，可以给证明加前缀标签并把它们并入一个新系统，这只是有限分派。所有多项式时间验证器虽可枚举，却各有不同时间界、可靠性问题和编码约定；把枚举器直接拼成所谓万能验证器，既可能无法在统一多项式时间内运行，也无法有效判定被模拟机器是否可靠。因此有限构造不能解决 p-最优系统是否存在。

给定两个系统 $P_0,P_1$，可构造合并系统 $R$。证明首位为 $i\in \{0,1\}$ 时，令 $R(i\pi )=P_i(\pi )$；首位或编码非法时输出固定永真式 $z\vee \mathrm{\neg }z$。从 $P_i$ 到 $R$ 的翻译只是添加一位 $i$，耗时与长度均为线性，所以 $R$ p-模拟这两个系统。这个手算构造说明“对任意有限集合都有共同上界”，却没有产生一个对所有系统都有效的有限前缀表。

即使 $P$ p-最优，也不能推出 $P$ 多项式有界。最优性只说：若别的系统对某个公式有长度 $m$ 的证明，$P$ 有长度 $\mathrm{poly}(m)$ 的证明；它没有保证任何系统先拥有 $\mathrm{poly}(|\phi |)$ 的证明。只有再假设某个多项式有界系统存在，p-最优性才会把该性质传给 $P$。因此“p-最优存在”不等于“NP=coNP”。

反过来，给每个永真式选一份最短证明也不构成 Cook–Reckhow 系统：这个选择可能不可计算，更谈不上多项式时间验证。所谓最优必须在可高效核验的系统类内部比较，而不是借助一个知道全部语义真值的非有效目录。

最优命题证明系统与 p-最优命题证明系统是否存在，都是公开问题；目前既没有相应构造，也没有无条件排除。后一个问题连接了证明搜索、可满足性算法、互不相交 NP 对以及弱算术理论中的可证完备性，但这些联系各有编码和 uniformity 假设，不能被简写成某个熟知的 P 对 NP 等式。尤其不能把“尚未找到熟悉系统之间的分离”当作 p-最优系统存在的证据。

若某候选 $P$ 被证明 p-最优，那么对任意具体系统 $Q$ 的证明上界都可转移到 $P$；若还能证明 $P$ 的某个公式族需要超多项式证明，则每个被比较系统都受相应约束。证明系统可自动化性公理库命题证明系统的可自动化性Proof-system automatizability · Automatizability of proof systems以输入公式和该公式最短证明长度的多项式时间找到证明的输出敏感搜索性质。提出另一维问题：即便 $P$ 在长度上统摄其他系统，能否在接近最短证明长度的时间内真正找到证明仍需单独分析。最优性是表示能力的全局上界，不是搜索算法。