# Proof using natural deduction (Tautology)

I've been asked to prove the following tautology via natural deduction:

$$\forall x \, (\lnot Px \lor Qx) \rightarrow (\forall y \, Py \rightarrow \forall z \,Qz)$$

I normally use tree proofs, but I don't think I can show those here so I'll say in words what I've done so far.

First, I assume $$\forall x (\lnot Px \lor Qx)$$ to deduce $$\lnot Pd \lor Qd$$ from $$\forall x \, (\lnot Px \lor Qx)$$.

Secondly, I assume $$\forall y \, Py$$ and $$\lnot Pd$$ to deduce $$(\forall y \, Py \rightarrow \forall \, z Qz)$$ from $$\lnot Pd$$.

Thirdly, I assume $$Qd$$ and am trying to deduce $$(\forall y \, Py \rightarrow \forall z \, Qz)$$ from $$Qd$$.

If I can make this third deduction I can use OR-elimination to get the conclusion, but I don't see how I can deduce $$(\forall y \, Py \rightarrow \forall z \, Qz)$$ from $$Qd$$.

Is there a way to make this third deduction or did I just start my whole proof wrong?

To deduce $$\forall y Py \to \forall z Qz$$ from $$Qd$$, you should deduce $$\forall z Q z$$ from the assumption $$Qd$$, but this is impossible because of the restriction on the free variable for the rule $$\forall_i$$ (see here for a discussion of the issue).
Thus, the right approach is to apply the rule $$\lor_e$$ in order to deduce $$Qd$$ without any assumption on $$d$$ (i.e. $$Qd$$ should be discharged), in this way you can correctly apply the rule $$\forall_i$$ to deduce $$\forall z Q z$$. Concretely, the following is a derivation in natural deduction of $$\forall x(\lnot Px \lor Qx) \to (\forall y Py \to \forall z Qz)$$.
$$$$\dfrac{\dfrac{[\forall x (\lnot Px \lor Qx)]^\circ}{\lnot Pz \lor Qz}\forall_e \qquad \dfrac{\dfrac{[\lnot Pz]^* \qquad \dfrac{[\forall y Py]^\bullet}{Pz}\forall_e}{\bot}\lnot_e}{Qz}\text{efq} \qquad [Qz]^*}{\dfrac{Qz}{\dfrac{\forall z Qz}{\dfrac{\forall y Py \to \forall z Qz}{\forall x (\lnot Px \lor Qx) \to (\forall y \to \forall z Qz)}\to_i^\circ}\to_i^\bullet}\forall_i} \lor_e^*$$$$