# Natural Deduction Proof without Logical Equivalences

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?

• Notice that there's no need to assume p ∨ q in step 3, you can get p ∨ q by E∧ in 1 Sep 12, 2020 at 20:10
• So by definition $1$ is already true?
– user750949
Sep 12, 2020 at 20:11
• 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 Sep 12, 2020 at 20:15
• 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?
– user750949
Sep 12, 2020 at 20:27
• 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. Sep 12, 2020 at 20:41

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.

• 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$. Sep 12, 2020 at 23:36
• @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. Sep 13, 2020 at 8:01
• Good. I see there is another way to get $\lnot \lnot p$ using the rule of Negation Introduction. 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 }$$

• 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. Sep 12, 2020 at 21:29
• Actually, I can do something that makes everybody happier, instead of deleting something nice: I upvoted your answer. Sep 13, 2020 at 8:03