Existential instantiation

Transformation rules
Propositional calculus
Rules of inference
Modus ponens / Modus tollens Biconditional introduction / elimination Conjunction introduction / Simplification Disjunction introduction / elimination Disjunctive / Hypothetical syllogism Constructive / Destructive dilemma Absorption 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)^[1]^[2]^[3] 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 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

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

where a is an arbitrary term that has not been a part of our proof thus far.

References

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

Existential instantiation

See also

References