查看“︁自然演绎系统”︁的源代码

[[分类:证明论]]{{DEFAULTSORT:zi4ran2yan3yi4xi4tong3}}
{{#seo:
|keywords=自然演绎系统
|description=自然演绎系统是根岑式系统的一种，每次通过出现过的公式推理出新的结论。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-19
}}
{{InfoBox
|name=自然演绎
|eng_name=natural deduction
}}
'''自然演绎系统'''是逻辑领域[[形式化公理系统（逻辑）|形式化公理系统]]的一种，属于 Gentzen 式系统，其特征是可以引入假设。自然演绎系统通常公理集合较少（典型的情况下可能没有），使用更多的[[推理规则]]代替，这些推理规则可以综合多个前提给出一个新结论。
自然演绎系统中每一行都是一个公式，通过公式进行变换得到新的公式。其变换规则除了重复、使用规则、引入公理外，还允许假言推理规则（即中途开始一个以假设开始的子证明）和标示步骤（即标记一个仅在当前子证明的域内有效的变项，并在结论中消除其自由出现）。

== 描述 ==

自然演绎系统是推理系统的一类。
在自然演绎系统中，推理的每一行都是一个公式，除前提外，每个公式都由当前证明或其外部证明中已出现的公式和变换规则（包括重复已出现的公式、使用给定的推理规则、使用公理）得到。
此外，自然演绎系统允许假言规则，表现为在证明中可以提出新前提，这样的新前提只在部分证明过程中有效。
一般认为这与人类自然语言描述证明的方式较为贴近，因此称为“自然”。

== 常见书写规则 ==

属于自然演绎系统的推理方式有多种不同书写规则，常见主要形式有：
* [[Gentzen 式自然演绎]]
* [[Fitch 式自然演绎]]
* [[Suppes–Lemmon 式自然演绎]]


{{证明论}}