Natural deduction proof of $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y)) \vdash \forall z.Q(z)$ My attempt


*

*$(\forall x.P(x))\land(\forall y.P(y) \implies Q(y))$ [premise]

*$\forall y.P(y) \implies Q(y)$ [$\land$ elim 1]

*$\forall x.P(x)$ [$\land$ elim 1]

*$a, P(a)$ [$\forall$ elim 3]

*$a, P(a) \implies Q(a)$ [$\forall$ elim 2]

*$Q(a)$ [$\implies$ elim 4,5]

*$\forall z.Q(z)$


I feel steps 4-5 is not correct, because we used a for two different expressions. I'm also not so sure about whether it's okay to go from step 6-7. Could anyone tell me whether what I did is correct and if not how I should fix it?
 A: You can eliminate any universal with any term you wabnt, so there is no need to introduce $a$ on line 4 or 5.
However, you do need to introduce the $a$ in order to set up the Universal Introduction rule. That is, you need to basically say: "let $a$ be an arbitrary object.  By $\forall x P(x)$ it follows that $P(a)$, and by $\forall y (P(y) \rightarrow Q(y))$ it follows that $P(A) \rightarrow Q(a)$. Hence, we have $Q(a)$. But since $a$ was arbitrary, it follows that $\forall z Q(z)$"
I don't know how exactly that proof formalizes in whatever system you are using, but here is one done in Fitch:

A: I would justify your steps 4 and 5 with "universal instantiation" and write down that $a$ in step 5 is the same $a$ as in step 4.  (If step 2 is true for all $y$, then it is certainly true with the assignment $y = a$ for the same $a$ as in step 4.)  Then step 6 is modus ponens on steps 5 and 4.  (Not everything is elimination.)  Then step 7 is universal generalization applied to 6.
But otherwise, this seems fine.
A: The universal elimination ($\forall\textsf {Elim}$) steps are that : If the statement $S(w)$ holds for any entity $w$ of the domain, then $S(a)$ holds for an arbitrary value $a$ of the domain. $$\forall w~S(w)~\vdash~ S(a)$$
The universal introduction ($\forall\textsf{Intro}$) step is likewise that : If the statement $S(a)$ holds for an arbitrary value $a$ of the domain, then $S(z)$ holds for all values $z$ of the domain. 
$$S(a)~\vdash~\forall z~S(z)$$
The key criteria is that you must not violate the arbitrary nature of the free variable $a$ between assumption(s) and discharge.   However, it is fine to for two universal eliminations to assume the same arbitrary value; and there is not any problem with the bound variables using different tokens.   All steps are okay.

$$\dfrac{\dfrac{\dfrac{\dfrac{\forall x~P(x)~\wedge~\forall y~(P(y)\to Q(y))}{\forall y~(P(y)\to Q(y))}{\wedge\textsf E}}{P(a)\to Q(a)}{\forall\textsf E,a}\quad\dfrac{\dfrac{\forall x~P(x)~\wedge~\forall y~(P(y)\to Q(y))}{\forall x~P(x)}{\wedge\textsf E}}{P(a)}{\forall\textsf E,a}\quad}{Q(a)}{{\to}\textsf E,a}}{\forall z~Q(z)}{\forall\textsf I,\not a}$$
