在数理逻辑中，自然演绎（natural deduction）是一个形式系统，其推理方法是一种接近于自然推理的演绎法，与希尔伯特系统的主要区别是没有公理，这是证明理论史上的重要一步。

一，自然演绎法的源起

“自然演绎”是德国数学家根岑（Gerhard Gentzen，1909－1945）于1935年在一篇提交给哥廷根大学数学系的学位论文中提出的：

- 首先我希望构造尽可能接近于实际推理的一种形式化主义，所以提议了“自然演绎演算”。

— Gentzen, (Mathematische Zeitschrift 39, pp.176-210, 1935)

许多逻辑学家，从弗雷格和希尔伯特开始，还有罗素和怀特海的《数学原理》（Principia Mathematica），在欧几里得方法的启发下，以公理的形式发展了逻辑：基本上是利用肯定前件（拉丁语：Modus ponens）从公理中推导出来的。这种方法揭示了与以下事实有关的困难：根据假设进行推理，这是数学中常见的做法，但不能在这样的方法中直接表示出来。

根岑通过部分放弃欧几里得方法，使逻辑学重新具有自然路径的特征，更好地接近数学实践。根岑的主要想法很简单：用演绎规则取代希尔伯特式系统中必要但不自然的逻辑公理。在这样做的过程中，根岑开发了一个非常对称的逻辑表述，其中每个逻辑操作符都是由一对双重规则定义的：引入和消除。

二，自然演绎系统

1，问题表述

自然演绎的逻辑后承（consequence）关系符号⊢ ，表示：

证明：Σ ⊢ ψ

或者

证明：Σ,¬ψ ⊢⊥（反证法）

Σ指一组前提，Σ= φ1 ∧ φ2 ∧...∧ φn ；ψ指结论。

2，推理规则

（1）主要推理规则

- Modus Ponens （MP，肯定前件）

p →  q, p

———————

q

- Modus Tonens （MT，否定后件）

p →  q, ¬ q

———————

¬ P

（2）逻辑操作符的引入和消除规则

三，例子

习题1 

证明 p → q, p → ¬q ⊢ ¬p.

证明 :

1. p → q      前提

2. p → ¬q    前提

3. [p]           假设

4. q             MP: 1,3

5. ¬q           MP: 2,3

6. ⊥             ⊥I: 4,5 (contradiction)

7. ¬p           ab absurde

习题2: 

证明 p →(q → r) ⊢ (p ∧ q) → r.

证明 :

1. p →(q → r)       前提

2. [p ∧ q]              假设

3. p                       ∧E: 2

4. q → r                MP: 1,3

5. q                       ∧E: 2

6. r                       MP: 4,5

7. (p ∧ q) → r       →I: 2,6

参考文献：

https://fr.wikipedia.org/wiki/Déduction_naturelle