扩展 Frege 证明系统

普通 Frege 已能引用先前整行，却仍把每行内部的公式写成树；若同一大型子式在很多位置出现，文本会反复复制。EF 把“令 $e$ 表示这个子式”变成受认证的证明步骤，后续只写一个变量。它类似编译器的 common subexpression elimination：不改变计算的布尔函数，只改变表示及共享方式。

新变量之所以必须 fresh，是因为定义需要是保守扩展。若允许 $e$ 已带有别的含义，或允许自指式 $e\leftrightarrow \mathrm{\neg }e$，新公理本身就不可满足，任何公式都可由矛盾推出。无环、新鲜的 extension axioms 则总能从原赋值唯一延拓，可靠性由这个延拓机制保障。

为了证明

可先引入

Frege 推理从定义得到 $e_2\to e_1$ 与 $e_1\to p$，再推出 $e_2\to p$；同时由原前件和两条定义得到 $((p\wedge q)\wedge r)\to e_2$，合成后末行正是没有扩展变量的目标公式。若大型子式 $p\wedge q$ 在后续一百行中反复使用，证明仍只保留一次定义，这才是扩展规则的规模收益。

这个例子只展示压缩机制，并未证明渐近优势。虽然 EF 显然 p-模拟普通 Frege，目前不知道 Frege 是否也能以多项式开销模拟所有 EF 证明；也没有已知的超多项式 Frege–EF 分离。正因如此，frontmatter 不能把 EF 反向归类成 Frege 的已知严格特例，也不能用 symmetric equivalent 边声称二者已知 p-等价。

EF 也不等于给证明任意 oracle gate。每个 $e$ 只能定义为当前命题语言中的显式公式；定义右侧的编码大小仍计入证明。若允许一个符号在常数长度内代表指数规模真值表，便悄悄改变了输入表示和验证时间。

EF 与多项式规模布尔电路推理关系紧密：扩展变量对应门，定义依赖图对应电路连线。许多不同的 extended Frege 公理化可通过局部门翻译互相 p-模拟，因而通常把 EF 视为稳健的强证明系统。它也能高效模拟 resolution、cutting planes 的常见有限系数推理以及多种代数系统的编码，但每项模拟都有表示与系数位长条件，不能仅凭系统名称建立无条件等价边。

对 EF 给出显式超多项式下界是重大开放问题，并会触及一般电路下界与可行推理障碍。证明系统最优性公理库命题证明系统的最优性Optimal proof system · p-optimal proof system以能否统一模拟或 p-模拟所有命题证明系统定义的全局最优性概念。比“EF 是否最强的熟悉系统”更严格：p-最优系统必须模拟所有 Cook–Reckhow 系统；目前既不知道 EF p-最优，也不知道任何 p-最优系统存在。