普遍化

维基百科，自由的百科全书

普遍化是谓词演算的一个推理规则，它声称:

$\mathit{if} \vdash P(x), \mathit{then} \vdash \forall x P(x)$ 。

"普遍化"可以缩写为GEN，而推理规则可以被总结为相继式

$P(x) \vdash \forall x P(x)$ ，

但是这引起了一个重要的限制: 不能应用演绎定理(DT)于它而推导出

$\vdash P(x) \rightarrow \forall x P(x)$ (注意: 这个公式是错的)。

这个公式是错的，因为 x 在前提中是一个无约束的实例，在结论中是一个约束的出现，所以如果这个公式是正确的，则它的 x 的自由实例可以被任何常量(域的元素)所替代:

$\vdash P(t) \rightarrow \forall x P(x)$

但这是不正确的。比如，如果 P(x) 意味着 "x 是素数" 而域是自然数集合，则

$\vdash P(7) \rightarrow \forall x P(x)$

明显不是真的，因为从它和

$\vdash P(7)$ ,

"7 是素数", 可以通过肯定前件推出

$\vdash \forall x P(x)$ ,

"所有自然数都是素数"，这是个矛盾，所以反证法得出这个公式是错的。

这个限制适用于证明: 如果 GEN 在一个证明中应用于一个公式，从而约束了它的自由变量 x，则 DT 不能应用于这个证明中把这个公式移动到十字转门的右侧。

注意 P(x) 符号化带有自由变量 x 的开放陈述，它的真实视 x 而定，但是 $\vdash P(x)$ 符号化(对于 x 的所有值)有效的一个陈述，即使它的变量 x 是自由的。GEN 应用于这种有效陈述，约束自由变量并生成 $\vdash \forall x P(x)$ 。

所以公式 $\vdash \forall x P(x)$ 只是陈述已经被 $\vdash P(x)$ 蕴涵的事情的更明确的方式。

在谓词演算中还有一个公理，它声称

$\vdash \forall x P(x) \rightarrow P(x)$

它通过演绎定理的逆定理可变换成

$\forall x P(x) \vdash P(x)$ ,

这意味着从 $\vdash \forall x P(x)$ 可以推导 $\vdash P(x)$ 。把 GEN 和这个公理放在一起，你可以推出

$\vdash P(x) \ \equiv \ \vdash \forall x P(x)$

它的意义不同于

$P(x) \leftrightarrow \forall x P(x)$ (注意: 这个公式是错的)。

它是错误的原因是 P(x) 可以是任何偶然的(contingent)、无效的、开放公式。为了从根本上防止这种错误的公式，在谓词逻辑中这个限制被增加到 DT 上。

十字转门符号 $\vdash$ 不是合式公式的一部分: 严格的说它既不属于命题演算也不属于谓词演算，而可以被认为是一个"元符号"。所以，最终 $\vdash \forall x P(x)$ 实际上意义不多于 $\vdash P(x)$ ，因为 $\vdash$ 符号实际上不是公式 P(x) 的一部分；比喻来说，它只是用来"抓住"这个公式的一个"把手"。

[编辑] 证明的例子

要证明: $\forall x (P(x) \rightarrow Q(x)) \rightarrow (\forall x P(x) \rightarrow \forall x Q(x))$ .

证明:

编号	公式	理由
1	$\forall x (P(x) \rightarrow Q(x))$	假设
2	$\forall x P(x)$	假设
3	$(\forall x (P(x) \rightarrow Q(x))) \rightarrow (P(x) \rightarrow Q(x)))$	公理 PRED-1
4	$P(x) \rightarrow Q(x)$	从 (1) 和 (3) 通过肯定前件
5	$(\forall x P(x)) \rightarrow P(x)$	公理 PRED-1
6	$P(x) \$	从 (2) 和 (5) 通过肯定前件
7	$Q(x) \$	从 (6) 和 (4) 通过肯定前件
8	$\forall x Q(x)$	从 (7) 通过普遍化
9	$\forall x (P(x) \rightarrow Q(x)), \forall x P(x) \vdash \forall x Q(x)$	总结 (1) 到 (8)
10	$\forall x (P(x) \rightarrow Q(x)) \vdash \forall x P(x) \rightarrow \forall x Q(x)$	从 (9) 通过演绎定理
11	$\vdash \forall x (P(x) \rightarrow Q(x)) \rightarrow (\forall x P(x) \rightarrow \forall x Q(x))$	从 (10) 通过演绎定理