普遍化(generalization)是數理邏輯裡一條極為常用的規則,直觀來說,這條規則在滿足一條件下,可以將原合式公式推廣成被全称量化的版本。
視為元定理
在谓词演算裡,以下的元定理{{math_theorem
| name = 元定理
| math_statement = 在 \mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n 裡變數 x 都完全被約束,若
: \mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n\vdash\mathcal{B}
則有
: \mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n\vdash(\forall x)\mathcal{B}
}}
就是一般所稱的普遍化。
視為推理規則
普遍化可以視為谓词演算的一條推理规则,也就是說:( 以下的 x 為任意變數,\mathcal{A} 為任意合式公式)
: \mathcal{A} 可以推出 \forall x \mathcal{A} 。
也可以用相继式表記為
: \mathcal{A}\vdash \forall x \mathcal{A}
但這個推理規則會嚴苛地限制演绎定理的適用範圍,如
: \vdash P(x) \Rightarrow \forall x P(x)
不成立,因为無法確定變數 x 在 P(x) 有沒有完全被約束(參見上面元定理一節)。這就破壞了元語言的"十字旋轉門"「 \vdash」跟逻辑语言的「 \Rightarrow」間的聯繫。也就是說,直觀上「 以合式公式 \mathcal{A} 為前提,根據推理規則和公理可以推出合式公式 \mathcal{B} 」跟「根據推理規則和公理可以推出合式公式 \mathcal{A}\Rightarrow\mathcal{B} 」是等價的,但將普遍化視為推理規則就不免打破這個直觀聯繫。
证明的例子
以下的證明是基於將普遍化視為推理規則 。
\vdash \forall x [P(x) \Rightarrow Q(x)] \Rightarrow [\forall x P(x) \Rightarrow \forall x Q(x)]
证明:
步骤(10)中,因为 \forall x P(x) 裡 x 完全被約束,所以可以套用演繹定裡,步骤(11)也是基於類似的理由。
评论 (0)