Quantifier Instantiation Rules
Think back to our treatment of the semantics of QL. To determine validity we interpreted quantified wffs and instantiated them in order to then apply our truth-functional truth-tree rules to them. In proofs the strategy is much the same. When we come across a quantified proposition in a derivation, we can either apply our Quantifier Negation Rules, or we can apply instantiation rules.
There are two instantiation rules, one for each quantifier.
Existential Instantiation: Suppose someone is happy. Then it follows that an individual, who we can refer to with an individual constant, e.g. "a", is happy. Thus:
| 1. | (∃x)Hx | premise |
| 2. | Ha | E.I., 1, flag "a" |
From the existential proposition on line 1, I infer the instantiation, in this case a singular proposition, by E.I., "Existential Instantiation." Note, however, that there is an additional item on the justification for E.I., and that is what we will call a flagging restriction. Remember when we instantiated existential propositions in truth-trees that we used individual constants that did not already appear on the tree. That insured that we didn't make the mistake of using the same constant to instantiate two different existential propositions. The same care must be taken here. When we existentially instantiate, we must flag the instantiated constant, and adhere to the restriction that flagged constants must be new to the derivation. They may not appear in any earlier line to the line in which they are introduced.
So our rule is:
| Existential
Instantiation
restriction: flag "a" |
|
| (∃x)Fx | |
| Fa |
Universal Instantiation: For this rule we begin with a universally quantified wff, and we infer the instantiation of that wff. Here we can choose any individual constant, and there is no flagging restriction. The reason for the lack of restriction is that if everything has a property, then each individual in the universe of discourse has it.
| Universal
Instantiation
|
|
| (x)Fx | |
| Fa |
Try the Instantiation Rule Exercise.
 |
 |