# Restrictions on universal generalization

Wikipedia's article on universal generalization doesn't seem to give a satisfactory explanation of the restrictions on when it can be used:

Assume $\Gamma$ is a set of formulas, $\varphi$ a formula, and $\Gamma \vdash \varphi(y)$ has been derived. The generalization rule states that $\Gamma \vdash \forall x \varphi(x)$ can be derived if $y$ is not mentioned in $\Gamma$ and $x$ does not occur in $\varphi$.

The article then gives an example of UG being used incorrectly to derive $\exists z\exists w(z\neq w) \vdash \forall x(x\neq x)$, with the restrictions given certainly being violated. However, wouldn't the following modification of the "proof" be in accordance with the restrictions?

$\exists z\exists w(z\neq w)$

$\exists w(y\neq w)$

$y\neq x$

$\forall\alpha(\alpha\neq x)$

$x\neq x$

Here, the generalization in step 4 has been amended to use $\alpha$ as the quantifier's bound variable, which should be permitted, as $\alpha$ does not occur in $y\neq x$ and $y$ does not occur in the assumption $\exists z\exists w(z\neq w)$, yet this leads to a universal instantiation that is clearly false! Is the $\Gamma$ of the restrictions meant to be all previous steps of the proof, not just the assumptions? If so, wouldn't this invalidate the proof given further in the article that includes the steps $P(y)\to Q(y)$ and $P(y)$ before generalizing $Q(y)$? Does the presence of existential instantiation place further restrictions on universal generalization somehow, with the existential instantiated counting as a mention of the variable introduced?

-
I've belatedly realized that this is just a self-contained duplicate of math.stackexchange.com/questions/43941 –  jwodder Apr 16 '12 at 3:01
Here is how the problem in the question is resolved in Mendelson's logic textbook, which does use a Hilbert-style deductive system. Recall that the deduction of $\phi(c)$ from $(\exists x)\phi(x)$, as in the first two steps of the deduction in the question, is called existential instantiation. In Mendelson's system, this is not formalized as an inference rule, it is treated as a definitional extension of the original theory, in which a new constant symbol $c$ is added along with a new axiom $\phi(c)$. Now Mendelson's version of universal generalization is just that from $\phi$ we can deduce $(\forall x)\phi$ for any variable $x$. Thus there is no way to go from step 3 to step 4 of the deduction above, because Mendelson's universal generalization rule does not have the ability to replace the constant symbol $y$ with a variable $\alpha$ in the formula that is having a quantifier adjoined. In this way Mendelson is able to avoid any restrictions on the variable in the universal generalization rule.
In a different deductive system where the universal generalization rule does have the ability to replace constant symbols with variables, you're right that extra restrictions will have to be added if the constant symbols can be added by existential instantiation. For example, if we take as a convention that any constant symbol introduced by existential instantiation has been mentioned in $\Gamma$, that would also prevent this sort of problem.