|
|
| 第17行： |
第17行： |
| 自然演绎系统是推理系统的一类。 | | 自然演绎系统是推理系统的一类。 |
| 在自然演绎系统中，推理的每一行都是一个公式，除前提外，每个公式都由当前证明或其外部证明中已出现的公式和变换规则（包括重复已出现的公式、使用给定的推理规则、使用公理）得到。 | | 在自然演绎系统中，推理的每一行都是一个公式，除前提外，每个公式都由当前证明或其外部证明中已出现的公式和变换规则（包括重复已出现的公式、使用给定的推理规则、使用公理）得到。 |
| 此外，自然演绎系统允许假言规则，表现为在证明中开启一个子证明，子证明附加有新前提，这样的新前提只在当前子证明及这内部的子证明中有效。
| | 此外，自然演绎系统允许假言规则，表现为在证明中可以提出新前提，这样的新前提只在部分证明过程中有效。 |
| | 一般认为这与人类自然语言描述证明的方式较为贴近，因此称为“自然”。 |
|
| |
|
| == 常见规则 == | | == 常见书写规则 == |
| | |
| === 自然演绎 ===
| |
| | |
| 关于命题逻辑的自然演绎系统，通常包括以下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>=_\mathrm{I}</math>'''，'''<math>=</math>-int'''）：在任意地方，可以对任意项 <math>t</math> 得到 <math>t=t</math> 。
| |
| * 等词消去（'''<math>=_\mathrm{E}</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> 中可自由代入。
| |
| | |
| == 常见书写记号 ==
| |
|
| |
|
| 属于自然演绎系统的推理方式有多种不同书写规则，常见主要形式有： | | 属于自然演绎系统的推理方式有多种不同书写规则，常见主要形式有： |
| 自然演绎
|
| 术语名称
|
自然演绎
|
| 英语名称
|
natural deduction
|
自然演绎系统是逻辑领域形式化公理系统的一种，属于 Gentzen 式系统，其特征是可以引入假设。自然演绎系统通常公理集合较少（典型的情况下可能没有），使用更多的推理规则代替，这些推理规则可以综合多个前提给出一个新结论。
自然演绎系统中每一行都是一个公式，通过公式进行变换得到新的公式。其变换规则除了重复、使用规则、引入公理外，还允许假言推理规则（即中途开始一个以假设开始的子证明）和标示步骤（即标记一个仅在当前子证明的域内有效的变项，并在结论中消除其自由出现）。
描述
自然演绎系统是推理系统的一类。
在自然演绎系统中，推理的每一行都是一个公式，除前提外，每个公式都由当前证明或其外部证明中已出现的公式和变换规则（包括重复已出现的公式、使用给定的推理规则、使用公理）得到。
此外，自然演绎系统允许假言规则，表现为在证明中可以提出新前提，这样的新前提只在部分证明过程中有效。
一般认为这与人类自然语言描述证明的方式较为贴近，因此称为“自然”。
常见书写规则
属于自然演绎系统的推理方式有多种不同书写规则，常见主要形式有：
