普遍化(generalization)是数理逻辑里一条极为常用的规则,直观来说,这条规则在满足一条件下,可以将原合式公式推广成被全称量化的版本。
在谓词演算里,以下的元定理
元定理 — 在
里变数
都完全被约束,若
![{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash {\mathcal {B}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea27062f6e4954b9861d02cf89cce1bfbe7a5701)
则有
![{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash (\forall x){\mathcal {B}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/35c90ca447043a4885597caa9d7bd42365ab3ab6)
就是一般所称的普遍化。
普遍化可以视为谓词演算的一条推理规则,也就是说:( 以下的
为任意变数,
为任意合式公式)
可以推出
。
也可以用相继式表记为
![{\displaystyle {\mathcal {A}}\vdash \forall x{\mathcal {A}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f8dc6139e06fa20cca8452f4f5890ba8feeae1a3)
但这个推理规则会严苛地限制演绎定理的适用范围,如
![{\displaystyle \vdash P(x)\Rightarrow \forall xP(x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/731c60ee951b66afc14a97ab4479d75c64d6c92b)
不成立,因为无法确定变数
在
有没有完全被约束(参见上面元定理一节)。这就破坏了元语言的"十字旋转门"“
”跟逻辑语言的“
”间的联系。也就是说,直观上“ 以合式公式
为前提,根据推理规则和公理可以推出合式公式
”跟“根据推理规则和公理可以推出合式公式
”是等价的,但将普遍化视为推理规则就不免打破这个直观联系。
以下的证明是基于将普遍化视为推理规则 。
证明:
编号
|
公式
|
理由
|
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)也是基于类似的理由。