Show that ${Q(x), \forall y(Q(y) \rightarrow \forall zP(z))} \vdash \forall xP(x)$ 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:


*

*$Q(x)$ (hyp)

*$\forall y(Q(y) \rightarrow \forall zP(z))$ (hyp)

*$\forall y(Q(y) \rightarrow \forall zP(z)) \rightarrow  (Q(x) \rightarrow \forall z P(z)) $ (A3)

*$Q(x) \rightarrow \forall zP(z)$
(by MP 2,3)

*$\forall zP(z)$ (by MP 1,4)

*$\forall zP(z) \rightarrow P(x)$ (A3)

*$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?

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)$.
