What is "existential instantiation"

n. (context logic English) ''In predicate logic'', an inference rule of the form ∃''x P''(''x'') ⊢ ''P''(''c''), where ''c'' is a new symbol (not part of the original domain of discourse, but which can stand for an element of it (as in (w Skolem normal form Skolemization))).

In predicate logic, existential instantiation (also called existential elimination) is a valid rule of inference which says that, given a formula of the form (∃x)ϕ(x), one may infer ϕ(c) for a new constant or variable symbol c. The rule has the restriction that the constant or variable 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

(∃x)Fx :  : Fa, 
where a is an arbitrary term that has not been a part of our proof thus far.