||
在数理逻辑中,自然演绎(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.
证明 :
p → q 前提
p → ¬q 前提
[p] 假设
q MP: 1,3
¬q MP: 2,3
⊥ ⊥I: 4,5 (contradiction)
¬p ab absurde
习题2:
证明 p →(q → r) ⊢ (p ∧ q) → r.
证明 :
p →(q → r) 前提
[p ∧ q] 假设
p ∧E: 2
q → r MP: 1,3
q ∧E: 2
r MP: 4,5
(p ∧ q) → r →I: 2,6
参考文献:
https://fr.wikipedia.org/wiki/Déduction_naturelle
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-12-3 04:56
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社