Universal generalization

Template:Rules of inference In mathematical logic, generalization (also universal generalization, GEN) is an inference rule of predicate calculus. It states that if $\vdash P(x)$ has been derived, then $\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 Γ is a set of formulas, φ a formula, and $\Gamma \vdash \phi (y)$ has been derived. The generalization rule states that $\Gamma \vdash \forall x\phi (x)$ can be derived if y is not mentioned in Γ and x does not occur in φ.

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

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

This purports to show that $\exists z\exists w(z\not =w)\vdash \forall x(x\not =x),$ which is an unsound deduction.

Example of a proof

Prove: $\forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))$.

Proof:

Number	Formula	Justification
1	$\forall x\,(P(x)\rightarrow Q(x))$	Hypothesis
2	$\forall x\,P(x)$	Hypothesis
3	$(\forall x\,(P(x)\rightarrow Q(x)))\rightarrow (P(y)\rightarrow Q(y)))$	Axiom PRED-1
4	$P(y)\rightarrow Q(y)$	From (1) and (3) by Modus Ponens
5	$(\forall x\,P(x))\rightarrow P(y)$	Axiom PRED-1
6	$P(y)\$	From (2) and (5) by Modus Ponens
7	$Q(y)\$	From (6) and (4) by Modus Ponens
8	$\forall x\,Q(x)$	From (7) by Generalization
9	$\forall x\,(P(x)\rightarrow Q(x)),\forall x\,P(x)\vdash \forall x\,Q(x)$	Summary of (1) through (8)
10	$\forall x\,(P(x)\rightarrow Q(x))\vdash \forall x\,P(x)\rightarrow \forall x\,Q(x)$	From (9) by Deduction Theorem
11	$\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, the deduction theorem was applicable in steps 10 and 11 because the formulas being moved have no free variables.

See also

• Categorical imperative redirected from "Generalization in Ethics"
• Derivative (generalizations)
• First-order logic
• Hasty generalization
• Generalization error
• Generalizations of Fibonacci numbers
• Generalizations of Pauli matrices
• Universal instantiation