形式陈述

自然演绎是一类以“引入规则”和“消去规则”刻画逻辑联结词的证明演算。例如

$$ \frac{\Gamma\vdash A\qquad\Gamma\vdash B}{\Gamma\vdash A\land B}(\land I), \qquad \frac{\Gamma\vdash A\land B}{\Gamma\vdash A}(\land E), $$$$\frac{\mathrm{\Gamma }⊢A\mathrm{\Gamma }⊢B}{\mathrm{\Gamma }⊢A\wedge B}(\wedge I),\frac{\mathrm{\Gamma }⊢A\wedge B}{\mathrm{\Gamma }⊢A}(\wedge E),$$

而蕴涵引入从在临时假设 $A$$A$ 下得到 $B$$B$ 的推导，解除该假设并推出 $A\to B$$A\to B$。存在量词消去、析取消去等规则也包含“新变量”或假设解除的侧条件。直觉主义系统不含经典排中或双重否定消去；经典自然演绎可额外加入这些原则。

直觉

每个联结词有一对操作：引入规则说明怎样构造该联结词的证据，消去规则说明拥有该证据后能安全取出什么信息。假设像局部作用域，可在规则结束时被解除。

例子与边界

从 $A\land B$$A\wedge B$ 可经两次消去分别得到 $A$$A$、$B$$B$；在假设 $A$$A$ 下若推出 $B$$B$，便可解除 $A$$A$ 得到 $A\to B$$A\to B$。不能把未解除的临时假设当作无条件定理。存在消去中选取的见证变量必须对最终结论保持新鲜，否则可能把某个特殊见证误当成任意对象。证明树的叶通常是开放假设，根是结论；不同教材可采用序列式、盒式或 Fitch 记法，但规则含义一致。自然演绎的“自然”不代表自动证明搜索总是容易，规则反向使用仍可能产生巨大分支。

推论与应用

自然演绎直接对应结构化证明、类型系统中的 Curry–Howard 对应和交互式定理证明器。规范化定理还能消去相邻的引入—消去绕路，揭示证明的计算内容。

参考资料

• A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2nd ed., Cambridge University Press, 2000，Chs. 1–3, natural deduction, discharge, and normalization。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Part A, deduction systems and first-order rules。