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