# 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 restriction that the constant c introduced by the rule must be a new term that has not occurred earlier in the proof.

In one formal notation, the rule may be denoted by

${\displaystyle (\exists x){\mathcal {F}}x::{\mathcal {F}}a,}$

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