In predicate logic, generalization (also universal generalization or universal introduction,[1][2][3] GEN) 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. Contents 1 Generalization with hypotheses 2 Example of a proof 3 See also 4 References Generalization with hypotheses[edit] The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume Γ 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 xvarphi (x) can be derived if y is not mentioned in Γ and 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 zexists w(znot =w) (Hypothesis) ∃ w ( y ≠ w ) displaystyle exists w(ynot =w) (Existential instantiation) y ≠ x displaystyle ynot =x (Existential instantiation) ∀ x ( x ≠ x ) displaystyle forall x(xnot =x) (Faulty universal generalization) This purports to show that ∃ z ∃ w ( z ≠ w ) ⊢ ∀ x ( x ≠ x ) , displaystyle exists zexists w(znot =w)vdash forall x(xnot =x), which is an unsound deduction. Example of a proof[edit] 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: Number 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))) 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) 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,
First-order logic Hasty generalization Universal instantiation References[edit] ^ Copi and Cohen ^ Hurley ^ Moor |