普遍化

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

普遍化(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)也是基于类似的理由。