命题逻辑的自然推演及规则

在命题逻辑中，形式推演是从给定的前提（可以为空）利用给定的推理规则，得出给定结论的过程。严格定义如下：命题逻辑中的形式推演是一个有穷长的公式序列，序列中的每一项或者是给定的前提，或者是从序列中前面的公式，根据给定的规则得到的公式，序列的末尾是该推演的结论。如果序列末尾的公式是从空前提得到的，则称该公式是命题逻辑的定理，此推理是关于该定理的一个证明。

建构命题逻辑系统时，有公理化方法、公理系统（比如欧氏几何），这种方法严格、可靠、精确，但是与实际推理过程有点距离。还有一种方法就是自然推演方法，是一种特殊的公理化方法，它的公理为零，多借助推理规则推出命题逻辑的定理。

Pᴺ推演规则

1，合取消去规则∧—

从A∧B可推出A；从A∧B可推出B。

2，合取引入规则∧+

从A和B可推出A∧B。

3，析取消去规则∨-

从A∨B，A→C，B→C可推出C。也就是二难推理。

4，析取引入规则∨+

从A可推出A∨B；从B可推出A∨B。

5，蕴涵消去规则→-

从A→B和A可推出B。

6，蕴涵引入规则→+

如果在公式集Γ下引入假设A可以推出B，则在Γ本身之下可以推出A→B。

7，等值消去规则↔-

从A↔B可推出A→B；从A↔B可推出B→A。

8，等值引入规则↔+

从A→B，B→A可推出A↔B。

9，否定消去规则¬-（反证法）

如果在公式集Γ下引入假设¬A可推出B和¬B，则在Γ下可推出A。

10，否定引入规则¬+

如果在公式集Γ下引入假设A可推出B和¬B，则在Γ下可推出¬A。

否定消去规则和否定引入规则有一个就可以。

11，自推规则P

从一组前提或假设A₁，A₂，A₃，…Aₙ出发，可推出该组中的任一公式Aᵢ。