普遍汎化

普遍汎化（ふへんはんか、英: Universal generalization, Universal introduction,^[1][2][3] GEN）は、述語論理において妥当な推論規則のひとつである。これは、もし${\displaystyle \vdash P(x)}$が導出されていれば、${\displaystyle \vdash \forall x\,P(x)}$を導出してよい、という意味である。

汎化と仮定

十分な汎化規則のもとでは${\displaystyle \vdash }$記号の左側に仮定を置くことができるが、制限もある。Γは論理式の集合であり、${\displaystyle \varphi }$は論理式であり、${\displaystyle \Gamma \vdash \varphi (y)}$は導出されていると仮定する。汎化規則では、yがΓに言及されておらず、xが${\displaystyle \varphi }$に現れない場合、${\displaystyle \Gamma \vdash \forall x\varphi (x)}$が導かれる、とする。

これらの制限は健全性を保つために必要である。最初の制限がなければ、仮定${\displaystyle P(y)}$から${\displaystyle \forall xP(x)}$を結論づけることができてしまう。また2番目の制約がなければ、次のような演繹を行うことができてしまう。

1. ${\displaystyle \exists z\exists w(z\not =w)}$ （仮定）
2. ${\displaystyle \exists w(y\not =w)}$ （存在例化）
3. ${\displaystyle y\not =x}$ （存在例化）
4. ${\displaystyle \forall x(x\not =x)}$ （誤った普遍汎化）

これは、${\displaystyle \exists z\exists w(z\not =w)\vdash \forall x(x\not =x)}$が不健全な演繹であると示すことを目的としている。

証明の例

例題: ${\displaystyle \forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))}$は${\displaystyle \forall x\,(P(x)\rightarrow Q(x))}$および${\displaystyle \forall x\,P(x)}$から導出できる。

証明:

番号	式	正当化
1	${\displaystyle \forall x\,(P(x)\rightarrow Q(x))}$	仮定
2	${\displaystyle \forall x\,P(x)}$	仮定
3	${\displaystyle (\forall x\,(P(x)\rightarrow Q(x)))\rightarrow (P(y)\rightarrow Q(y)))}$	普遍例化
4	${\displaystyle P(y)\rightarrow Q(y)}$	(1)(3)と前件肯定
5	${\displaystyle (\forall x\,P(x))\rightarrow P(y)}$	普遍例化
6	${\displaystyle P(y)\ }$	(2)(5)と前件肯定
7	${\displaystyle Q(y)\ }$	(6)(4)と前件肯定
8	${\displaystyle \forall x\,Q(x)}$	(7)と普遍汎化
9	${\displaystyle \forall x\,(P(x)\rightarrow Q(x)),\forall x\,P(x)\vdash \forall x\,Q(x)}$	(1)から(8)のまとめ
10	${\displaystyle \forall x\,(P(x)\rightarrow Q(x))\vdash \forall x\,P(x)\rightarrow \forall x\,Q(x)}$	(9)と演繹定理
11	${\displaystyle \vdash \forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))}$	(10)と演繹定理

この証明では、普遍汎化がステップ8で使用されている。移行された式に自由変項がないため、ステップ10と11では演繹定理が適用できた。

関連項目

• 一階述語論理
• 早まった一般化
• 普遍例化