Universal generalization

In predicate logic, generalization (also universal generalization, universal introduction,^{[1] [2] [3]} GEN, UG) is a valid inference rule. It states that if ${\displaystyle \vdash \!P(x)}${\displaystyle \vdash \!P(x)} has been derived, then ${\displaystyle \vdash \!\forall x,円P(x)}${\displaystyle \vdash \!\forall x,円P(x)} can be derived.

The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume ${\displaystyle \Gamma }${\displaystyle \Gamma } is a set of formulas, ${\displaystyle \varphi }${\displaystyle \varphi } a formula, and ${\displaystyle \Gamma \vdash \varphi (y)}${\displaystyle \Gamma \vdash \varphi (y)} has been derived. The generalization rule states that ${\displaystyle \Gamma \vdash \forall x,円\varphi (x)}${\displaystyle \Gamma \vdash \forall x,円\varphi (x)} can be derived if ${\displaystyle y}${\displaystyle y} is not mentioned in ${\displaystyle \Gamma }${\displaystyle \Gamma } and ${\displaystyle x}${\displaystyle x} does not occur in ${\displaystyle \varphi }${\displaystyle \varphi }.

These restrictions are necessary for soundness. Without the first restriction, one could conclude ${\displaystyle \forall xP(x)}${\displaystyle \forall xP(x)} from the hypothesis ${\displaystyle P(y)}${\displaystyle P(y)}. Without the second restriction, one could make the following deduction:

1. ${\displaystyle \exists z,円\exists w,円(z\not =w)}${\displaystyle \exists z,円\exists w,円(z\not =w)} (Hypothesis)
2. ${\displaystyle \exists w,円(y\not =w)}${\displaystyle \exists w,円(y\not =w)} (Existential instantiation)
3. ${\displaystyle y\not =x}${\displaystyle y\not =x} (Existential instantiation)
4. ${\displaystyle \forall x,円(x\not =x)}${\displaystyle \forall x,円(x\not =x)} (Faulty universal generalization)

This purports to show that ${\displaystyle \exists z,円\exists w,円(z\not =w)\vdash \forall x,円(x\not =x),}${\displaystyle \exists z,円\exists w,円(z\not =w)\vdash \forall x,円(x\not =x),} which is an unsound deduction. Note that ${\displaystyle \Gamma \vdash \forall y,円\varphi (y)}${\displaystyle \Gamma \vdash \forall y,円\varphi (y)} is permissible if ${\displaystyle y}${\displaystyle y} is not mentioned in ${\displaystyle \Gamma }${\displaystyle \Gamma } (the second restriction need not apply, as the semantic structure of ${\displaystyle \varphi (y)}${\displaystyle \varphi (y)} is not being changed by the substitution of any variables).

Prove: ${\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))\rightarrow (\forall x,円P(x)\rightarrow \forall x,円Q(x))} is derivable from ${\displaystyle \forall x,円(P(x)\rightarrow Q(x))}${\displaystyle \forall x,円(P(x)\rightarrow Q(x))} and ${\displaystyle \forall x,円P(x)}${\displaystyle \forall x,円P(x)}.

Proof:

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.

• First-order logic
• Hasty generalization
• Universal instantiation
• Existential generalization

• Rules of inference
• Predicate logic

• Articles with short description
• Short description is different from Wikidata
• Articles lacking in-text citations from March 2023
• All articles lacking in-text citations