| Universal generalization | |
| Type: | Rule of inference |
| Field: | Predicate logic |
| Statement: | Suppose P p P |
| Symbolic Statement: | \vdashP(x) \vdash\forallxP(x) |
In predicate logic, generalization (also universal generalization, universal introduction,[1] [2] [3] GEN, UG) is a valid inference rule. It states that if
\vdashP(x)
\vdash\forallxP(x)
The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume
\Gamma
\varphi
\Gamma\vdash\varphi(y)
\Gamma\vdash\forallx\varphi(x)
y
\Gamma
x
\varphi
These restrictions are necessary for soundness. Without the first restriction, one could conclude
\forallxP(x)
P(y)
\existsz\existsw(z\not=w)
\existsw(y\not=w)
y\not=x
\forallx(x\not=x)
This purports to show that
\existsz\existsw(z\not=w)\vdash\forallx(x\not=x),
\Gamma\vdash\forally\varphi(y)
y
\Gamma
\varphi(y)
Prove:
\forallx(P(x) → Q(x)) → (\forallxP(x) → \forallxQ(x))
\forallx(P(x) → Q(x))
\forallxP(x)
Proof:
| Step | Formula | Justification | |
|---|---|---|---|
| 1 | \forallx(P(x) → Q(x)) | Hypothesis | |
| 2 | \forallxP(x) | Hypothesis | |
| 3 | (\forallx(P(x) → Q(x))) → (P(y) → Q(y)) | From (1) by Universal instantiation | |
| 4 | P(y) → Q(y) | From (1) and (3) by Modus ponens | |
| 5 | (\forallxP(x)) → P(y) | From (2) by Universal instantiation | |
| 6 | P(y) | From (2) and (5) by Modus ponens | |
| 7 | Q(y) | From (6) and (4) by Modus ponens | |
| 8 | \forallxQ(x) | From (7) by Generalization | |
| 9 | \forallx(P(x) → Q(x)),\forallxP(x)\vdash\forallxQ(x) | Summary of (1) through (8) | |
| 10 | \forallx(P(x) → Q(x))\vdash\forallxP(x) → \forallxQ(x) | From (9) by Deduction theorem | |
| 11 | \vdash\forallx(P(x) → Q(x)) → (\forallxP(x) → \forallxQ(x)) | 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.