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.

  • 1
    $\begingroup$ Please don't ask us to reinvent the wheel. Tell us what do you have so far so we can identify your issue. $\endgroup$ – Graham Kemp Feb 12 '16 at 0:10

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


    $\neg ( r \imp p )$.

    If $r$:

      If $\neg p$:

        $\neg p \land r$.

        $q \lor s$.

        If $\neg s$:

          If $\neg q$:

            If $q$:


            If $s$:



          $\neg \neg q$.


        $\neg s \imp q$.

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


      $\neg \neg p$.


    $r \imp p$.


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

  • $\begingroup$ These are all valid answers. And I thank you very much for the detailed effort. But what I'm not able to inform you, is that, the problem is forcing me to use only the following rules: $\endgroup$ – ex.nihil Feb 14 '16 at 19:10
  • $\begingroup$ Sorry I got logged out for some reason. These are all valid answers. And I thank you very much for the detailed effort. But what I'm not able to inform you, is that, the problem is forcing me to use only the following rules: AND introduction/elimination. OR introduction/elimination. NOT introduction/elimination. IMPLIES introduction/elimination. CONTRADICTION introduction/elimination. So using equivalencies such as $p \rightarrow q \equiv \neg p \lor q$ is not allowed. I appreciate the answers, and I will validate these. $\endgroup$ – ex.nihil Feb 14 '16 at 19:19
  • $\begingroup$ @ex.nihil: Did you read my answer before commenting? I didn't use any equivalences. Also, don't assume that everyone knows exactly what your rules are, because there are about as many variants of natural deduction as there are authors. However, it should be quite trivial to translate between variants. $\endgroup$ – user21820 Feb 15 '16 at 2:53
  • $\begingroup$ Of course I have, and it looked very similar to my attempt only shorter (which is what I was looking for). Your answer is 100% valid, but like you said it's a different variant. The way I understood your answer is by translating it to the variant I was working with. And as for the method of analytic tableaux, it made me understand the order of the assumptions you took, while non-intuitive, got there concisely. What I sometimes do with long expressions is I work backwards in a sort of "Reverse Mathematics" kind of way. I start with the conclusion and work my way back to the premises. $\endgroup$ – ex.nihil Feb 15 '16 at 11:08
  • $\begingroup$ @ex.nihil: Right. The tableaux method also shows that for propositional logic you should not have to use each piece of the desired theorem more than a few times (I think twice at most). To get the shortest proof you have to work both forward and backward. The reason for my comment is that in your second comment you said "using equivalences is not allowed" as if implying my answer did so. Also, I do not see why you accepted Brian's answer instead of mine since he didn't answer the question (especially given your complaint about equivalences) while I did! $\endgroup$ – user21820 Feb 15 '16 at 11:30

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

  • $\begingroup$ Thanks for the attempt. But my question was WITHOUT using simple equivalences. This was the question formalized. I reached a few minutes ago to a result. I'll post the answer to the question. Thanks everyone. $\endgroup$ – ex.nihil Feb 12 '16 at 0:34
  • $\begingroup$ So eliminate those yourself — that's the easy part, That's what's had you stumped for over 3 weeks?!? Can't deduce $\neg B\to A$ from $A\lor B$ ? I hope that's not the case. Inserting them would just make the answer long-winded. I wasn't using "shorter equivalent formulas". Good luck. $\endgroup$ – BrianO Feb 12 '16 at 0:55
  • $\begingroup$ That WAS the case. See now I agree with you this is a really easy and dull problem IF you can deduce an IMPLIES from OR. But for some reason the formulation of the problem insists that we only stick to 5 natural deduction rules of inference (Introduction/Elimination for AND, OR, IMPLIES, NOT, CONTRADICTION). It's merely a matter of limiting your comfort with what you can use. What solved this is using the same assumption way too many times along the proof to get where we want. And yes, this took me 3 weeks (not really, on/off work), merely because the proof is gigantic. Many thanks BrianO. $\endgroup$ – ex.nihil Feb 12 '16 at 12:08
  • $\begingroup$ Then my sympathies & also congratulations. Problems like this build character, they say ;) $\endgroup$ – BrianO Feb 12 '16 at 12:11
  • $\begingroup$ @ex.nihil: Actually it's not that hard, but it takes practice to get used to natural deduction. If you've learnt the tableaux method (en.wikipedia.org/wiki/Method_of_analytic_tableaux) you'll notice that the steps in natural deduction correspond quite closely to the choices made in the tableaux method. $\endgroup$ – user21820 Feb 13 '16 at 11:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.