普遍化

维基百科,自由的百科全书
跳转至: 导航搜索

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

如果  \vdash P(x)  \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) 通过演绎定理

在这个证明中,DT 应用于步骤 (10),因为被引动到十字转门的右侧(通过 DT)的公式  \forall x P(x) 不包含任何自由变量。DT 也出于同样的原因而应用于步骤 (11)。