Natural Deduction Prove ∀x¬P (x)

Question

$\begin{array}{|l} \forall xP(x) \vee \forall x \neg P(x) \quad premise \\ \exists xQ(x) \rightarrow \neg P(x) \quad premise \\ \forall xQ(x) \quad premise \\\hline \begin{array}{|l} \forall xP(x) \quad assumption \\\hline \vdots \quad \\ \forall x\neg P(x) \quad \end{array} \\\begin{array}{|l} \forall x\neg P(x) \quad assumption \\\hline \end{array} \\ \forall x \neg P(x) \quad \vee elim\\ \end{array}$

Am I on the right path to solving this or how should I be thinking about it? I think I may have strayed from the path in trying to use $\vee$ elim, just didn't see a different path to take.

Answer 1

Hint: you have an existential and a universal in the premises. Assume a witness for the existance and see what happens under the assumption of $\forall x~P(x)$.

$\begin{array}{|l} \forall xP(x) \vee \forall x \neg P(x) \quad premise \\ \exists xQ(x) \rightarrow \neg P(x) \quad premise \\ \forall xQ(x) \quad premise \\\hline \begin{array}{|l} \forall xP(x) \quad assumption\\\hline \begin{array}{|l}[c]~Q(c)\to\neg P(c)\quad assumption\\\hline \vdots \end{array}\\\ldots \qquad existential~elimination \\ \vdots \\ \forall x\neg P(x) \quad \end{array} \\\begin{array}{|l} \forall x\neg P(x) \quad assumption \\\hline \end{array} \\ \forall x \neg P(x) \quad \vee elim\\ \end{array}$

Answer 2

What you did so far is correct, and you only have to fill in the "..."s in your subproofs.

The second subproof is easy: You already got your conclusion $\forall x \neg P(x)$ as an assumption -- just reiterate (R) that line and you're done.

As for the first subproof, the idea is to derive a contradiction between $\neg P(a)$ for some individual $a$ in the second premise -- of which we know there is an instance, since we are given $\forall x Q(x)$ -- and the universal claim $\forall x P(x)$:
Assume $Q(a) \to \neg P(a)$ for an arbitrary individual $a$. By the third premise $\forall x Q(x)$ we know by universal instantiation ($\forall\!$ E) that $Q$ indeed holds of $a$. By modus ponens ($\to\!$ E), we can conclude $\neg P(a)$. But this contradicts the proposition that $P(a)$, which we get out of the assumption $\forall x P(x)$ by $\forall\!$ E, so we get a contradiction $\bot$. From this contradiction we are allowed to conclude anything thanks to ex falso quodlibet ($\bot$) -- conveniently, we can choose $\forall x \neg P(x)$ as the next conclusion. Since we were able to derive this conclusion under the assumption that $Q(a) \to \neg P(a)$ holds for some individual $a$, and by the second premise we know that at least one such individual does exist, we may apply $\exists\!$ E on the existential formula and the subproof, and thereby discharge the assumption $Q(a) \to \neg P(a)$ to conclude $\forall x \neg P(x)$ for sure.