# 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:

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?

• Aren't you missing $z$ in $\forall P(z)$ in the header? – Abstraction Aug 22 '16 at 12:55
• Yes, thanks! Edited. – Bruno A Aug 22 '16 at 12:57
• @Magdiragdag: first, derive $(\forall z)P(z)$. Then derive $(\forall x)P(x)$ from that. – Carl Mummert Aug 22 '16 at 13:00
• @Luiz S.: use the generalization theorem on page 117 of Enderton. Certainly $(\forall z)P(z) \vdash P(x)$ by axiom A3. Therefore, by the generalization theorem, because $x$ is not free in $(\forall z)P(z)$, we have $(\forall z) P(z) \vdash (\forall x)P(x)$. – Carl Mummert Aug 22 '16 at 13:03
• I think you can put it anywhere, it's a self-contained derivation to show $(\forall z)P(z) \vdash (\forall x)P(x)$. It just takes some reading of the proof of the generalization theorem to see how to write that derivation. – Carl Mummert Aug 22 '16 at 13:08

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