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?

Solution 1:

This sort of thing can only be answered by looking at a particular set of inference rules, rather than looking at one inference rule at a time. This is an inherent flaw in the way that Wikipedia covers inference rules, because rules that are sound individually may be unsound when combined, as the deduction in the question shows.

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.

Of course the real test is not whether it appears that problems have been prevented - the test is whether the soundness and completeness theorems can be proved for a particular deductive system. It's easiest to pick one book that has a system that matches your taste, and then stick scrupulously to the system in that book. That avoids all these subtle problems about mismatched inference rules.