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

Question

My attempt

1. $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y))$ [premise]
2. $\forall y.P(y) \implies Q(y)$ [$\land$ elim 1]
3. $\forall x.P(x)$ [$\land$ elim 1]
4. $a, P(a)$ [$\forall$ elim 3]
5. $a, P(a) \implies Q(a)$ [$\forall$ elim 2]
6. $Q(a)$ [$\implies$ elim 4,5]
7. $\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?

Answer 1

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.

Answer 2

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}$$

Answer 3

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: