Frege 证明系统

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

可靠性说明每条可证公式在所有赋值下都真，完备性说明每个语义永真式都可证；二者由命题逻辑可靠性与完备性定理理路命题逻辑可靠性与完备性定理Soundness and completeness of propositional logic命题演算中的可证性与对所有赋值成立的语义蕴涵恰好一致。连接。证明复杂度在此基础上追问的是量：完备性构造的证明究竟多长。仅知道某公式有有限证明，不足以判断是否有多项式大小证明。

取两个 Hilbert 公理模式

与

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

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

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

另一个边界是 substitution Frege：它允许对已经证明的永真式作统一代入，作为一条新的显式推理规则。Cook–Reckhow 的 §5 证明这种系统能够 p-模拟扩展 Frege；因此不能仅凭普通 Frege 的公理模式也允许代入，就断言两者具有相同证明能力。该规则应用于无前提定理才保持可靠；若随意替换一个仍依赖未代入假设的结论，推理可以失效。

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

一般 Frege 的超多项式证明大小下界仍是证明复杂度核心开放问题。已有下界多针对受限模型，如有界深度 Frege理路有界深度 FregeBounded-depth Frege · AC0-Frege · Constant-depth Frege将证明行限制为固定常数逻辑深度、通常允许无界扇入联结词的 Frege 片段。、单调系统或特定推理规则。Frege 还与 bounded arithmetic、可行推理和电路复杂度相连，但这些翻译要求精确控制公式编码、理论公理与 proof translation；“Frege 很强”不是可替代定理的结论。