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

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 式系统（可以引入假设）。自然演绎系统通常公理集合较少（典型的情况下可能没有），使用更多的[[推理规则]]代替，这些推理规则可以综合多个前提给出一个新结论。
 自然演绎系统中每一行都是一个公式，通过公式进行变换得到新的公式。其变换规则除了重复、使用规则、引入公理外，还允许假言推理规则（即中途开始一个以假设开始的子证明）和标示步骤（即标记一个仅在当前子证明的域内有效的变项，并在结论中消除其自由出现）。
@@ 第17行： / 第17行： @@
 自然演绎系统是推理系统的一类。
 在自然演绎系统中，推理的每一行都是一个公式，除前提外，每个公式都由当前证明或其外部证明中已出现的公式和变换规则（包括重复已出现的公式、使用给定的推理规则、使用公理）得到。
-此外，自然演绎系统允许假言规则，表现为在证明中开启一个子证明，子证明可以附加有新前提，这样的新前提只在当前子证明其这一子证明内部的新的子证明中有效。
+此外，自然演绎系统允许假言规则，表现为在证明中可以提出新前提，这样的新前提只在部分证明过程中有效。
+一般认为这与人类自然语言描述证明的方式较为贴近，因此称为“自然”。
-== 常见规则 ==
+== 常见书写规则 ==
-=== 自然演绎 ===
+属于自然演绎系统的推理方式有多种不同书写规则，常见主要形式有：
+* [[Gentzen 式自然演绎]]
-关于命题逻辑的自然演绎系统，通常包括以下10条规则。
+* [[Fitch 式自然演绎]]
+* [[Suppes–Lemmon 式自然演绎]]
-* 否定引入（'''<math>\lnot</math>-int'''）：从 <math>\phi\rightarrow\psi</math> 和 <math>\phi\rightarrow\lnot\psi</math> 可推出 <math>\lnot\phi</math> 。由于条件证明规则，在有的理论中的形式是在子证明中假定 <math>\phi</math> ，并演绎出<math>\psi</math> 和 <math>\lnot\psi</math> 。
-* 否定消去（'''<math>\lnot</math>-elim'''）或称双重否定消去（'''<math>\lnot\lnot</math>-elim'''）：从 <math>\lnot\lnot \phi</math> 可推出 <math>\phi</math>
-* 合取引入（'''<math>\land</math>-int'''）：从 <math>\phi</math> 和 <math>\psi</math> 可推出 <math>\phi\land\psi</math>。
-* 合取消去（'''<math>\land</math>-elim'''）：从 <math>\phi\land\psi</math> 可推出 <math>\phi</math> 、从 <math>\phi\land\psi</math> 可推出 <math>\psi</math>。
-* 析取引入（'''<math>\lor</math>-int'''）：从 <math>\phi</math> 可推出 <math>\phi\lor\psi</math> 、从 <math>\phi</math> 可推出 <math>\psi\lor\phi</math>。
-* 析取消去（'''<math>\lor</math>-elim'''）：从 <math>\phi\lor\psi</math> 、 <math>\phi\rightarrow\chi</math> 和 <math>\psi\rightarrow\chi</math> 可推出 <math>\chi</math>。由于条件证明规则，在有的理论中的形式是在两个子证明中假定 <math>\phi</math> 和 <math>\psi</math> ，并均演绎出<math>\chi</math> 。
-* 双条件引入（'''<math>\leftrightarrow</math>-int'''）：从 <math>\phi\rightarrow\psi</math> 和 <math>\psi\rightarrow\phi</math> 可推出 <math>\phi\leftrightarrow\psi</math>。由于条件证明规则，在有的理论中的形式是在两个子证明中假定 <math>\phi</math> 和 <math>\psi</math> ，并演绎出对方。
-* 双条件消去（'''<math>\leftrightarrow</math>-elim'''）：从 <math>\phi\leftrightarrow\psi</math> 可推出 <math>\phi\rightarrow\psi</math> 、 从 <math>\phi\leftrightarrow\psi</math> 可推出 <math>\psi\rightarrow\phi</math> 。
-* 条件消去（'''<math>\rightarrow</math>-elim'''）：从 <math>\phi\rightarrow\psi</math> 和 <math>\phi</math> 可推出 <math>\psi</math>。
-* 条件引入（'''<math>\rightarrow</math>-int'''）（'''假言规则'''）：中途引入一个由假设开始的子证明，假定 <math>\phi</math> 为真后演绎出 <math>\psi</math> ，此子证明可推出 <math>\phi\rightarrow\psi</math> 。
-这些规则都可以看作某种条件下的联结词的引入和消去，因此统称为'''引入消去规则'''或 '''intelim 规则'''。
-其中，由于最后一条必须通过加入假设来进行，前九条称为“非假言规则”，最后一条称为“假言规则”。
-=== 谓词逻辑 ===
-关于谓词逻辑的则增加以下4条规则。
-* 全称量词消去（'''<math>\forall</math>-elim'''，'''US'''/'''UI'''）：从 <math>\forall x \phi</math> 可推出 <math>\phi(t / x)</math> ，其中要求 <math>t</math> 对 <math>x</math> 在 <math>\phi</math> 中可自由代入。
-* 存在量词引入（'''<math>\exists</math>-int'''，'''EG'''）：从 <math>\phi(t / x)</math> 可推出 <math>\exists x \phi</math> ，其中要求 <math>t</math> 对 <math>x</math> 在 <math>\phi</math> 中可自由代入。
-* 等词引入（'''<math>=</math>-int'''）：在任意地方，可以对任意项 <math>t</math> 得到 <math>t=t</math> 。
-* 等词消去（'''<math>=</math>-elim'''）：从 <math>s=t</math> 或 <math>t=s</math>，以及 <math>\phi(s/x)</math> 可以得到 <math>\phi(t/x)</math> 。
-然后还有两条规则，涉及“'''标示'''('''flag''')”一个变量。这意味着引入一个个体变项，且对这个引入项进行使用范围上的限制。
-* 存在量词消去（'''<math>\exists</math>-elim'''，'''ES'''/'''EI'''）：从 <math>\exists x \phi</math> 可推出 <math>\phi(t / x)</math> ，其中要求 <math>t</math> 对 <math>x</math> 在 <math>\phi</math> 中可自由代入，且此步骤将 <math>t</math> 标示。
-* 全称量词引入（'''<math>\forall</math>-int'''，'''UG'''）：标示任意 <math>t</math> 演绎出 <math>\phi(t/x)</math> 可推出 <math>\forall x \phi</math> ，其中要求 <math>t</math> 对 <math>x</math> 在 <math>\phi</math> 中可自由代入。
 {{证明论}}