Existential instantiation

In predicate logic, existential instantiation (also called existential elimination)[1][2][3] is a valid rule of inference which says that, given a formula of the form ${\displaystyle (\exists x)\phi (x)}$, one may infer ${\displaystyle \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.

In one formal notation, the rule may be denoted by

${\displaystyle \exists xP\left({x}\right)\implies P\left({\mathbf {a} }\right)}$

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

See also

• Existential fallacy
• Universal instantiation
• List of rules of inference

References

1. Hurley, Patrick. A Concise Introduction to Logic. Wadsworth Pub Co, 2008.
2. Copi and Cohen
3. Moore and Parker