Frege 证明系统 | Codeboy's Blog

形式陈述

Frege 系统固定一个函数完备的命题联结词基、有限组公理模式和有限组推理规则。证明是一列命题公式，每行要么是公理模式的代入实例，要么由先前若干行按某条规则推出，末行是目标永真式。典型 Hilbert 版本只用 modus ponens：

A,\quad A\to B\quad\Longrightarrow\quad B.

公理模式允许用任意公式统一替换模式变量；“有限”指模式与规则种类固定，不是其代入实例只有有限个。只要系统可靠且完备，每份证明都可逐行多项式时间核验，所有永真式又都有证明，因此 Frege 是Cook–Reckhow 命题证明系统的具体实例。

证明大小通常取所有行的符号总数，而不仅是行数。不同合理 Frege 公理化、不同有限完备联结词基以及 Hilbert 与有限规则版本之间可相互 p-模拟；这个稳健性结论依赖固定编码和多项式翻译，不表示它们逐行相同。

直觉

归结的中间行只能是子句，Frege 行却可保存任意嵌套命题结构。它能把已经证明的复杂公式当作整体代入公理模式，再由规则组合，因此更接近普通数学演绎。强表达力也让下界更难：若试图证明某一行“必须很宽”，Frege 可以换一种等价语法重组信息，局部子句指标不再控制全部证明。

可靠性说明每条可证公式在所有赋值下都真，完备性说明每个语义永真式都可证；二者由命题逻辑可靠性与完备性定理连接。证明复杂度在此基础上追问的是量：完备性构造的证明究竟多长。仅知道某公式有有限证明，不足以判断是否有多项式大小证明。

例子与边界

取两个 Hilbert 公理模式

A\to(B\to A)

与

\bigl(A\to(B\to C)\bigr)\to \bigl((A\to B)\to(A\to C)\bigr).

公式 $p\to p$ 有如下五行证明：

\begin{aligned} 1.\;&p\to((p\to p)\to p),\\ 2.\;&p\to(p\to p),\\ 3.\;&[p\to((p\to p)\to p)]\to([p\to(p\to p)]\to(p\to p)),\\ 4.\;&[p\to(p\to p)]\to(p\to p),\\ 5.\;&p\to p. \end{aligned}

前两行分别是第一模式的代入，第三行是第二模式的代入；第四行由第 1、3 行 modus ponens，末行由第 2、4 行得到。这条逐行 trace 展示了“模式实例”与“规则引用”如何被验证，而不是把 $p\to p$ 的真值表当成 Frege 证明。

Frege 不允许随意给大公式取新名字；共享只能通过重复引用整行实现，公式内部的重复子式仍按树形语法计入长度。扩展 Frege加入新变量定义来获得电路式共享。扩展 Frege p-模拟 Frege 很直接，但目前不知道普通 Frege 是否 p-模拟扩展 Frege，也不知道二者存在超多项式证明长度分离，不能把语法差别写成已证复杂度分离。

另一个边界是 substitution Frege：把已证公式作统一代入作为显式规则，可能改变逐行表示；与普通 Frege 的多项式等价需引用具体模拟定理，不能仅凭二者都“允许模式”混同。

推论与应用

Frege 可以多项式模拟许多弱命题系统的基本推理，包括标准 resolution 的每一步；于是若对 Frege 证明某个显式永真式族的超多项式下界，也会同时覆盖这些弱系统。反方向的 resolution 下界并不能传给 Frege，因为强系统可能用非子句中间公式绕过宽度瓶颈。

一般 Frege 的超多项式证明大小下界仍是证明复杂度核心开放问题。已有下界多针对受限模型，如有界深度 Frege、单调系统或特定推理规则。Frege 还与 bounded arithmetic、可行推理和电路复杂度相连，但这些翻译要求精确控制公式编码、理论公理与 proof translation；“Frege 很强”不是可替代定理的结论。

参考资料

Stephen A. Cook and Robert A. Reckhow, “The Relative Efficiency of Propositional Proof Systems,” Journal of Symbolic Logic 44(1), 1979, pp. 36–50, §§2–3.
Jan Krajíček, Bounded Arithmetic, Propositional Logic, and Complexity Theory, Cambridge University Press, 1995, Chapter 4, Frege systems.
Pavel Pudlák, “The Lengths of Proofs,” in Samuel R. Buss (ed.), Handbook of Proof Theory, Elsevier, 1998, pp. 547–637, §§4–5.

形式陈述 ​

反向链接

形式陈述