# Natural Deduction Prove ∀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 \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.

• Correct : you have to use $\lor$-elim on 1st premise : one of the two sub-proof is trivial. For the second one (assumption $\forall Px$) we use also other premises. If all are $P$s and all are $Q$s, all are $P \land Q$s, contradicting the fact taht there is something that is noot $P$ and $Q$. Sep 25, 2019 at 14:04
• @MauroALLEGRANZA So for the first subproof would I have to use a $\rightarrow$ elim and a $\forall$ intro to get the to $\forall x \neg P(x)$ there? For the second subproof I see that it is trivial, but what then would I have to use in order to obtain the result? Since it is already what I am trying to prove. Sep 25, 2019 at 14:19
• The second sub-proof is already there : delete the "dots" and it's done. The first one is more tricky... Sep 25, 2019 at 14:39
• @MauroALLEGRANZA What would I state as my reasoning to end that proof? Sep 25, 2019 at 14:50

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

• Do you mean something more like this? $\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 \quad \\ \forall x\neg P(x) \quad \end{array} \\ \forall x\neg P(x) \quad \exists Elim \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}$ assume witness? Whats that Sep 25, 2019 at 17:40
• $\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) \rightarrow \neg P(c)\quad assumption \\\hline Q(x) \quad\forall Elim ~3 \\\neg P(c) \quad\rightarrow Elim ~5,6 \\(\forall x)\neg P(x)\quad\forall intro ~7\end{array} \\\forall x\neg P(x) \quad\exists Elim ~4-7\end{array} \\\begin{array}{|l} \forall x\neg P(x) \quad assumption\\\hline\end{array} \\\forall x\neg P(x)\quad\vee Elim ~4-9,10\\\end{array}$ Sep 25, 2019 at 22:58
• No. @AndrewRyan . You cannot use $\forall$ introduction. Use $\forall$ elimination on the assumption to derive a contradiction. From a contradiction you can then derive ... Sep 26, 2019 at 1:57
• $\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) \rightarrow \neg P(c)\quad assumption \\\hline Q(x) \quad\forall Elim ~3 \\\neg P(c) \quad\rightarrow Elim ~5,6 \\ P(x) \quad\forall Elim ~4 \\\vdots\end{array} \\\forall x\neg P(x) \quad\exists Elim ~4-7\end{array} \\\begin{array}{|l} \forall x\neg P(x) \quad assumption\\\hline\end{array} \\\forall x\neg P(x)\quad\vee Elim ~4-9,10\\\end{array}$ Sep 26, 2019 at 3:43
• where to go from here? How are we going to get to $\forall x \neg P(x)$? Sep 26, 2019 at 3:47

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. 