普遍汎化

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

汎化と仮定[編集]

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

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

$\exists z\exists w(z\not =w)$ （仮定）
$\exists w(y\not =w)$ （存在例化）
$y\not =x$ （存在例化）
$\forall x(x\not =x)$ （誤った普遍汎化）

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

証明の例[編集]

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

証明:

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