自然演绎系统：修订间差异

2026年1月21日 (三) 11:48的最新版本

自然演绎
术语名称	自然演绎
英语名称	natural deduction

自然演绎系统是逻辑领域形式化公理系统的一种，属于 Gentzen 式系统（可以引入假设）。自然演绎系统通常公理集合较少（典型的情况下可能没有），使用更多的推理规则代替，这些推理规则可以综合多个前提给出一个新结论。自然演绎系统中每一行都是一个公式，通过公式进行变换得到新的公式。其变换规则除了重复、使用规则、引入公理外，还允许假言推理规则（即中途开始一个以假设开始的子证明）和标示步骤（即标记一个仅在当前子证明的域内有效的变项，并在结论中消除其自由出现）。

描述

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

常见书写规则

属于自然演绎系统的推理方式有多种不同书写规则，常见主要形式有：

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统：Hilbert 表示
	Gentzen 风格-自然演绎系统： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性

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