In predicate logic, generalization (also universal generalization, universal introduction,[1][2][3] GEN, UG) is a valid inference rule.

The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions.

is a set of formulas,

φ

⊢ φ ( y )

The generalization rule states that

φ ( x )

φ

These restrictions are necessary for soundness.

Without the first restriction, one could conclude

Without the second restriction, one could make the following deduction: This purports to show that

which is an unsound deduction.

φ ( y )

(the second restriction need not apply, as the semantic structure of

is not being changed by the substitution of any variables).

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.