普遍化
普遍化(generalization)是数理逻辑里一条极为常用的规则,直观来说,这条规则在满足一条件下,可以将原合式公式推广成被全称量化的版本。
视为元定理
元定理 — 在 里变数 都完全被约束,若
则有
就是一般所称的普遍化。
视为推理规则
普遍化可以视为谓词演算的一条推理规则,也就是说:( 以下的 为任意变数, 为任意合式公式)
- 可以推出 。
也可以用相继式表记为
但这个推理规则会严苛地限制演绎定理的适用范围,如
不成立,因为无法确定变数 在 有没有完全被约束(参见上面元定理一节)。这就破坏了元语言的"十字旋转门"“ ”跟逻辑语言的“ ”间的联系。也就是说,直观上“ 以合式公式 为前提,根据推理规则和公理可以推出合式公式 ”跟“根据推理规则和公理可以推出合式公式 ”是等价的,但将普遍化视为推理规则就不免打破这个直观联系。
证明的例子
以下的证明是基于将普遍化视为推理规则 。
证明:
编号 | 公式 | 理由 |
---|---|---|
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) 通过演绎定理 |
步骤(10)中,因为 里 完全被约束,所以可以套用演绎定里,步骤(11)也是基于类似的理由。