谓词逻辑的推理演算

1．推理定律

下面列出一些常用的推理定律（同命题逻辑一样，在后面的推理演算中以大写字母I加以引用）。

1）由命题逻辑推理定律推广而来的谓词逻辑推理定律

利用代入定理将命题逻辑中的推理定律推广而得到谓词逻辑中的推理定律。

如在命题逻辑中有公式：

α∧β⇒α，α⇒α∨β

可推广而得：

∀x A（x）∧∀y B（y）⇒∀x A（x），∀x A（x）⇒∀x A（x）∨∃y B（y）

等。

2）由基本等值式生成的推理定律

谓词等值式中的每个等值式可生成两个推理定律。例如：

∀x A（x）⇒﹁﹁∀x A（x），﹁﹁∀x A（x）⇒∀x A（x）

和 ﹁∀x A（x）⇒∃x﹁A（x），∃x﹁A（x）⇒﹁∀x A（x）

等。

3）一些特有的重要推理定律

（1）∀x A（x）∨∀x B（x）⇒∀x（A（x）∨B（x））

（2）∃x（A（x）∧B（x））⇒∃x A（x）∧∃x B（x）

（3）∀x（A（x）→B（x））⇒∀x A（x）→∀x B（x）

（4）∃x（A（x）→B（x））⇒∃x A（x）→∃x B（x）

等。

2．推理规则

命题逻辑中所使用的推理规则，都可以应用于谓词逻辑的推理中。除此以外，由于谓词逻辑中引进了个体、谓词和量词等，因此又增加了一些推理规则。

1）全称量词消去规则（US）

（1）∀x A（x）⇒A（y）或

（2）∀x A（x）⇒A（c）

两式成立的条件是：

①x是A（x）的自由变元；

②在（1）中，y为不在A（x）中约束出现的变元，y可以在A（x）中自由出现，也可在证明序列中前面的公式中出现；

③在（2）中，c为任意的个体常元，可以是证明序列中前面公式所指定的个体常元。

2）全称量词引入规则（UG）

A（y）⇒∀x A（x）

该式成立的条件是：

①y在A（y）中自由出现，且y取任何值时A均为真；

②替换y的x要选择在A（y）中不出现的变元符号。

3）存在量词消去规则（ES）

∃x A（x）⇒A（c）

该式成立的条件是：

①c是使A为真特定的个体常元，c不能在前面的公式序列中出现；

②c不曾在A（x）中出现；

③A（x）中除x外还有其他自由出现的个体变元时，不能用此规则。

4）存在量词引入规则（EG）

A（c）⇒∃x A（x）

该式成立的条件是：

①c是特定的个体常元；

②替换c的x要选择在A（c）中没有出现过的变元符号。

需要注意的是，以上四条规则只能对前束范式使用。

在谓词逻辑中，常用的推理方法有两种：直接证法和间接证法。间接证法又包含两种：反证法和CP规则。其内容与命题逻辑中的类似。