一阶逻辑推理

推理规则

一阶逻辑的推理除了使用命题逻辑中的推理规则外，还需要引入关于量词的推理规则。

$\forall x A (x) \Rightarrow A (c)$

其中 c 为个体域中的某个个体。即如果所有 x 都满足 A(x)，则任取一个个体 c，A(c) 成立。

$A (c) \Rightarrow \forall x A (x)$

其中 c 是任意选取的个体，且不能对 c 附加其他条件。即如果对任意选取的个体 c，A(c) 成立，则所有 x 都满足 A(x)。

$\exists x A (x) \Rightarrow A (c)$

其中 c 是某个特定的个体，且该 c 不曾在公式中出现过。即如果存在 x 满足 A(x)，则可以引入一个特定个体 c 使得 A(c) 成立。

$A (c) \Rightarrow \exists x A (x)$

其中 c 是某个特定的个体。即如果某个特定个体 c 满足 A(c)，则存在 x 满足 A(x)。

对于第一个注，正方向箭头正确，即如果所有 x 都满足 A 或者 x 都满足 B，那么对于所有 x，x 满足 A 或者 B 成立。

对于第二个注，正方向箭头正确，即如果存在一个 x 既满足 A 又满足 B，那么存在一个满足 A 的 x 且存在一个满足 B 的 x。