Editing Universal instantiation

{{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>

== Quine ==
According to [[Willard Van Orman Quine]], universal instantiation and [[existential generalization]] are two aspects of a single principle, for instead of saying that "∀''x''&nbsp;''x''&nbsp;=&nbsp;''x''" implies "Socrates&nbsp;=&nbsp;Socrates", we could as well say that the denial "Socrates&nbsp;≠&nbsp;Socrates" implies "∃''x''&nbsp;''x''&nbsp;≠&nbsp;''x''". The principle embodied in these two operations is the link between [[Quantification (logic)|quantification]]s and the singular statements that are related to them as instances. Yet it is a principle only by courtesy. It holds only in the case where a term names and, furthermore, occurs [[Reference#Semantics|referentially]].<ref>{{cite book |author1=Willard Van Orman Quine |author1-link=Willard Van Orman Quine|author2=Roger F. Gibson |title=Quintessence  |contribution= V.24. Reference and Modality |location=Cambridge, Mass |publisher=Belknap Press of Harvard University Press |year=2008 |oclc=728954096}} Here: p.&nbsp;366.</ref>

==See also==
*[[Existential instantiation]] 
*[[Existential quantification]]

==References==
{{Reflist}}

[[Category:Rules of inference]]
[[Category:Predicate logic]]