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

[[分类:证明论]]
'''自然演绎系统'''是命题形式化公理系统的一种，特征是公理集合为空，并使用更多的推理规则。
变换中除了重复、使用规则、引入公理外，还允许假言推理规则（即中途开始一个以假设开始的子证明）和标示步骤（即标记一个仅在当前子证明的域内有效的变项，并在结论中消除其自由出现）。

== 常见规则 ==

=== 自然演绎 ===

关于命题逻辑的自然演绎系统，通常包括以下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>
* 合取引入（'''<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> 中可自由代入。


{{证明论}}