Cook–Reckhow 命题证明系统

这个定义把“证明是什么”压缩成两个可操作条件：读者拿到证明后必须能迅速检查，而系统必须覆盖所有真的命题。它刻意不规定证明行长什么样；行可以是 Frege 公式、归结子句、整数不等式或多项式。这样才能把不同语法放到同一把尺上，以最短证明长度比较它们，而不把某套演绎记号误当作复杂度结论。

验证时间是证明长度的多项式，而不是公式长度的多项式。一个长度为 $2^n$ 的证明仍可能在 $2^{O(n)}$ 时间逐行检查，完全符合定义。Cook–Reckhow 系统也不承诺能找到证明：验证器面对给定 $\pi$ 只做局部核验，搜索算法却要在指数多个候选串中定位一个原像。正是“易验”和“易找”的分离，使证明长度与自动化成为两个不同问题。

以一个固定 Hilbert–Frege 演算为例，证明串可编码成公式序列。验证器逐行检查：该行是否是某个公理模式的代入实例，或是否由先前两行经 modus ponens 得到；最后比较末行与目标公式。对三行证明，验证器只需扫描三行及其引用，不需要重新枚举公式的全部真值表。若末行是 $p\vee \mathrm{\neg }p$，可靠性定理保证它是永真式；完备性定理保证每个永真式都有某个有限序列。这便给出一个具体 Cook–Reckhow 系统，而非只给出“存在证书”的口号。

有三个边界必须分清。第一，只要求验证关系在多项式时间可判定，却不要求证明长度受公式长度的多项式约束。第二，若删去“值域等于全部 TAUT”而只保留可靠性，永远输出 $p\vee \mathrm{\neg }p$ 的算法也会冒充证明系统；它显然不完备。第三，若允许验证器在证明长度上运行指数时间，任何真值表式核验都可被塞进验证过程，系统间的复杂度比较便失去共同基准。

称 $P$ 多项式有界，若存在多项式 $q$，使每个永真式 $\phi$ 都有 $|\pi |\le q(|\phi |)$ 的 $P$-证明。这里量词顺序是“一个统一多项式控制所有永真式”，不能为每个公式临时选择不同指数。多项式有界系统是否存在，与 NP 和 coNP 的关系紧密，但它不是 Cook–Reckhow 定义本身附带的性质。

函数复杂度类 FP理路函数复杂度类 FPFP · Function polynomial time · 多项式时间函数明确单值函数的全输入输出契约、写出成本与复合封闭性，并区分FP函数、P语言和FNP关系的选择算法。提供本页所用的单值全函数接口及输出长度、复合成本证明。它与多项式可验证的搜索关系不同：在本页给定证明串便要算出指定公式，而不是仅回答某个候选证明是否有效。

若存在多项式有界 Cook–Reckhow 系统，那么 TAUT 具有多项式长度、可多项式时间验证的证书，因而 $\mathrm{TAUT}\in \mathrm{NP}$。TAUT 又是 coNP 完全问题，于是得到 $\mathrm{NP}=\mathrm{coNP}$；反过来，若两类相等，就能用 TAUT 的 NP 验证器构造多项式有界系统。因此“存在多项式有界命题证明系统”恰刻画这个尚未解决的复杂度类等式。相关的coNP理路复杂度类 coNPComplexity class co-NP · coNP补语言属于 NP 的语言类。视角也解释了为何证明复杂度研究的对象是永真式或不可满足公式，而不是 SAT 的满足赋值证书。

这一抽象框架让归结反驳理路归结反驳Resolution refutation · Propositional resolution从 CNF 初始子句反复归结并导出空子句的命题反驳系统。、切割平面证明系统理路切割平面证明系统Cutting planes proof system · CP proof system用布尔变量上的整数线性不等式、非负组合和整数取整导出矛盾的证明系统。、多项式演算理路多项式演算证明系统Polynomial calculus proof system · Polynomial calculus · PC proof system将 CNF 不可满足性编码成域上多项式方程并通过理想推理导出常数一的代数证明系统。与Frege 系统理路Frege 证明系统Frege proof system · Frege system以有限公理模式和有限推理规则对任意命题公式进行演绎的标准强命题证明系统。可以在统一编码下比较。具体系统通常直接反驳不可满足 CNF；单把 $F$ 的反驳视为 $\mathrm{\neg }F$ 的证明，只覆盖了具有这种语法的永真式。要覆盖任意目标公式 $\phi$，可固定一种Tseitin CNF 编码理路Tseitin CNF 转换Tseitin CNF transformation · Tseitin transformation · Tseitin encoding为公式或布尔电路的内部节点引入辅助变量，以线性规模生成保持可满足性投影的 CNF。 $E(\mathrm{\neg }\phi )$，使它与 $\mathrm{\neg }\phi$ 等可满足，证明串包含 $\phi$ 及对该编码的反驳。验证器重新生成编码并核查反驳，通过才输出原公式 $\phi$。这样既保证所有输出永真，又由反驳完备性覆盖全部 TAUT；编码开销也被明确计入。定义只提供公共赛道，并不预先判定哪套系统更强。