|
|
| （未显示同一用户的9个中间版本） |
| 第1行： |
第1行： |
| [[分类:证明论]] | | [[分类:证明论]]{{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</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>
| | * [[Gentzen 式自然演绎]] |
| * 合取引入（'''<math>\land</math>-int'''）：从 <math>\phi</math> 和 <math>\psi</math> 可推出 <math>\phi\land\psi</math>。
| | * [[Fitch 式自然演绎]] |
| * 合取消去（'''<math>\land</math>-elim'''）：从 <math>\phi\land\psi</math> 可推出 <math>\phi</math> 、从 <math>\phi\land\psi</math> 可推出 <math>\psi</math>。
| | * [[Suppes–Lemmon 式自然演绎]] |
| * 析取引入（'''<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> 中可自由代入。 | |
|
| |
|
|
| |
|
| {{证明论}} | | {{证明论}} |
| 自然演绎
|
| 术语名称
|
自然演绎
|
| 英语名称
|
natural deduction
|
自然演绎系统是逻辑领域形式化公理系统的一种，属于 Gentzen 式系统（可以引入假设）。自然演绎系统通常公理集合较少（典型的情况下可能没有），使用更多的推理规则代替，这些推理规则可以综合多个前提给出一个新结论。
自然演绎系统中每一行都是一个公式，通过公式进行变换得到新的公式。其变换规则除了重复、使用规则、引入公理外，还允许假言推理规则（即中途开始一个以假设开始的子证明）和标示步骤（即标记一个仅在当前子证明的域内有效的变项，并在结论中消除其自由出现）。
描述
自然演绎系统是推理系统的一类。
在自然演绎系统中，推理的每一行都是一个公式，除前提外，每个公式都由当前证明或其外部证明中已出现的公式和变换规则（包括重复已出现的公式、使用给定的推理规则、使用公理）得到。
此外，自然演绎系统允许假言规则，表现为在证明中可以提出新前提，这样的新前提只在部分证明过程中有效。
一般认为这与人类自然语言描述证明的方式较为贴近，因此称为“自然”。
常见书写规则
属于自然演绎系统的推理方式有多种不同书写规则，常见主要形式有：
