Existential instantiation

Summary

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