In predicate logic, generalization (also universal generalization, universal introduction, GEN, UG) is a valid inference rule. It states that if ⊢ P ( x ) {\displaystyle \vdash \!P(x)} has been derived, then ⊢ ∀ x P ( x ) {\displaystyle \vdash \!\forall x\,P(x)} can be derived.
Generalization with hypotheses
The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume Γ {\displaystyle \Gamma } is a set of formulas, φ {\displaystyle \varphi } a formula, and Γ ⊢ φ ( y ) {\displaystyle \Gamma \vdash \varphi (y)} has been derived. The generalization rule states that Γ ⊢ ∀ x φ ( x ) {\displaystyle \Gamma \vdash \forall x\,\varphi (x)} can be derived if y {\displaystyle y} is not mentioned in Γ {\displaystyle \Gamma } and x {\displaystyle x} does not occur in φ {\displaystyle \varphi } .
These restrictions are necessary for soundness. Without the first restriction, one could conclude ∀ x P ( x ) {\displaystyle \forall xP(x)} from the hypothesis P ( y ) {\displaystyle P(y)} . Without the second restriction, one could make the following deduction:
- ∃ z ∃ w ( z ≠ w ) {\displaystyle \exists z\,\exists w\,(z\not =w)} (Hypothesis)
- ∃ w ( y ≠ w ) {\displaystyle \exists w\,(y\not =w)} (Existential instantiation)
- y ≠ x {\displaystyle y\not =x} (Existential instantiation)
- ∀ x ( x ≠ x ) {\displaystyle \forall x\,(x\not =x)} (Faulty universal generalization)
This purports to show that ∃ z ∃ w ( z ≠ w ) ⊢ ∀ x ( x ≠ x ) , {\displaystyle \exists z\,\exists w\,(z\not =w)\vdash \forall x\,(x\not =x),} which is an unsound deduction. Note that Γ ⊢ ∀ y φ ( y ) {\displaystyle \Gamma \vdash \forall y\,\varphi (y)} is permissible if y {\displaystyle y} is not mentioned in Γ {\displaystyle \Gamma } (the second restriction need not apply, as the semantic structure of φ ( y ) {\displaystyle \varphi (y)} is not being changed by the substitution of any variables).
Example of a proof
Prove: ∀ 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))} is derivable from ∀ x ( P ( x ) → Q ( x ) ) {\displaystyle \forall x\,(P(x)\rightarrow Q(x))} and ∀ x P ( x ) {\displaystyle \forall x\,P(x)} .
Proof:
| Step | Formula | Justification |
|---|---|---|
| 1 | ∀ x ( P ( x ) → Q ( x ) ) {\displaystyle \forall x\,(P(x)\rightarrow Q(x))} | Hypothesis |
| 2 | ∀ x P ( x ) {\displaystyle \forall x\,P(x)} | Hypothesis |
| 3 | ( ∀ x ( P ( x ) → Q ( x ) ) ) → ( P ( y ) → Q ( y ) ) {\displaystyle (\forall x\,(P(x)\rightarrow Q(x)))\rightarrow (P(y)\rightarrow Q(y))} | From (1) by Universal instantiation |
| 4 | P ( y ) → Q ( y ) {\displaystyle P(y)\rightarrow Q(y)} | From (1) and (3) by Modus ponens |
| 5 | ( ∀ x P ( x ) ) → P ( y ) {\displaystyle (\forall x\,P(x))\rightarrow P(y)} | From (2) by Universal instantiation |
| 6 | P ( y ) {\displaystyle P(y)\ } | From (2) and (5) by Modus ponens |
| 7 | Q ( y ) {\displaystyle Q(y)\ } | From (6) and (4) by Modus ponens |
| 8 | ∀ x Q ( x ) {\displaystyle \forall x\,Q(x)} | From (7) by Generalization |
| 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)} | Summary of (1) through (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)} | From (9) by Deduction theorem |
| 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))} | From (10) by Deduction theorem |
In this proof, universal generalization was used in step 8. The deduction theorem was applicable in steps 10 and 11 because the formulas being moved have no free variables.