existential instantiation

{{logic}} ''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}})).