自然演绎系统

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

常见规则

自然演绎

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

否定引入（[math]\displaystyle{ \lnot }[/math]-int）：从 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 和 [math]\displaystyle{ \phi\rightarrow\lnot\psi }[/math] 可推出 [math]\displaystyle{ \lnot\phi }[/math] 。由于条件证明规则，在有的理论中的形式是在子证明中假定 [math]\displaystyle{ \phi }[/math] ，并演绎出[math]\displaystyle{ \psi }[/math] 和 [math]\displaystyle{ \lnot\psi }[/math] 。
否定消去（[math]\displaystyle{ \lnot }[/math]-elim）或称双重否定消去（[math]\displaystyle{ \lnot\lnot }[/math]-elim）：从 [math]\displaystyle{ \lnot\lnot \phi }[/math] 可推出 [math]\displaystyle{ \phi }[/math]
合取引入（[math]\displaystyle{ \land }[/math]-int）：从 [math]\displaystyle{ \phi }[/math] 和 [math]\displaystyle{ \psi }[/math] 可推出 [math]\displaystyle{ \phi\land\psi }[/math]。
合取消去（[math]\displaystyle{ \land }[/math]-elim）：从 [math]\displaystyle{ \phi\land\psi }[/math] 可推出 [math]\displaystyle{ \phi }[/math] 、从 [math]\displaystyle{ \phi\land\psi }[/math] 可推出 [math]\displaystyle{ \psi }[/math]。
析取引入（[math]\displaystyle{ \lor }[/math]-int）：从 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \phi\lor\psi }[/math] 、从 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \psi\lor\phi }[/math]。
析取消去（[math]\displaystyle{ \lor }[/math]-elim）：从 [math]\displaystyle{ \phi\lor\psi }[/math] 、 [math]\displaystyle{ \phi\rightarrow\chi }[/math] 和 [math]\displaystyle{ \psi\rightarrow\chi }[/math] 可推出 [math]\displaystyle{ \chi }[/math]。由于条件证明规则，在有的理论中的形式是在两个子证明中假定 [math]\displaystyle{ \phi }[/math] 和 [math]\displaystyle{ \psi }[/math] ，并均演绎出[math]\displaystyle{ \chi }[/math] 。
双条件引入（[math]\displaystyle{ \leftrightarrow }[/math]-int）：从 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 和 [math]\displaystyle{ \psi\rightarrow\phi }[/math] 可推出 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math]。由于条件证明规则，在有的理论中的形式是在两个子证明中假定 [math]\displaystyle{ \phi }[/math] 和 [math]\displaystyle{ \psi }[/math] ，并演绎出对方。
双条件消去（[math]\displaystyle{ \leftrightarrow }[/math]-elim）：从 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math] 可推出 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 、从 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math] 可推出 [math]\displaystyle{ \psi\rightarrow\phi }[/math] 。
条件消去（[math]\displaystyle{ \rightarrow }[/math]-elim）：从 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 和 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \psi }[/math]。
条件引入（[math]\displaystyle{ \rightarrow }[/math]-int）：若假定 [math]\displaystyle{ \phi }[/math] 为真后可演绎出 [math]\displaystyle{ \psi }[/math] ，可推出 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 。

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

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

谓词逻辑

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

全称量词消去（[math]\displaystyle{ \forall }[/math]-elim，US/UI）：从 [math]\displaystyle{ \forall x \phi }[/math] 可推出 [math]\displaystyle{ \phi(t / x) }[/math] ，其中要求 [math]\displaystyle{ t }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入。
存在量词引入（[math]\displaystyle{ \exists }[/math]-int，EG）：从 [math]\displaystyle{ \phi(t / x) }[/math] 可推出 [math]\displaystyle{ \exists x \phi }[/math] ，其中要求 [math]\displaystyle{ t }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入。
等词引入（[math]\displaystyle{ = }[/math]-int）：在任意地方，可以对任意项 [math]\displaystyle{ t }[/math] 得到 [math]\displaystyle{ t=t }[/math] 。
等词消去（[math]\displaystyle{ = }[/math]-elim）：从 [math]\displaystyle{ s=t }[/math] 或 [math]\displaystyle{ t=s }[/math]，以及 [math]\displaystyle{ \phi(s/x) }[/math] 可以得到 [math]\displaystyle{ \phi(t/x) }[/math] 。

然后还有两条规则，涉及“标示(flag)”一个变量。这意味着引入一个个体变项，且对这个引入项进行使用范围上的限制。

存在量词消去（[math]\displaystyle{ \exists }[/math]-elim，ES/EI）：从 [math]\displaystyle{ \exists x \phi }[/math] 可推出 [math]\displaystyle{ \phi(t / x) }[/math] ，其中要求 [math]\displaystyle{ t }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入，且此步骤将 [math]\displaystyle{ t }[/math] 标示。
全称量词引入（[math]\displaystyle{ \forall }[/math]-int，UG）：标示任意 [math]\displaystyle{ t }[/math] 演绎出 [math]\displaystyle{ \phi(t/x) }[/math] 可推出 [math]\displaystyle{ \forall x \phi }[/math] ，其中要求 [math]\displaystyle{ t }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入。

证明论
形式化公理系统（形式化、公理化）
举例	公理系统、自然演绎系统
证明、演绎	证明、可证明、演绎、可演绎
命题、定理	公理、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完全性、一致性、独立性