Universal generalization is a rule of inference for predicate logic. It states that if we can derive a formula with free variables then me may infer a formula in which those variables are bound with a universal quantifier, or symbolically: where is a metavariable representing a wff and is a term representing all occurances of in .