普遍的な一般化

述語論理において、一般化（普遍一般化、普遍導入、^{[ 1 ] [ 2 ] [ 3 ]} GEN、UGとも呼ばれる）は有効な推論規則である。それは、もし${\displaystyle \vdash \!P(x)}$導出された後、${\displaystyle \vdash \!\forall x\,P(x)}$導出できる。

完全な一般化ルールは、改札口の左側の仮説を許容するが、制約がある。${\displaystyle \Gamma }$これは一連の数式です。${\displaystyle \varphi }$数式、そして${\displaystyle \Gamma \vdash \varphi (y)}$が導出された。一般化規則は次のように述べている。${\displaystyle \Gamma \vdash \forall x\,\varphi (x)}$導出できる場合${\displaystyle y}$は言及されていません${\displaystyle \Gamma }$そして${\displaystyle x}$発生しない${\displaystyle \varphi }$。

これらの制約は健全性のために必要である。最初の制約がなければ、結論は${\displaystyle \forall xP(x)}$仮説から${\displaystyle P(y)}$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 \Gamma \vdash \forall y\,\varphi (y)}$許容されるのは${\displaystyle y}$は言及されていません${\displaystyle \Gamma }$（2 番目の制限は適用する必要はありません。意味構造は${\displaystyle \varphi (y)}$（変数の置換によって変更されることはありません）。

証明する：${\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)}$。

証拠：

この証明では、ステップ8で普遍一般化が用いられた。ステップ10と11では、移動される式に自由変数がないため、演繹定理が適用可能であった。

• 一階述語論理
• 早まった一般化
• 普遍的なインスタンス化
• 存在論的一般化