Existential instantiation

Transformation rules
Propositional calculus
Rules of inference
Implication introduction / elimination (modus ponens) Biconditional introduction / elimination Conjunction introduction / elimination Disjunction introduction / elimination Disjunctive / hypothetical syllogism Constructive / destructive dilemma Absorption / modus tollens / modus ponendo tollens
Rules of replacement
Associativity Commutativity Distributivity Double negation De Morgan's laws Transposition Material implication Exportation Tautology Negation introduction
Predicate logic
Universal generalization / instantiation Existential generalization / instantiation

In predicate logic, existential instantiation (also called existential elimination) is a valid 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 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

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

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

See also

• Existential fallacy