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 = $\backslash exists\; x\; P\; \backslash left(\{x\}\backslash right)\; \backslash implies\; P\; \backslash left(\{a\}\backslash right)$

}}

{{Transformation rules}}

In predicate logic, existential instantiation (also called existential elimination)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}}{{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.}} is a rule of inference which says that, given a formula of the form $(\backslash exists\; x)\; \backslash phi(x)$, one may infer $\backslash phi(c)$ 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 $x$ which is bound to $\backslash exists\; x$ must be uniformly replaced by c. This is implied by the notation $P\backslash left(\{a\}\backslash right)$, but its explicit statement is often left out of explanations.

In one formal notation, the rule may be denoted by

:$\backslash exists\; x\; P\; \backslash left(\{x\}\backslash right)\; \backslash implies\; P\; \backslash left(\{a\}\backslash right)$

where a is a new constant symbol that has not appeared in the proof.