1
$\begingroup$

$\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.

$\endgroup$
4
  • $\begingroup$ 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$. $\endgroup$ Commented Sep 25, 2019 at 14:04
  • $\begingroup$ @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. $\endgroup$ Commented Sep 25, 2019 at 14:19
  • $\begingroup$ The second sub-proof is already there : delete the "dots" and it's done. The first one is more tricky... $\endgroup$ Commented Sep 25, 2019 at 14:39
  • $\begingroup$ @MauroALLEGRANZA What would I state as my reasoning to end that proof? $\endgroup$ Commented Sep 25, 2019 at 14:50

2 Answers 2

1
$\begingroup$

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

$\endgroup$
7
  • $\begingroup$ 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 $\endgroup$ Commented Sep 25, 2019 at 17:40
  • $\begingroup$ $\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}$ $\endgroup$ Commented Sep 25, 2019 at 22:58
  • $\begingroup$ No. @AndrewRyan . You cannot use $\forall$ introduction. Use $\forall$ elimination on the assumption to derive a contradiction. From a contradiction you can then derive ... $\endgroup$ Commented Sep 26, 2019 at 1:57
  • $\begingroup$ $\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}$ $\endgroup$ Commented Sep 26, 2019 at 3:43
  • $\begingroup$ where to go from here? How are we going to get to $\forall x \neg P(x)$? $\endgroup$ Commented Sep 26, 2019 at 3:47
0
$\begingroup$

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.

enter image description here

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .