Existential instantiation

{{Short description|Rule of inference in predicate logic}} {{Infobox mathematical statement | name = Existential instantiation | type = Rule of inference | field = Predicate logic | statement = | symbolic statement = <math>\exists x P \left({x}\right) \implies P \left({a}\right)</math> }} {{Transformation rules}}

In predicate logic, '''existential instantiation''' (also called '''existential elimination''')<ref>Hurley, Patrick. ''[https://home.iitk.ac.in/~avrs/PH142/Books/Patrick2012.pdf#page=480 A Concise Introduction to Logic]'' (11th ed.). Wadsworth Pub Co, 2008. Pg. 454. {{ISBN|978-0-8400-3417-5}}</ref><ref>{{Cite book |last=Copi |first=Irving M. |url=https://archive.org/details/studyguideintrod0000mill/mode/2up?q=instantiation |title=Introduction to logic |last2=Cohen |first2=Carl |date=2002 |publisher=Prentice Hall |isbn=978-0-13-033737-5 |edition=11th |location=Upper Saddle River, N.J.}}</ref> is a rule of inference which says that, given a formula of the form <math>(\exists x) \phi(x)</math>, one may infer <math>\phi(c)</math> for a new constant symbol ''c''. The rule has the restrictions that the constant ''c'' introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof. It is also necessary that every instance of <math>x</math> which is bound to <math>\exists x</math> must be uniformly replaced by ''c''. This is implied by the notation <math>P\left({a}\right)</math>, but its explicit statement is often left out of explanations.

In one formal notation, the rule may be denoted by :<math>\exists x P \left({x}\right) \implies P \left({a}\right)</math> where ''a'' is a new constant symbol that has not appeared in the proof.

== References == {{reflist}}

Category:Rules of inference Category:Predicate logic