普遍汎化 （ふへんはんか、英 : Universal generalization , Universal introduction ,[1] [2] [3] GEN ）は、述語論理 において妥当な推論規則 のひとつである。これは、もし ⊢ P ( x ) {\displaystyle \vdash P(x)} ⊢ ∀ x P ( x ) {\displaystyle \vdash \forall x\,P(x)}
一般化と仮定 十分な汎化規則のもとでは ⊢ {\displaystyle \vdash } φ {\displaystyle \varphi } Γ ⊢ φ ( y ) {\displaystyle \Gamma \vdash \varphi (y)} y がΓに言及されておらず、y が φ {\displaystyle \varphi } Γ ⊢ ∀ x φ ( x ) {\displaystyle \Gamma \vdash \forall x\varphi (x)}
これらの制限は健全性を保つために必要である。最初の制限がなければ、仮定 P ( y ) {\displaystyle P(y)} ∀ x P ( x ) {\displaystyle \forall xP(x)}
∃ z ∃ w ( z ≠ w ) {\displaystyle \exists z\exists w(z\not =w)} ∃ w ( y ≠ w ) {\displaystyle \exists w(y\not =w)} 存在例化 ） y ≠ x {\displaystyle y\not =x} 存在例化 ） ∀ x ( x ≠ x ) {\displaystyle \forall x(x\not =x)} これは、 ∃ z ∃ w ( z ≠ w ) ⊢ ∀ x ( x ≠ x ) {\displaystyle \exists z\exists w(z\not =w)\vdash \forall x(x\not =x)}
証明の例 例題: ∀ x ( P ( x ) → Q ( x ) ) → ( ∀ x P ( x ) → ∀ x Q ( x ) ) {\displaystyle \forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))} ∀ x ( P ( x ) → Q ( x ) ) {\displaystyle \forall x\,(P(x)\rightarrow Q(x))} ∀ x P ( x ) {\displaystyle \forall x\,P(x)}
証明:
番号 式 正当化 1 ∀ x ( P ( x ) → Q ( x ) ) {\displaystyle \forall x\,(P(x)\rightarrow Q(x))} 仮定 2 ∀ x P ( x ) {\displaystyle \forall x\,P(x)} 仮定 3 ( ∀ x ( P ( x ) → Q ( x ) ) ) → ( P ( y ) → Q ( y ) ) ) {\displaystyle (\forall x\,(P(x)\rightarrow Q(x)))\rightarrow (P(y)\rightarrow Q(y)))} 普遍例化 4 P ( y ) → Q ( y ) {\displaystyle P(y)\rightarrow Q(y)} (1)(3)と前件肯定 5 ( ∀ x P ( x ) ) → P ( y ) {\displaystyle (\forall x\,P(x))\rightarrow P(y)} 普遍例化 6 P ( y ) {\displaystyle P(y)\ } (2)(5)と前件肯定 7 Q ( y ) {\displaystyle Q(y)\ } (6)(4)と前件肯定 8 ∀ x Q ( x ) {\displaystyle \forall x\,Q(x)} (7)と普遍汎化 9 ∀ x ( P ( x ) → Q ( x ) ) , ∀ x P ( x ) ⊢ ∀ x Q ( x ) {\displaystyle \forall x\,(P(x)\rightarrow Q(x)),\forall x\,P(x)\vdash \forall x\,Q(x)} (1)から(8)のまとめ 10 ∀ x ( P ( x ) → Q ( x ) ) ⊢ ∀ x P ( x ) → ∀ x Q ( x ) {\displaystyle \forall x\,(P(x)\rightarrow Q(x))\vdash \forall x\,P(x)\rightarrow \forall x\,Q(x)} (9)と演繹定理 11 ⊢ ∀ x ( P ( x ) → Q ( x ) ) → ( ∀ x P ( x ) → ∀ x Q ( x ) ) {\displaystyle \vdash \forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))} (10)と演繹定理
この証明では、普遍汎化がステップ8で使用されている。移行された式に自由変項がないため、ステップ10と11では演繹定理が適用できた。
関連項目 脚注 ^ Copi and Cohen ^ Hurley ^ Moore and Parker 
カテゴリ:推論規則
