普遍汎化のソースを表示

{{推論規則}}

'''普遍汎化'''（ふへんはんか、{{Lang-en-short|Universal generalization}}, '''Universal introduction''',<ref>Copi and Cohen</ref><ref>Hurley</ref><ref>Moore and Parker</ref> '''GEN'''）は、[[述語論理]]において妥当な[[推論規則]]のひとつである。これは、もし<math>\vdash P(x)</math>が導出されていれば、<math>\vdash \forall x \, P(x)</math>を導出してよい、という意味である。

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

これらの制限は健全性を保つために必要である。最初の制限がなければ、仮定<math>P(y)</math>から<math>\forall x P(x)</math>を結論づけることができてしまう。また2番目の制約がなければ、次のような演繹を行うことができてしまう。
#<math>\exists z \exists w ( z \not = w) </math> （仮定）
#<math>\exists w (y \not = w) </math> （[[存在例化]]）
#<math>y \not = x</math> （[[存在例化]]）
#<math>\forall x (x \not = x)</math> （誤った普遍汎化）
これは、<math>\exists z \exists w ( z \not = w) \vdash \forall x (x \not = x)</math>が不健全な演繹であると示すことを目的としている。

== 証明の例 ==
'''例題:''' <math>\forall x \, (P(x) \rightarrow Q(x)) \rightarrow (\forall x \, P(x) \rightarrow \forall x \, Q(x))</math>は<math> \forall x \, (P(x) \rightarrow Q(x)) </math>および<math> \forall x \, P(x) </math>から導出できる。

'''証明:'''
{| border="1" cellpadding="3"
! 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(y) \rightarrow Q(y)))  </math>
| [[普遍例化]]
|-
| 4
| <math> P(y) \rightarrow Q(y) </math>
| (1)(3)と[[モーダスポネンス|前件肯定]]
|-
| 5
| <math> (\forall x \, P(x)) \rightarrow P(y) </math>
| 普遍例化
|-
| 6
| <math> P(y) \ </math>
| (2)(5)と前件肯定
|-
| 7
| <math> Q(y) \ </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)と演繹定理
|}
この証明では、普遍汎化がステップ8で使用されている。移行された式に自由変項がないため、ステップ10と11では演繹定理が適用できた。

== 関連項目 ==
* [[一階述語論理]]
* [[早まった一般化]]
* [[普遍例化]]

== 脚注 ==
{{reflist}}

{{DEFAULTSORT:ふへんはんか}}
[[Category:推論規則]]
[[Category:述語論理]]
[[Category:数学に関する記事]]