The constraints of Universal Introduction in logic proofs

Question

I'm having some trouble understanding the constraints on the rule of inference Universal Introduction.

From Wikipedia:

The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. 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$.

(Emphasis mine)

I dont understand why these constraints are correct. I have seen other constraints elsewhere, and those I understand (I think). For example, the universal introduction in Dirk van Dalen's Logic and Structure (4th ed) is:

$${\forall I}\, \frac{\varphi}{\forall x\, \varphi} $$ where the intended restriction is: the variable $x$ may not occur free in any hypothesis on which $\varphi$ depends, i.e. an uncancelled hypothesis in the derivation of $\varphi$.

I understand why this is correct (we learned a similar pair of constraints in class), but according to the constraints described on the Wikipedia article, I dont see why I would not be able to infer the following (obviously this is incorrect) from the set of premises $\Gamma = \{\exists x \varphi(x)\}$

$$ 1.\ \exists x \varphi(x) \quad \quad \quad \quad \quad \quad \quad \quad \text{premise} $$ $$ 2.\ \varphi(y) \quad \quad \text{1, existential elimination} $$ $$ 3.\ \forall x \varphi(x) \quad \text{2, universal introduction} $$

This seems to imply that $\exists x \varphi(x) \vdash \forall x \varphi(x)$, and I dont see how this would violate the conditions on Wikipedia. $y$ has not been mentioned in $\Gamma$, and $x$ does not occur in $\varphi$.

Am I misunderstanding something? Or is the Wikipedia article wrong?

Answer 1

Using existential elimination properly is more nuanced than that.

In natural deduction, existential elimination says that from $\exists x\varphi(x)$ and $\varphi(y)\to\psi$, that you can infer $\psi$, as long as $y$ doesn't exist in $\psi$ or $\exists x\varphi(x)$ or any of your hypotheses.

I believe the reason that Wikipedia is as simplistic as it is is because there are formulas of first-order logic in which existantial elimination (or existential instantiation) as a single step is as simple as it is stated there. For instance, this was the case in Andrew's formulation in To Truth Through Proof.

However, the rule of inference I mention above is also in the system by a different name. (In Andrews, it is called Rule C.) In his system, existential instantiation and Rule C are bookends of choosing a variable and then "releasing" it at the end. In Fitch, by contrast, you choose a variable in an assumption and then release it by $\exists E$, which in practice is a lot less drama in my experience.

Answer 2

You have made an error in your second step. This is one reason I like a certain style that I believe had been introduced by Fitch. I learned it in "Symbolic Logic" by James Thomas. It uses vertical lines alongside of proof steps to keep track of subsidiary assumptions.

The formula in your second step is a subsidiary assumption. Discharging it will give you 'P implies P'. Applying the universal introduction before the discharge will give you

$$\varphi(y) \to (\forall x ( \varphi(x)))$$

after the discharge. But this is just an instance of universal generalization, itself. So, it is true by stipulation of the logical axioms, and, it can take any formula as an antecedent.