universal generalization

In predicate logic, generalization (also universal generalization, universal introduction,Moore and Parker GEN, UG) is a valid inference rule. 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 $\Gamma$ is a set of formulas, $\varphi$ a formula, and $\Gamma \vdash \varphi(y)$ has been derived. The generalization rule states that $\Gamma \vdash \forall x \, \varphi(x)$ can be derived if $y$ is not mentioned in $\Gamma$ and $x$ does not occur in $\varphi$.

These restrictions are necessary for soundness. Without the first restriction, one could conclude $\forall x P(x)$ from the hypothesis $P(y)$. Without the second restriction, one could make the following deduction:
#$\exists z \, \exists w \, ( z \not = w)$ (Hypothesis)
#$\exists w \, (y \not = w)$ (Existential instantiation)
#$y \not = x$ (Existential instantiation)
#$\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. Note that $\Gamma \vdash \forall y \, \varphi(y)$ is permissible if $y$ is not mentioned in $\Gamma$ (the second restriction need not apply, as the semantic structure of $\varphi(y)$ is not being changed by the substitution of any variables).

Example of a proof

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

See also

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

References

{{DEFAULTSORT:Generalization (Logic)
Rules of inference
Predicate logic