普遍化
这个限制适用于证明:如果 GEN 在一个证明中应用于一个公式,从而约束了它的自由变量 x,则 DT 不能应用于这个证明中把这个公式移动到十字转门的右侧。
- 如果 ,則 。
"普遍化"可以缩写为GEN,而推理规则可以被总结为相继式
- ,
但是这引起了一个重要的限制:不能应用演绎定理(DT)于它而推导出
- (注意:这个公式是错的)。 这个公式是错的,因为 x 在前提中是一个无约束的实例,在结论中是一个约束的出现,所以如果这个公式是正确的,则它的 x 的自由实例可以被任何常量(域的元素)所替代:
但这是不正确的。比如,如果 P(x) 意味着 "x 是素数" 而域是自然数集合,则
明显不是真的,因为从它和
- ,
"7 是素数",可以通过肯定前件推出
- ,
"所有自然数都是素数",这是个矛盾,所以反证法得出这个公式是错的。
注意 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)。
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.