- Universal instantiation
In
logic universal instantiation (UI, sometimes confused with Dictum de omni) is aninference 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 aquantification rule for theuniversal quantifier but it can also be encoded in an axiom. It is one of the basic principles used inquantification theory .Example: "All dogs are mammals. Fido is a dog. Therefore Fido is a mammal."
In symbols the rule as an
axiom schema is:
for some term "a" and where is the result of substituting "a" for all free occurrences of "x" in "A".
And as a
rule of inference it isfrom ⊢ ∀"x" "A" infer ⊢ "A"("a"/"x"),
with "A"("a"/"x") the same as above.
Irving Copi noted that universal instantiation "...follows from variants of rules for 'natural deduction ', which were devised independently byGerhard Gentzen andStanislaw Jaskowski in 1934." -pg. 71. Symbolic Logic; 5th ed.
Wikimedia Foundation. 2010.