Natural Deduction Proof without Logical Equivalences

discrete mathematicsformal-proofslogicnatural-deductionpropositional-calculus

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?

Best Answer

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.

Related Question