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). 


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

Ad blocker interference detected!

Wikia is a free-to-use site that makes money from advertising. We have a modified experience for viewers using ad blockers

Wikia is not accessible if you’ve made further modifications. Remove the custom ad blocker rule(s) and the page will load as expected.