Natural Deduction (you cannot use logical equivalences), prove the following:
$$\frac{(p\lor q)\land(r\rightarrow \lnot p), \space q \rightarrow \lnot r}{\therefore \lnot r}$$

So far I have the following:
$1. \space (p\lor q)\land(r\rightarrow \lnot p)\qquad$ Premise.
$2. \space q\rightarrow \lnot r \qquad \qquad \qquad $ Premise.
$\boxed{3. \space p \lor q \qquad \qquad \qquad Assumption. \\ 4. \space r \rightarrow \lnot p \qquad \qquad \space \space \land-eliminatation(3 )}$

Now I don't know where to go. I am lost on what we are trying to prove. How are proposition $1$ and proposition $2$ linked? I know I want to obtain the last statement $\lnot r$, but don't know what to do after $r$.

Am I supposed to find out $p \lor q$ is true by showing $p$ is true, and if $p$ is true then for $r \rightarrow \lnot p$, $r$ has to be false? Then $q$ must be true then $\lnot r$ equals $T$ leading to $\lnot r$? Is this what I should be thinking?

  • 1
    $\begingroup$ Notice that there's no need to assume p ∨ q in step 3, you can get p ∨ q by E∧ in 1 $\endgroup$ Sep 12, 2020 at 20:10
  • $\begingroup$ So by definition $1$ is already true? $\endgroup$
    – user750949
    Sep 12, 2020 at 20:11
  • 2
    $\begingroup$ Yes, and since you have a disjunction it seems natural to assume that the rule of E∨ has to be used in the derivation. Notice that if you can derivate (q) then you can get ¬r with modus pones in the second premise $\endgroup$ Sep 12, 2020 at 20:15
  • $\begingroup$ So my thinking in the second part of my question is right? That I need to prove $p$ is true, and $q$ is true, then show $r$ is false? $\endgroup$
    – user750949
    Sep 12, 2020 at 20:27
  • 3
    $\begingroup$ If you are trying to use natural deduction you should be thinking about what rules are needed in the derivation. As your conlusion is (¬r) you can assume (r) and try to derivate a contradiction (⊥) so that way you can use the rule of "Introduction of ¬" to conclude (¬r). The rules should be specified in the textbook you are reading. $\endgroup$ Sep 12, 2020 at 20:41

2 Answers 2


As correctly said by Mauro curto in his comment, the missing step in your attempt of derivation is the use of the inference rule $\lor \mathbf{E}$ for eliminating the disjunction $p \lor q$.

The idea is that, because of the first premise $(p \lor q) \land (r \to \lnot p)$, the disjunction $p \lor q$ holds but it is unknown if $p$ holds or $q$ holds. In the first case, since $r \to \lnot p$, you can easily infer $\lnot r$ (via modus tollens). In the second case, $\lnot r $ immediately follows because of the second premise.

Therefore, a correct derivation in natural deduction of $\lnot r$ from the premises $(p \lor q) \land (r \to \lnot p)$ and $q \to \lnot r$ is the following:

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $

$ \fitch{1. \, (p \lor q) \land (r \to \lnot p) \qquad \text{premise} \\ 2.\, q \to \lnot r \qquad \text{premise} } { 3. \, p \lor q \ce{(1)} \fitch{4.\, p \qquad \text{assumption}} { 5. \, r \to \lnot p \ce{(1)} \fitch{6. \, r \qquad \text{assumption}} { 7. \, \lnot p \ie{(6, 5)} 8. \, \bot \ne{(7, 4)} } \\ 9. \, \lnot r \ni{(6{-}8)} }\\ \fitch{10.\, q \qquad \text{assumption}} { 11. \, \lnot r \ie{(2, 10)} }\\ 12. \, \lnot r \oe{(3{-}11)} } $

Note that in your attempt of derivation, $p \lor q$ need not be assumed, because it follows from the first premise $(p \lor q) \land (r \to \lnot p)$ by means of the inference rule $\land \mathbf{E}$ for elimination of conjunction.

  • $\begingroup$ No problem. Your explanation is nice. I can delete mine. However, I have a question. You mentioned Modus Tollens rule. Are you assuming the OP has the inference rule $P \vdash \lnot\lnot P$, to derive $\lnot\lnot p$ from $p$ ? Perhaps, I am wrong but I think Modus Tollens is $P \to Q, \lnot Q \vdash \lnot P$. $\endgroup$
    – F. Zer
    Sep 12, 2020 at 23:36
  • $\begingroup$ @F.Zer - Yes, the scheme for modus tollens is $P \to Q, \, \lnot Q \vdash \lnot P$. And $r \to \lnot p, \, p \vdash \lnot r$ can be seen as an instance of that scheme, because $\lnot \lnot p$ can be easily derived from $p$, using the rule $\lnot_\text{intro}$ (you don't need to add an inference rule $p \vdash \lnot \lnot p$). Anyway, my comment was just intended as a hint about how to achieve the goal. In the final derivation, the "modus tollens approach" is actually simplified. $\endgroup$ Sep 13, 2020 at 8:01
  • $\begingroup$ Good. I see there is another way to get $\lnot \lnot p$ using the rule of Negation Introduction. $\endgroup$
    – F. Zer
    Sep 13, 2020 at 10:49

Am I supposed to find out $p \lor q$ is true ...?

As Mauro says in the comments, there is no need to assume $p \lor q$ is true. It is derived from one of your premises using $\land$-Elimination.

As you goal is $\lnot r$, and you can derive (no need to assume) $p \lor q$, if you can get $\lnot r$ assuming $p$ is true and obtain that same statement when assuming $q$, then, with the use of $\lor$-Elimination, you are allowed to write $\lnot r$.

A possible proof skeleton would be: $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $

$ \fitch{ (p\lor q) \lor (r \to \lnot p)\\ q \to \lnot r }{ p \lor q\\ r \to \lnot p\\ \fitch{p}{ \fitch{r}{ \vdots } }\\ \fitch{q}{ \vdots }\\ \lnot r } $

  • $\begingroup$ Oh sorry, I didn't see your answer, I started writing mine before you posted yours. Since they are quite similar, I can delete mine. $\endgroup$ Sep 12, 2020 at 21:29
  • 1
    $\begingroup$ Actually, I can do something that makes everybody happier, instead of deleting something nice: I upvoted your answer. $\endgroup$ Sep 13, 2020 at 8:03

You must log in to answer this question.