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?


1 Answer 1


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}

  • $\begingroup$ Thanks for the detailed explanation. $\endgroup$
    – NaborDH
    Jan 5, 2019 at 17:18
  • $\begingroup$ @NaborDH - You are welcome! $\endgroup$ Jan 5, 2019 at 19:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.