Editing Universal instantiation (section)

{{Short description|Rule of inference in predicate logic}}
{{Infobox mathematical statement
| name = Universal instantiation
| type = [[Rule of inference]]
| field = [[Predicate logic]]
| statement = 
| symbolic statement = <math>\forall x \, A \Rightarrow A\{x \mapsto t\}</math>
}}
{{Transformation rules}}

In [[predicate logic]], '''universal instantiation'''<ref>{{cite book|author1=Irving M. Copi |author2=Carl Cohen |author3=Kenneth McMahon |title=Introduction to Logic | date = Nov 2010 | isbn=978-0205820375 |publisher=Pearson Education}}{{page needed|date=November 2014}}</ref><ref>Hurley, Patrick. A Concise Introduction to Logic. Wadsworth Pub Co, 2008.</ref><ref>Moore and Parker{{full citation needed|date=November 2014}}</ref> ('''UI'''; also called '''universal specification''' or '''universal elimination''',{{cn|reason=Give a reference for each synonym.|date=June 2022}} and sometimes confused with ''[[Dictum de omni et nullo|dictum de omni]]''){{cn|date=June 2022}} is a [[Validity (logic)|valid]] [[rule of 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 schema]]. It is one of the basic principles used in [[quantification theory]].

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

Formally, the rule as an axiom schema is given as
: <math>\forall x \, A \Rightarrow A\{x \mapsto t\},</math>
for every formula ''A'' and every term ''t'', where <math>A\{x \mapsto t\}</math> is the result of [[substitution (logic)|substituting]] ''t'' for each ''free'' occurrence of ''x'' in ''A''. <math>\, A\{x \mapsto t\}</math> is an '''instance''' of <math>\forall x \, A.</math>

And as a rule of inference it is
:from <math>\vdash \forall x A</math> infer <math>\vdash A \{ x \mapsto t \} .</math>

[[Irving Copi]] noted that universal instantiation "...[[logical consequence|follows from]] variants of rules for '[[natural deduction]]', which were devised independently  by [[Gerhard Gentzen]] and [[Stanisław Jaśkowski]] in 1934."<ref>Copi, Irving M. (1979). ''Symbolic Logic'', 5th edition, Prentice Hall, Upper Saddle River, NJ</ref>