## FANDOM

174 Pages

Universal instantiation is a rule of inference for several predicate logics that allows one to substitute any term for a variable bound with the universal quantifier, while removing the quantifier. In symbols:

$\forall x \phi (x) \vdash \phi (t/x)$

where $t$ is any term (such as a variable, function symbol, or a constant).

## RestrictionsEdit

• The term that replaces the variable must not get quantified after subsitution.