查看“︁普遍化”︁的源代码

普遍化（'''generalization'''）是[[數理邏輯]]裡一條極為常用的規則，直觀來說，這條規則在滿足一條件下，可以將原[[合式公式]]推廣成被[[全称量化]]的版本。

== 視為元定理 ==
{{main|一阶逻辑#普遍化元定理}}在[[谓词演算]]裡，以下的[[元定理]]{{math_theorem
| name = 元定理
| math_statement = 在 <math>\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n</math> 裡變數 <math>x</math> 都完全被約束，若

: <math>\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n\vdash\mathcal{B}</math>

則有

: <math>\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n\vdash(\forall x)\mathcal{B}</math>
}}
就是一般所稱的'''普遍化'''。

== 視為推理規則 ==
'''普遍化'''可以視為[[谓词演算]]的一條[[推理规则]]，也就是說：（ 以下的 <math>x</math> 為任意變數，<math>\mathcal{A}</math> 為任意[[合式公式]]）
: <math> \mathcal{A} </math>可以推出 <math> \forall x \mathcal{A} </math>。
也可以用[[相继式]]表記為
: <math> \mathcal{A}\vdash \forall x \mathcal{A} </math>
但這個推理規則會嚴苛地限制[[演绎定理]]的適用範圍，如
: <math> \vdash P(x) \Rightarrow \forall x P(x)</math>
'''不成立'''，因为無法確定變數 ''<math> x </math>'' 在<math> P(x) </math>有沒有完全被約束（參見上面[[普遍化#視為元定理|元定理]]一節）。這就破壞了[[元語言]]的＂十字旋轉門＂「 <math> \vdash</math>」跟[[逻辑语言]]的「<math> \Rightarrow</math>」間的聯繫。也就是說，直觀上「 以[[合式公式|合式公式<math> \mathcal{A} </math>]]為前提，根據推理規則和[[公理]]可以推出[[合式公式|合式公式<math> \mathcal{B} </math>]]」跟「根據推理規則和[[公理]]可以推出[[合式公式|合式公式<math> \mathcal{A}\Rightarrow\mathcal{B} </math>]]」是等價的，但將普遍化視為推理規則就不免打破這個直觀聯繫。

==证明的例子==
以下的證明是基於'''將普遍化視為推理規則''' 。

<math> \vdash \forall x [P(x) \Rightarrow Q(x)] \Rightarrow [\forall x P(x) \Rightarrow \forall x Q(x)] </math>

'''证明：'''
{| class="wikitable"
! style="background:#93D7AE;"| 编号
! style="background:#93D7AE;"| 公式
! style="background:#93D7AE;"| 理由
|-
| 1
| <math> \forall x [P(x) \Rightarrow Q(x)] </math>
| 假设
|-
| 2
| <math> \forall x P(x) </math>
| 假设
|-
| 3
| <math> \forall x [P(x) \Rightarrow Q(x)] \Rightarrow [P(x) \Rightarrow Q(x)]  </math>
| 公理 PRED-1
|-
| 4
| <math> P(x) \Rightarrow Q(x) </math>
| 从 (1) 和 (3) 通过[[肯定前件]]
|-
| 5
| <math> \forall x P(x) \Rightarrow P(x) </math>
| 公理 PRED-1
|-
| 6
| <math> P(x) \ </math> 
| 从 (2) 和 (5) 通过肯定前件
|-
| 7
| <math> Q(x) \ </math>
| 从 (6) 和 (4) 通过肯定前件
|-
| 8
| <math> \forall x Q(x) </math>
| 从 (7) 通过'''普遍化'''
|-
| 9
| <math> \forall x [P(x) \Rightarrow Q(x)],\, \forall x P(x) \vdash \forall x Q(x) </math>
| 总结 (1) 到 (8)
|-
| 10
| <math> \forall x [P(x) \Rightarrow Q(x)] \vdash \forall x P(x) \Rightarrow \forall x Q(x) </math>
| 从 (9) 通过演绎定理
|-
| 11
| <math> \vdash \forall x [P(x) \Rightarrow Q(x)] \Rightarrow [\forall x P(x) \Rightarrow \forall x Q(x)] </math>
| 从 (10) 通过演绎定理
|}

步骤(10)中，因为 <math> \forall x P(x) </math> 裡''<math> x </math>''完全被約束，所以可以套用演繹定裡，步骤(11)也是基於類似的理由。

[[Category:數理邏輯|P]]
[[Category:推理规则]]