Quantifier instantiation rules are the inference rules for introducing and eliminating quantifiers in first-order logic proof systems. Universal instantiation (UI) allows deriving φ[t/x] from ∀x φ (instantiate the universal quantifier with a term t). Existential generalization (EG) allows deriving ∃x φ from φ[t/x] (generalize a specific instance to an existential claim). These rules connect the syntactic manipulation of quantifiers to their semantic meaning and are essential for constructing proofs in first-order logic.
Use natural deduction proofs as examples. Distinguish between free and bound variables carefully. Understand that UI can instantiate with any term (constant or complex), while EG introduces a witness. Work through proofs that use these rules, paying attention to variable capture issues.
You already know the syntax of first-order logic and the structure of natural deduction proofs. Natural deduction handles propositional connectives through introduction and elimination rules: ∧-intro, ∧-elim, →-intro, →-elim, and so on. Quantifiers have analogous rules, but they involve the interplay between syntax (formulas) and the domain (terms), which makes them slightly more delicate.
Universal instantiation (UI), also written ∀-Elimination, says: from ∀x φ(x), derive φ[t/x] for any term t. The intuition is direct: if a property holds for every element, it holds for this particular element (or expression) t. The term t can be any constant symbol, any variable, or any complex term built from function symbols. For example, from ∀x (x + 0 = x) you can derive (a + 0 = a), or (f(b) + 0 = f(b)), or even (0 + 0 = 0). The only constraint is that t must be free for x in φ — substituting t for x must not cause any free variable in t to become accidentally bound inside φ. This is the variable capture condition. In practice, you can always avoid capture by first renaming bound variables in φ.
Existential generalization (EG), also written ∃-Introduction, says: from φ[t/x], derive ∃x φ(x). The intuition is equally direct: if a specific element t has property φ, then something has property φ. From (a + a = 2a), you can derive ∃x (x + x = 2a), or ∃x (a + a = 2x), depending on which occurrence of a you choose to generalize over. Note that you are *introducing* an existential claim from a specific witness — you are weakening, not strengthening.
The complementary rules — ∃-Elimination and ∀-Introduction — handle the reverse directions and require more care. ∃-Elimination says: if you know ∃x φ(x), you can introduce a fresh constant c (a "witness name") and assume φ(c), provided c does not appear anywhere else in the proof. ∀-Introduction says: if you have derived φ(c) for a completely arbitrary constant c (one introduced with no assumptions about it), then you can conclude ∀x φ(x). Together, the four rules form a complete system for reasoning with quantifiers: to prove something about all elements, introduce an arbitrary witness; to use an existential claim, name the witness and reason about it without committing to what it is. Understanding these constraints — when c is "arbitrary enough" for ∀-intro, and when substitution is "safe enough" for UI — is the core technical skill in first-order proof construction.