自然演绎

在数理逻辑中,自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。这种方式对比于使用公理的公理系统。
自然演绎来源自对共通于弗雷格、罗素和希尔伯特系统的判句公理化(希尔伯特演绎系统)的不满。这种公理化最著名使用是在罗素和怀特海的《数学原理》的数学论述中。在1926年由扬·武卡谢维奇在波兰发起的一系列研讨会提倡一种对逻辑的更加自然处理,斯坦尼斯瓦夫·亚希科夫斯基做了定义更自然的演绎的最早尝试,首先在1929年使用了一种图表表示法,并在1934年和1935年的一串行论文中更改了他的提议。但是他的提议没有流行起来。现代形式的自然演绎是由德国数学家格哈德·根岑于1935年在一篇提交给哥廷根大学数学系的学位论文中独立提出的。术语自然演绎就是在那篇论文中出现的: