Template:Short description Template:More footnotes Template:Infobox mathematical statement Template:Transformation rules
In predicate logic, generalization (also universal generalization, universal introduction,<ref>Copi and Cohen</ref><ref>Hurley</ref><ref>Moore and Parker</ref> GEN, UG) is a valid inference rule. It states that if <math>\vdash \!P(x)</math> has been derived, then <math>\vdash \!\forall x \, P(x)</math> can be derived.
Generalization with hypothesesEdit
The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume <math>\Gamma</math> is a set of formulas, <math>\varphi</math> a formula, and <math>\Gamma \vdash \varphi(y)</math> has been derived. The generalization rule states that <math>\Gamma \vdash \forall x \, \varphi(x)</math> can be derived if <math>y</math> is not mentioned in <math>\Gamma</math> and <math>x</math> does not occur in <math>\varphi</math>.
These restrictions are necessary for soundness. Without the first restriction, one could conclude <math>\forall x P(x)</math> from the hypothesis <math>P(y)</math>. Without the second restriction, one could make the following deduction:
- <math>\exists z \, \exists w \, ( z \not = w) </math> (Hypothesis)
- <math>\exists w \, (y \not = w) </math> (Existential instantiation)
- <math>y \not = x</math> (Existential instantiation)
- <math>\forall x \, (x \not = x)</math> (Faulty universal generalization)
This purports to show that <math>\exists z \, \exists w \, ( z \not = w) \vdash \forall x \, (x \not = x),</math> which is an unsound deduction. Note that <math>\Gamma \vdash \forall y \, \varphi(y)</math> is permissible if <math>y</math> is not mentioned in <math>\Gamma</math> (the second restriction need not apply, as the semantic structure of <math>\varphi(y)</math> is not being changed by the substitution of any variables).
Example of a proofEdit
Prove: <math> \forall x \, (P(x) \rightarrow Q(x)) \rightarrow (\forall x \, P(x) \rightarrow \forall x \, Q(x)) </math> is derivable from <math> \forall x \, (P(x) \rightarrow Q(x)) </math> and <math> \forall x \, P(x) </math>.
Proof:
| Step | Formula | Justification |
|---|---|---|
| 1 | <math> \forall x \, (P(x) \rightarrow Q(x)) </math> | Hypothesis |
| 2 | <math> \forall x \, P(x) </math> | Hypothesis |
| 3 | <math> (\forall x \, (P(x) \rightarrow Q(x))) \rightarrow (P(y) \rightarrow Q(y)) </math> | From (1) by Universal instantiation |
| 4 | <math> P(y) \rightarrow Q(y) </math> | From (1) and (3) by Modus ponens |
| 5 | <math> (\forall x \, P(x)) \rightarrow P(y) </math> | From (2) by Universal instantiation |
| 6 | <math> P(y) \ </math> | From (2) and (5) by Modus ponens |
| 7 | <math> Q(y) \ </math> | From (6) and (4) by Modus ponens |
| 8 | <math> \forall x \, Q(x) </math> | From (7) by Generalization |
| 9 | <math> \forall x \, (P(x) \rightarrow Q(x)), \forall x \, P(x) \vdash \forall x \, Q(x) </math> | Summary of (1) through (8) |
| 10 | <math> \forall x \, (P(x) \rightarrow Q(x)) \vdash \forall x \, P(x) \rightarrow \forall x \, Q(x) </math> | From (9) by Deduction theorem |
| 11 | <math> \vdash \forall x \, (P(x) \rightarrow Q(x)) \rightarrow (\forall x \, P(x) \rightarrow \forall x \, Q(x)) </math> | 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.