普遍化
维基百科,自由的百科全书
。
"普遍化"可以缩写为GEN,而推理规则可以被总结为相继式
,
但是这引起了一个重要的限制: 不能应用演绎定理(DT)于它而推导出
(注意: 这个公式是错的)。
这个公式是错的,因为 x 在前提中是一个无约束的实例,在结论中是一个约束的出现,所以如果这个公式是正确的,则它的 x 的自由实例可以被任何常量(域的元素)所替代:
但这是不正确的。比如,如果 P(x) 意味着 "x 是素数" 而域是自然数集合,则
明显不是真的,因为从它和
,
"7 是素数", 可以通过肯定前件推出
,
"所有自然数都是素数",这是个矛盾,所以反证法得出这个公式是错的。
这个限制适用于证明: 如果 GEN 在一个证明中应用于一个公式,从而约束了它的自由变量 x,则 DT 不能应用于这个证明中把这个公式移动到十字转门的右侧。
注意 P(x) 符号化带有自由变量 x 的开放陈述,它的真实视 x 而定,但是 符号化(对于 x 的所有值)有效的一个陈述,即使它的变量 x 是自由的。GEN 应用于这种有效陈述,约束自由变量并生成
。
所以公式 只是陈述已经被
蕴涵的事情的更明确的方式。
在谓词演算中还有一个公理,它声称
它通过演绎定理的逆定理可变换成
,
这意味着从 可以推导
。把 GEN 和这个公理放在一起,你可以推出
它的意义不同于
(注意: 这个公式是错的)。
它是错误的原因是 P(x) 可以是任何偶然的(contingent)、无效的、开放公式。为了从根本上防止这种错误的公式,在谓词逻辑中这个限制被增加到 DT 上。
十字转门符号 不是合式公式的一部分: 严格的说它既不属于命题演算也不属于谓词演算,而可以被认为是一个"元符号"。所以,最终
实际上意义不多于
,因为
符号实际上不是公式 P(x) 的一部分;比喻来说,它只是用来"抓住"这个公式的一个"把手"。
[编辑] 证明的例子
要证明: .
证明:
编号 | 公式 | 理由 |
---|---|---|
1 | ![]() |
假设 |
2 | ![]() |
假设 |
3 | ![]() |
公理 PRED-1 |
4 | ![]() |
从 (1) 和 (3) 通过肯定前件 |
5 | ![]() |
公理 PRED-1 |
6 | ![]() |
从 (2) 和 (5) 通过肯定前件 |
7 | ![]() |
从 (6) 和 (4) 通过肯定前件 |
8 | ![]() |
从 (7) 通过普遍化 |
9 | ![]() |
总结 (1) 到 (8) |
10 | ![]() |
从 (9) 通过演绎定理 |
11 | ![]() |
从 (10) 通过演绎定理 |
在这个证明中,DT 应用于步骤 (10),因为被引动到十字转门的右侧(通过 DT)的公式 不包含任何自由变量。DT 也出于同样的原因而应用于步骤 (11)。