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

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

== 描述 ==

自然演绎系统是推理系统的一类。
在自然演绎系统中，推理的每一行都是一个公式，除前提外，每个公式都由当前证明或其外部证明中已出现的公式和变换规则（包括重复已出现的公式、使用给定的推理规则、使用公理）得到。
此外，自然演绎系统允许假言规则，表现为在证明中开启一个子证明，子证明可以附加有新前提，这样的新前提只在当前子证明其这一子证明内部的新的子证明中有效。

== 常见规则 ==

=== 自然演绎 ===

关于命题逻辑的自然演绎系统，通常包括以下10条规则。

* 否定引入（'''<math>\lnot_\mathrm{I}</math>''' 或 '''<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\lnot_\mathrm{E}</math>''' 或 '''<math>\lnot\lnot</math>-elim'''）：从 <math>\lnot\lnot \phi</math> 可推出 <math>\phi</math> 。（有些材料可能称为否定消去 '''<math>\lnot</math>-elim'''）
* 合取引入（'''<math>\land_\mathrm{I}</math>''' 或 '''<math>\land</math>-int'''）：从 <math>\phi</math> 和 <math>\psi</math> 可推出 <math>\phi\land\psi</math>。
* 合取消去（'''<math>\land_\mathrm{E}</math>''' 或 '''<math>\land</math>-elim'''）：从 <math>\phi\land\psi</math> 可推出 <math>\phi</math> 、从 <math>\phi\land\psi</math> 可推出 <math>\psi</math>。
* 析取引入（'''<math>\lor_\mathrm{I}</math>''' 或 '''<math>\lor</math>-int'''）：从 <math>\phi</math> 可推出 <math>\phi\lor\psi</math> 、从 <math>\phi</math> 可推出 <math>\psi\lor\phi</math>。
* 析取消去（'''<math>\lor_\mathrm{E}</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_\mathrm{I}</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_\mathrm{E}</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_\mathrm{E}</math>''' 或 '''<math>\rightarrow</math>-int'''）（'''假言规则'''）：中途引入一个由假设开始的子证明，假定 <math>\phi</math> 为真后演绎出 <math>\psi</math> ，此子证明可推出 <math>\phi\rightarrow\psi</math> 。
* 条件消去（'''<math>\rightarrow_\mathrm{E}</math>''' 或 '''<math>\rightarrow</math>-elim'''）：从 <math>\phi\rightarrow\psi</math> 和 <math>\phi</math> 可推出 <math>\psi</math>。

这些规则都可以看作某种条件下的联结词的引入和消去，因此统称为'''引入消去规则'''或 '''intelim 规则'''。

其中，由于条件引入必须通过加入假设来进行，这一条称为“假言规则”，其他九条称为“非假言规则”。

注：根据不同人的排版习惯，引入、消去的标记可能使用 <math>\odot</math>-int/elim 、 <math>\odot I/E</math> 、 <math>\odot \mathrm{I}/\mathrm{E}</math> 、 <math>\odot_{I/E}</math> 、 或 <math>\odot_{\mathrm{I}/\mathrm{E}}</math> 等。

=== 谓词逻辑 ===

关于谓词逻辑的则增加以下4条规则。

* 全称量词消去（'''<math>\forall_\mathrm{E}</math>'''，'''<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_\mathrm{I}</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> 。

然后还有两条规则，涉及一个自由变项。这意味着引入一个个体变项，且对这个引入项进行使用范围上的限制。

* 存在量词消去（'''<math>\exists_\mathrm{E}</math>'''，'''<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_\mathrm{I}</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> 中可自由代入。

== 常见书写记号 ==

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


{{证明论}}