Natural deduction proof / Formal proof : Complicated conclusion with no premise

Question

Find a formal proof for the following:

$\vdash [(\neg p \land r)\rightarrow (q \lor s )]\longrightarrow[(r\rightarrow p)\lor(\neg s \rightarrow q)]$

As you can see. No premise to use. We have to use assumptions and eliminate them.

This also means no using equivalent formulas. Because we can easily end the problem by finding a shorter and equivalent formula.

But the problem here specifically asks for a natural deduction/formal proof. I'm always arriving at the conclusion but my problem is I always have ONE non-eliminated assumption left.

Answer 1

General Strategy

Break down what you need to prove according to the introduction rule. This is always possible for conjunction and implication. For a disjunction "$A \lor B$", it may not be possible because sometimes you can prove neither "$A$" nor "$B$", in which case you need to go by contradiction, which is to assume $\neg ( A \lor B )$ and obtain a contradiction, from which you can obtain $\neg \neg ( A \lor B )$ without any assumption and then use double negation elimination. Under the assumption, you still want to prove something of the form "$A \lor B$" but this time it is possible. First assume $A$ and obtain a trivial contradiction. So you can conclude $\neg A$ and proceed.

Solution (Fitch-style natural deduction) $\def\imp{\rightarrow}$

If $( \neg p \land r ) \imp ( q \lor s )$:

  If $\neg ( ( r \imp p ) \lor ( \neg s \imp q ) )$:

    If $r \imp p$:

      $( r \imp p ) \lor ( \neg s \imp q )$.

      Contradiction.

    $\neg ( r \imp p )$.

    If $r$:

      If $\neg p$:

        $\neg p \land r$.

        $q \lor s$.

        If $\neg s$:

          If $\neg q$:

            If $q$:

              Contradiction.

            If $s$:

              Contradiction.

            Contradiction.

          $\neg \neg q$.

          $q$.

        $\neg s \imp q$.

        $( r \imp p ) \lor ( \neg s \imp q )$.

        Contradiction.

      $\neg \neg p$.

      $p$.

    $r \imp p$.

    Contradiction.

  $\neg \neg ( ( r \imp p ) \lor ( \neg s \imp q ) )$.

  $( r \imp p ) \lor ( \neg s \imp q )$.

$( ( \neg p \land r ) \imp ( q \lor s ) ) \imp ( ( r \imp p ) \lor ( \neg s \imp q ) )$.

Answer 2

Here's how to do it, not in full gory detail — three of the steps below appeal to simple equivalences; each has to be expanded to establish the particular case of the cited equivalence:

$$ \begin{array}{r|ll} \text{step} & \text{Formula} & \text{How obtained} \\ \hline 1 & (\neg p \land r)\to (q \lor s ) & \text{assumption} \\ 2 & \neg(r\to p) & \text{assumption} \\ 3 & \neg s & \text{assumption} \\ 4 & r \land \neg p & \text{From 2.: $\neg(A\to B) \equiv (A\land \neg B)$} \\ 5 & \neg p \land r & \text{From 4.} \\ 6 & q\lor s & \text{From 5. and 1. by MP} \\ 7 & \neg s\to q & \text{From 6.: $(A\lor B)\equiv (\neg B\to A)$} \\ 8 & q & \text{From 3. and 7. by MP} \\ 9 & \neg s \to q& \text{From 3. and 8. — discharge 3.} \\ 10 & \neg(r\to p)\to (\neg s \to q) & \text{From 2. and 9. — discharge 2.} \\ 11 & (r\to p)\lor (\neg s \to q) & \text{From 10.: $(\neg A\to B)\equiv (A\lor B)$} \\ 12 & [(\neg p \land r)\to (q \lor s )] \longrightarrow [(r\to p)\lor (\neg s \to q)] & \text{From 1. and 11. — discharge 1.} \end{array}$$

The steps that use equivalences $(\phi\equiv\psi)$ — 4., 7. and 11. — are shorthand for a sequence of multiple steps which deduce $\psi$ from $\phi$.