普遍汎化

普遍汎化（ふへんはんか、テンプレート:Lang-en-short, Universal introduction, GEN）は、述語論理において妥当な推論規則のひとつである。これは、もし$⊢P(x)$が導出されていれば、$⊢\mathrm{\forall }xP(x)$を導出してよい、という意味である。

汎化と仮定

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

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

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

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

証明の例

例題: $\mathrm{\forall }x(P(x)\to Q(x))\to (\mathrm{\forall }xP(x)\to \mathrm{\forall }xQ(x))$は$\mathrm{\forall }x(P(x)\to Q(x))$および$\mathrm{\forall }xP(x)$から導出できる。

証明:

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

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

関連項目

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