Universal instantiation

Encyclopedia : U : UN : UNI : Universal instantiation

In logic Universal instantiation (UI) is an inference from a truth about each member of a class of individuals to the truth about a particular individual of that class. It is generally given as a quantification rule for the universal quantifier but it can also be encoded in an axiom. It is one of the basic principles used in quantification theory.

Example: "All dogs are mammals. Therefore Fido is a mammal."

In symbols the rule as an axiom schema is:

∀xA → A(a/x), for some term a and where A(a/x) is the result of substituting a for all free occurrences of x in A.

And as a rule of inference it is:

from ⊢ ∀xA infer ⊢ A(a/x), with A(a/x) the same as above.

From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.