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?
Best Answer
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)$.
\begin{equation} \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^* \end{equation}