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