Quantifier Generalization Rules
The Instantiation Rules take us from quantified propositions to instantiated propositions. The Generalization Rules go the other way: They allow us to infer quantified propostions from instantiations. In parallel to our instantiation rules we have one "easy" rule, a rule with no restrictions, and a "hard" rule - a rule with a flagging restriction.
Let's start with the easy rule. Suppose that my 1965 Mercury Comet, "Blue Bell" is fast. I can translate this fact as a singular sentence, "Fa". Can I generalize this with a quantifier? Well it certainly does not follow that everything is fast. But it does follow that something is fast, since Blue Bell is something. So I can generalize as follows:
| 1. | Fa | premise |
| 2. | (∃x)Fx | E.G., 1 |
"E.G." is existential generalization, and the rule is:
| Existential Generalization | |
| Fa | |
| (∃x)Fx |
There are no restrictions on the use of this rule.
How do we universally generalize? We just pointed out that we can't generalize from a single instance to a universally quantified proposition, so how can we infer a universal generalization in a derivation? We can univerally generalize from an instantiation, provided that the instantiation we are generalizing from is an arbitrary instantiation, and not one that plays a role in other lines of the proof. To carry this idea out in an actual derivation, we begin by instantiating the propositional form we want to universally generalize, as a flagged subproof. We introduce a flagged subproof for universal generalization with a flagging assumption: We choose an individual constant that is new to the derivation, and flag it. Then we proceed until we derive the instantiated wff we wish to universally generalize from. Here's an example:
| 1. | (x)(Hx ⊃ Gx) | premise | |
| 2. | (x)Hx | premise | |
| 3. | flag a | flagging assump. UG | SP1 |
| 4. | Ha ⊃ Ga | UI, 1 | SP1 |
| 5. | Ha | UI, 2 | SP1 |
| 6. | Ga | MP, 4, 5 | SP1 |
| 7. | (x)Gx | UG, 3-6 |
We derived the singular sentence "Ga" and then used Universal Generalization in order to derive "(x)Gx". But to do that we had to isolate "a" in a flagged subproof. Here's the rule:
| flag a | SP, UG | Universal
Generalization restriction: requires flagged subproof |
| Fa | ||
| (x)Fx |
Our flagging restriction is the same as the flagging restriction for Existential Instantiation. A flagged constant in a subproof for Universal Generalization must be new to the proof. It can't appear in any other lines of the proof. The flagging assumption is discharged when we use the rule Universal Generalization in the last line of the subproof.
 |
 |