Editing Universal generalization (section)

==Generalization with hypotheses==
The full generalization rule allows for hypotheses to the left of the [[turnstile (symbol)|turnstile]], but with restrictions. Assume <math>\Gamma</math> is a set of formulas, <math>\varphi</math> a formula, and <math>\Gamma \vdash \varphi(y)</math> has been derived. The generalization rule states that <math>\Gamma \vdash \forall x \, \varphi(x)</math> can be derived if <math>y</math> is not mentioned in <math>\Gamma</math> and <math>x</math> does not occur in <math>\varphi</math>. 

These restrictions are necessary for soundness. Without the first restriction, one could conclude <math>\forall x P(x)</math> from the hypothesis <math>P(y)</math>. Without the second restriction, one could make the following deduction:
#<math>\exists z \, \exists w \, ( z \not = w) </math> (Hypothesis)
#<math>\exists w \, (y \not = w) </math> (Existential instantiation)
#<math>y \not = x</math> (Existential instantiation)
#<math>\forall x \, (x \not = x)</math> (Faulty universal generalization)

This purports to show that <math>\exists z \, \exists w \, ( z \not = w) \vdash \forall x \, (x \not = x),</math> which is an unsound deduction. Note that <math>\Gamma \vdash \forall y \, \varphi(y)</math> is permissible if <math>y</math> is not mentioned in <math>\Gamma</math> (the second restriction need not apply, as the semantic structure of <math>\varphi(y)</math> is not being changed by the substitution of any variables).