演绎定理

数学证明中，“假设 $A$，推出 $B$”几乎等同于证明“若 $A$，则 $B$”。Hilbert 系统的对象语言却只包含公式和少量规则，并没有把“打开一个临时假设块”列为原始动作。演绎定理说明，这种日常证明习惯并非额外的非形式化许可，而是可以被完整编译回 Hilbert 推导。

它完成了一次层次转换。左侧

是关于推导系统的元语言陈述；右侧

则把同一信息压入对象语言中的蕴含公式。正因为这条转换成立，$\to$ 才能稳定承载“在某个假设下可推出”的意义。

一阶侧条件防止的不是技术细枝末节，而是量词范围偷换。临时前提 $P(x)$ 只谈当前赋值下的那个 $x$。若中途把它概括成 $\mathrm{\forall }xP(x)$，就把局部假设提升成了全称断言；演绎定理不能替这种非法提升收尾。

要证明蕴含的传递律

可以依次临时假设 $A\to B$、$B\to C$ 和 $A$。前两次肯定前件先给出 $B$，再给出 $C$。随后按相反顺序三次应用演绎定理，把三个临时前提逐一关闭。这个过程几乎逐字对应自然演绎中的嵌套假设，却最终产生纯 Hilbert 推导。

一阶反例直接展示侧条件。若把 $P(x)$ 当作前提，并允许对其中自由的 $x$ 使用概括规则，就会得到

但

并不有效：取一个至少有两个元素的结构，让 $P$ 只对其中一个元素成立，即可使前件真而后件假。问题来自概括规则改变了临时假设的语义范围。

演绎定理也不是所有逻辑系统都以同一形式满足的普遍定律。模态逻辑若把必然化作为规则，线性逻辑若限制前提的复制与丢弃，原公式都可能需要改写。每个版本必须按照该系统的公理、结构规则和量词规则重新证明，不能只凭“它看起来像蕴含引入”便直接套用。

自然演绎公理库自然演绎Natural deduction用引入规则与消去规则直接刻画逻辑联结词推理行为的证明演算。把蕴含引入当作原始规则：在假设 $\phi$ 的子推导中得到 $\psi$，即可关闭假设并推出 $\phi \to \psi$。Hilbert 系统用公理模式和演绎定理实现同一动作。因此，两种证明风格虽然局部语法不同，却可以系统翻译。

完备性证明频繁使用这条转换。面对形如

的目标，可以转而研究扩张理论 $\mathrm{\Gamma }\cup \{\phi \}$ 是否推出 $\psi$。Lindenbaum 扩充、Henkin 构造以及命题逻辑可靠性与完备性公理库命题逻辑可靠性与完备性定理Soundness and completeness of propositional logic命题演算中的可证性与对所有赋值成立的语义蕴涵恰好一致。的标准证明，都借助这种假设开闭来整理推导。

在自动定理证明中，演绎定理对应假设消去与引理封装：证明器可以在局部上下文中调用额外事实，完成后再把依赖关系显式写进结论。反证法、条件证明和模块化引理共享的也是同一机制。需要保留的核心不是某个固定推导模板，而是“临时前提能够被准确关闭，且不会改变自由变量与资源的作用范围”。