扩展 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$，合成后末行正是没有扩展变量的目标公式。

目前不知道 Frege 是否也能以多项式开销模拟所有 EF 证明；二者也没有已知的超多项式证明长度分离。

每个扩展变量都由当前命题语言中的显式公式定义，右侧公式的编码大小计入证明长度。验证者逐条检查这些定义和后续推理，因而扩展规则保持了多项式时间可验证性。

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

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