Definition: A rule of inference that introduces existential quantifiers.  The symbol for an existential quantifier is (∃x).

More about the term: The existential quantifier indicates that there is at least one thing in a categorical reference.  Instantiation is an operation that removes a quantifier and replaces every variable bound by the quantifier with that same instantial letter.  There are eight rules of inference to derive a conclusion of an argument via deduction:

1. Modus Ponens: p ⊃ q … p… .:q
2. Modus Tollens: p ⊃ q … ~q … .: ~p
3. Pure Hypothetical Syllogism: p ⊃ q … q ⊃ r … .: p ⊃ r
4. Disjunctive Syllogism: p v q … ~q … .:p
5. Constructive Dilemma: (p ⊃ q) & (r ⊃ s) … p v r … .: q v s
6. Simplification: p & q… .: p
7. Conjunction: p … q … .: p & q
8. Addition: p … .: p v q

As long as an existential quantifier is attached to a line of argument the above actions cannot be done.

Example of use: All professors are college graduates.  Some professors are logicians.  Therefore, some logicians are college graduates.

1. (x) (Px ⊃ Cx)
2. (∃x) (Px & Lx)
3. .: (∃x) (Lx & Cx)

This is how we can get to this conclusion by removing the universal and existential quantifiers (let’s let x become m for Max).

1. (x) (Px ⊃ Cx)
2. (∃x) (Px & Lx)
3. Pm & Lm          2, EI
4. Pm ⊃ Cm         1, UI
5. Pm                   3, Simp
6. Cm                  4, 5, MP
7. Lm & Pm          3, Commutativity (not discussed here but you can see how it works)
8. Lm                  7, Simp
9. Lm & Cm        8, Conj
10. (∃x) (Lx & Cx)  9, EG

For more on logic and existential instantiation see any edition of Patrick Hurley’s Introduction to Logic.