普遍化

在谓词演算里，以下的元定理

就是一般所称的普遍化。

普遍化可以视为谓词演算的一条推理规则，也就是说：（ 以下的 ${\displaystyle x}$ 为任意变量，${\displaystyle {\mathcal {A}}}$ 为任意合式公式）

${\displaystyle {\mathcal {A}}}$可以推出 ${\displaystyle \forall x{\mathcal {A}}}$。

也可以用相继式表记为

${\displaystyle {\mathcal {A}}\vdash \forall x{\mathcal {A}}}$

但这个推理规则会严苛地限制演绎定理的适用范围，如

${\displaystyle \vdash P(x)\Rightarrow \forall xP(x)}$

不成立，因为无法确定变量 ${\displaystyle x}$ 在${\displaystyle P(x)}$有没有完全被约束（参见上面元定理一节）。这就破坏了元语言的＂十字旋转门＂「 ${\displaystyle \vdash }$」跟逻辑语言的「${\displaystyle \Rightarrow }$」间的联系。也就是说，直观上「 以合式公式${\displaystyle {\mathcal {A}}}$为前提，根据推理规则和公理可以推出合式公式${\displaystyle {\mathcal {B}}}$」跟「根据推理规则和公理可以推出合式公式${\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {B}}}$」是等价的，但将普遍化视为推理规则就不免打破这个直观联系。

以下的证明是基于将普遍化视为推理规则 。

${\displaystyle \vdash \forall x[P(x)\Rightarrow Q(x)]\Rightarrow [\forall xP(x)\Rightarrow \forall xQ(x)]}$

证明：

编号	公式	理由
1	${\displaystyle \forall x[P(x)\Rightarrow Q(x)]}$	假设
2	${\displaystyle \forall xP(x)}$	假设
3	${\displaystyle \forall x[P(x)\Rightarrow Q(x)]\Rightarrow [P(x)\Rightarrow Q(x)]}$	公理 PRED-1
4	${\displaystyle P(x)\Rightarrow Q(x)}$	从 (1) 和 (3) 通过肯定前件
5	${\displaystyle \forall xP(x)\Rightarrow P(x)}$	公理 PRED-1
6	${\displaystyle P(x)\ }$	从 (2) 和 (5) 通过肯定前件
7	${\displaystyle Q(x)\ }$	从 (6) 和 (4) 通过肯定前件
8	${\displaystyle \forall xQ(x)}$	从 (7) 通过普遍化
9	${\displaystyle \forall x[P(x)\Rightarrow Q(x)],\,\forall xP(x)\vdash \forall xQ(x)}$	总结 (1) 到 (8)
10	${\displaystyle \forall x[P(x)\Rightarrow Q(x)]\vdash \forall xP(x)\Rightarrow \forall xQ(x)}$	从 (9) 通过演绎定理
11	${\displaystyle \vdash \forall x[P(x)\Rightarrow Q(x)]\Rightarrow [\forall xP(x)\Rightarrow \forall xQ(x)]}$	从 (10) 通过演绎定理

步骤(10)中，因为 ${\displaystyle \forall xP(x)}$ 里${\displaystyle x}$完全被约束，所以可以套用演绎定里，步骤(11)也是基于类似的理由。