形式陈述

对标准 Hilbert 命题演算，若 $\mathrm{\Gamma }\cup \{\phi \}⊢\psi$，则 $\mathrm{\Gamma }⊢\phi \to \psi$；逆向由 modus ponens 成立。证明对推导长度归纳。带量词的一阶版本需要自由变量和概括规则的侧条件，不能无条件照搬。

直觉

它把“暂时假设 $\phi$ 后证明 $\psi$”内部化成可继续使用的公式 $\phi \to \psi$。

例子与边界

从前提 $P$ 可推出 $Q\to P$，于是可推出 $P\to (Q\to P)$。在模态或带特殊规则的系统中，演绎定理可能需要改写或失效。

推论与应用

解释自然演绎的蕴含引入，并用于证明压缩、理论闭包和完备性证明。

参考资料

• Open Logic Project contributors, Open Logic Project (2026), deduction theorem.
• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed. (2001), deduction theorem and side conditions.