Show that ${Q(x), \forall y(Q(y) \rightarrow \forall zP(z))} \vdash \forall xP(x)$

Question

List of axioms:

$(A1)$ - All Tautologies.

$(A2)$ - $(\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)) $.

$(A3)$ - $(\forall x \alpha) \rightarrow [\alpha]^{t}_{x} $ if x is free for t in $\alpha$.

$(A4)$ - $\alpha \rightarrow (\forall x \alpha) $ if x is not free in $\alpha $.

$(A5)$ - $ x = x$

$(A6)$ - $(x=y) \rightarrow (\alpha \rightarrow \beta)$ if $\beta$ if obtained by substitution of at least one occurrence of x free for y in $\alpha$.

Modus Ponens as inference rule.

And Generalization Theorem:

If $\Gamma \vdash \phi$ and x do not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \phi$

My attempt:

1. $Q(x)$ (hyp)
2. $\forall y(Q(y) \rightarrow \forall zP(z))$ (hyp)
3. $\forall y(Q(y) \rightarrow \forall zP(z)) \rightarrow (Q(x) \rightarrow \forall z P(z)) $ (A3)
4. $Q(x) \rightarrow \forall zP(z)$ (by MP 2,3)
5. $\forall zP(z)$ (by MP 1,4)
6. $\forall zP(z) \rightarrow P(x)$ (A3)
7. $P(x)$ (by MP 5, 6)

And now, I can't use the Generalization Theorem because x does occur free in $\Gamma$. Should I use another path?

Answer 1

The $x$ in $Q(x)$ is free, but in $\forall x P(x)$ is bound, therefore they are "different things" and you could carry out the derivation, because when a variable is bound it is called "dummy" because it acts merely as a placeholder, therefore it could be substituted by anything else.

To summarize, the issue is due to the fact that you are using the same symbol $x$ to represent two different things, which is fine as long as you understand that difference. In the first case it is representing a free variable, but in the second it is bounded by the quantifier.

So, if you recognize that, for instance, $\forall x P(x)$ is exactly the same thing as $\forall y P(y)$ or $\forall z P(z)$ then there is no problem to use the generalization theorem. So you can, instead of instantiating $\forall z P(z)$ to $P(x)$, instantiate it to any variable that you like (different from $x$ obviously) and then generalize it to $\forall x P(x)$.