证明系统的 p-模拟

把证明系统想成两种证明语言。若 $P$ p-模拟 $Q$，那么任何用 $Q$ 写成的论证都能由一台固定的高效编译器翻译成 $P$ 论证，而且目标定理完全不变。于是 $Q$ 出现短证明时，$P$ 也一定出现多项式长度证明；反过来没有任何保证。方向写反会把“能容纳别人”误读成“可被别人容纳”，这是证明复杂度图谱中最常见也最实质的错误之一。

p-模拟是传递的。若 $P$ p-模拟 $Q$ 的翻译为 $t$，$R$ p-模拟 $P$ 的翻译为 $u$，那么 $u\circ t$ 在多项式时间内把 $Q$-证明变成 $R$-证明，并保存末式。因此 $Q{\le }_{p}P{\le }_{p}R$ 推出 $Q{\le }_{p}R$。它也是预序而非天然偏序：两个语法不同的系统可以互相 p-模拟，此时只说明它们在多项式尺度上等强，并不要求证明串逐字符相同。

标准 DAG 归结 p-模拟树形归结的翻译最为直接。给定一棵树形反驳，把每个叶、每次 resolution 推导和父子引用原样登记为 DAG 节点；输出甚至可以与输入使用同一线性编码，翻译耗时 $O(|\pi |)$，末节点仍是空子句。类似地，扩展 Frege 可把一份普通 Frege 证明逐行照抄而完全不用扩展规则，所以“扩展系统 p-模拟基础系统”有一个明确的恒等翻译，而不是根据名称猜出的强弱关系。

再看组合开销。若第一段翻译把长度 $m$ 扩为至多 $m^3+1$，第二段把长度 $s$ 扩为至多 $2s^2$，组合后长度至多 $2(m^3+1{)}^2=O(m^6)$，仍为多项式。这里指数可以增大，但不能依赖具体公式临时变化。若有人只证明“$P$ 与 $Q$ 都可靠完备”，那只说明二者的值域都是 TAUT，完全没有给出短证明之间的翻译。

边界还包括 uniformity。对每个证明长度 $m$ 各自声称存在一张小电路，未必给出一台统一多项式时间翻译机；对每个 $\pi$ 选择一个短 $P$-证明，也未必可计算。另一方面，p-模拟不要求保留行数、宽度、深度或语法结构，只控制总编码长度与翻译时间；研究这些细粒度资源时必须另加条件。

若 $P$ p-模拟 $Q$，则对每个永真式 $\phi$，最短证明长度满足

对某个固定多项式 $q$ 成立。因此对 $P$ 的超多项式下界会传递给所有被 $P$ p-模拟的系统：若 $Q$ 有短证明而 $P$ 被证明必须很长，就会直接反驳模拟关系。反方向不成立；弱系统的下界通常不能自动推出强系统的下界。

证明系统最优性公理库命题证明系统的最优性Optimal proof system · p-optimal proof system以能否统一模拟或 p-模拟所有命题证明系统定义的全局最优性概念。把这个二元比较提升为“是否存在一个系统 p-模拟所有系统”。证明系统可自动化性公理库命题证明系统的可自动化性Proof-system automatizability · Automatizability of proof systems以输入公式和该公式最短证明长度的多项式时间找到证明的输出敏感搜索性质。则问能否从公式本身找到接近最短的证明。翻译器的输入已经包含一份 $Q$-证明，而自动化算法没有这份提示，所以 p-模拟强并不自动意味着容易搜索。将二者分开，才能准确表达“证明存在、证明可翻译、证明可找到”三层不同难度。