Universal generalization

Generalization with hypotheses

The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume Γ is a set of formulas, φ a formula, and Γ ⊢ φ ( y ) has been derived. The generalization rule states that Γ ⊢ ∀ x φ ( x ) can be derived if y is not mentioned in Γ and x does not occur in φ .

These restrictions are necessary for soundness. Without the first restriction, one could conclude ∀ x P ( x ) from the hypothesis P ( y ) . Without the second restriction, one could make the following deduction:

1. ∃ z ∃ w ( z ≠ w ) (Hypothesis)
2. ∃ w ( y ≠ w ) (Existential instantiation)
3. y ≠ x (Existential instantiation)
4. ∀ x ( x ≠ x ) (Faulty universal generalization)

This purports to show that ∃ z ∃ w ( z ≠ w ) ⊢ ∀ x ( x ≠ x ) , which is an unsound deduction.

Example of a proof

Prove: ∀ x ( P ( x ) → Q ( x ) ) → ( ∀ x P ( x ) → ∀ x Q ( x ) ) is derivable from ∀ x ( P ( x ) → Q ( x ) ) and ∀ x P ( x ) .

Proof:

In this proof, Universal generalization was used in step 8. The Deduction theorem was applicable in steps 10 and 11 because the formulas being moved have no free variables.