The problem is to prove $$P \lor Q, P \rightarrow R \lor S, R \rightarrow W \land Z, Z \land \lnot S \rightarrow \lnot W \vdash \lnot S \rightarrow Q$$ using natural deduction.

I'm studying natural deduction for my upcoming exam in Logic and I have come across this problem. Unfortunately, I cannot seem to find a path to its solution. What I have done is the following and I don't know how to proceed any further:

  1. $P \lor Q$
  2. $P \rightarrow R \lor S$
  3. $R \rightarrow W \land Z$
  4. $Z \land \lnot S \rightarrow \lnot W$
  5. $P \qquad H$
    1. $R \lor S \qquad E \rightarrow 2,5$
    2. $R \qquad H$
      1. $W \land Z \qquad E\rightarrow 3,7$
      2. $W \qquad E\rightarrow 8$
      3. $Z \qquad E\rightarrow 8$

My professor only uses the Fitch notation, so I would appreciate you using it in your answer.

EDIT: Using the suggestions in the answers provided and studying the rules some more, I have come up with this solution. Can you tell me whether it is acceptable?

$1 \quad P \lor Q \\ 2 \quad P \rightarrow R \lor S \\ 3 \quad R \rightarrow W \land Z \\ 4 \quad Z \land \lnot S \rightarrow \lnot W \\ 5 \qquad \lnot S \qquad assumption \\ 6 \qquad \qquad P \qquad assumption \\ 7 \qquad \qquad R \lor S \qquad implication \ elim \ 2,6 \\ 8 \qquad \qquad R \qquad disjunctive \ syll \ 7,5 \\ 9 \qquad \qquad W \land Z \qquad implication \ elim \ 3,8 \\ 10 \qquad \qquad Z \qquad conjunction \ elim \ 9 \\ 11 \qquad \qquad Z \land \lnot S \qquad conjunction \ intro \ 10,5 \\ 12 \qquad \qquad \lnot W \qquad implication \ elim \ 4,11 \\ 13 \qquad \qquad W \qquad conjunction \ elim \ 9 \\ 14 \qquad \qquad false \qquad negation \ elim \ 13,12 \\ 15 \qquad \lnot P \qquad negation \ intro \ 14 \\ 16 \qquad Q \qquad disjunctive \ syll \ 1,15 \\ 17 \quad \lnot S \rightarrow Q \qquad implication \ intro \ 5,16$

  • $\begingroup$ Please make sure the question is stated clearly in the body of your post - the title is not part of the post and may not be read by everyone. $\endgroup$ Sep 4 '16 at 13:37
  • 2
    $\begingroup$ It seems that we cannot prove it ... If $v(S)=$ t the conclusion is false. But then $P \to R \lor S$ is true and also $Z \land \lnot S \to \lnot W$ is true. Finally, we may satisfy both $P \lor Q$ and $R \to W \land Z$. $\endgroup$ Sep 4 '16 at 13:45
  • $\begingroup$ @Mauro ALLEGRANZA: indeed $\endgroup$ Sep 4 '16 at 13:48
  • 1
    $\begingroup$ You have to start from $P \lor Q$ and use $\lor$-elim. The "branch with $Q$ will produce immediately $\lnot S \to Q$, while the "branch" with $P$ needs the other premises. $\endgroup$ Sep 4 '16 at 14:07

We have to start from $P \lor Q$ and use $∨$elim [see here for the ND rules used].

The branch starting with $Q$ will be :

$1_Q)$ $Q$ --- assumed for $\lor$-elim

A) $\lnot S \to Q$ --- from 1) by $\to$-intro.

For the "branch" starting with $P$ we have :

$1_P)$ $P$ --- assumed for $\lor$-elim

2) $R \lor S$ --- from 1) and 2nd premise by $\to$-elim

3) $S$ --- assumed [a] from 2) for $\lor$-elim

4) $\lnot S$ --- assumed [b]

5) $\bot$ --- contradiction : from 3) and 4) by $\lnot$-elim

6) $Q$ --- from 5) by $\bot$-elim

7) $\lnot S \to Q$ --- from 4) and 6) by $\to$-intro, discharging [b].

Now for :

8) $R$ --- assumed [c] for $\lor$-elim

9) $W \land Z$ --- from 8) and 3rd premises by $\to$-elim

10) $W$ --- from 9) by $\land$-elim

11) $Z$ --- from 9) by $\land$-elim

12) $\lnot S$ --- assumed [d]

13) $Z \land \lnot S$ --- from 11) and 12) by $\land$-intro

14) $\lnot W$ --- from 13) and 4th premise by $\to$-elim

15) $\bot$ --- contradiction : from 10) and 14) by $\lnot$-elim

16) $Q$ --- from 15) by $\bot$-elim

17) $\lnot S \to Q$ --- from 12 and 16) by $\to$-intro, discharging [d]

B) $\lnot S \to Q$ --- from 2), 3)-7) and 8)-9) by $\lor$-elim, discharging [a] and [c].

Now from A), B) and the 1st premise: $P \lor Q$, we conclude by $\lor$-elim with:

$\lnot S \to Q$,

discharging assumptions $1_Q)$ and $1_P)$.

  • $\begingroup$ I'm having trouble understanding how to reach the contradiction we want using 3) and 4). $\endgroup$
    – diliad
    Sep 4 '16 at 14:55
  • $\begingroup$ @diliad - 3) $S$ and 4) $\lnot S$ is the contradiction; if you want, tou can use $\land$-intro to get: $S \land \lnot S$. But the rule $\lnot$-elim does not need it. $\endgroup$ Sep 4 '16 at 15:01
  • $\begingroup$ What I cannot understand is what leads us to $\lnot S$, when we make the assumption that S is true after inferring that $R \lor S$. $\endgroup$
    – diliad
    Sep 4 '16 at 15:22
  • $\begingroup$ @diliad - I've assumed it. Then I've discharged it in 7). $\endgroup$ Sep 4 '16 at 16:10

$$\begin{array} {l|l} \lnot S & \text{New Assumption} \\ \quad P & \text{New Assumption} \\ \quad \quad \vdots \\ \quad \quad \bot \\ \quad \lnot P & \lnot \text{Intro} \\ \quad P \lor Q & \text{Given} \\ \quad \vdots \\ \quad Q & \lor\text{Elim} \\ \lnot S \implies Q & \implies \text{Intro} \\ \end{array}$$

Can you fill in the $\vdots$ ?

  • $\begingroup$ I cannot find a way to create the contradiction needed after assuming that P is true. Maybe I'm missing something or it's my foggy head to blame, or even both. $\endgroup$
    – diliad
    Sep 4 '16 at 15:35
  • $\begingroup$ Hint: in the first $\vdots$, you can infer $S \implies W \land Z$ (since $\lnot S$ is under assumption, you can infer $S \implies \text{ anything}$). You should be able to derive a contradiction among the $W$. $\endgroup$
    – DanielV
    Sep 4 '16 at 16:12

The question asks us to prove $\lnot S \to Q$ from the following hypothesis:

  1. $P \lor Q$
  2. $P \to R \lor S$
  3. $R \to W \land Z$
  4. $Z \land \lnot S \to \lnot W$

Let's think about how this could go wrong. It is claimed that if $S$ is false and all four hypotheses hold, then $Q$ is true. So, for a contradiction, assume $S$ is false and $Q$ is false.

If $Q$ is false, then $P$ is true by item 1. Then $R \lor S$ is true by item $2$. We have assumed $S$ is false, so $R$ must be true.

Now, by item 3, $W$ and $Z$ must be true. Finally, by item 4, because $Z$ is true and $S$ is false, $W$ must be false. This is a contradiction, which is what we wanted.

That argument can be turned into a proof by natural deduction. However, instead of assuming $P$ at line 5 of your deduction above, you want to assume $\lnot S$. This is because you are trying to prove an implication whose hypothesis is $\lnot S$, and so you want to put yourself in a position to use implication introduction to do that. Assuming $P$ will not help as directly.

Then, at the next step, you can assume $\lnot Q$. Eventually, you will be able to derive a contradiction, which will let you deduce $Q$.

So the outline looks like this:

  1. Hypothesis 1
  2. Hypothesis 2
  3. Hypothesis 3
  4. Hypothesis 4
  5. $\lnot S$ (assumption)

    5.1. $\lnot Q$ (assumption)

    5.2. ...

    5.3. ...

    5.4. contradiction

    5.5. $Q$ (contradiction rule, discharge 5.1)

  6. $\lnot S \to Q$ (implication introduction, discharge 5)

To handle the implication $P\lor Q, \not Q \vdash P$, you can use something like this.

  1. $P \lor Q$ - assumption
  2. $Q$ - assumption
  3. $\lnot Q$ - assume for $\lor$ elimination from 1

    3.1 Contradiction with 2 3.2 Conclude $P$, discharge 3

  4. $P$ - assume for $\lor$ elimination from 1

    4.1 Conclude $Q$ from 2, discharge 4

  5. $Q$ - $\lor$ elimination from 1, 3, 4

  • $\begingroup$ If I understand this right, after the assumption that Q is false, we can directly infer that, by item 1, P must be true? Although it's very obvious that this holds, I can't think of how to correctly write it down using the basic Natural Deduction rules. $\endgroup$
    – diliad
    Sep 4 '16 at 14:53
  • $\begingroup$ You can't do it in just one step. You need to use the disjunction elimination rule. Basically, you just have to include a deduction of $(P \lor Q),\lnot Q \vdash P$ inside your larger deduction. $\endgroup$ Sep 4 '16 at 16:27
  • 2
    $\begingroup$ I don't understand can you please further explain $\endgroup$
    – user339807
    Sep 4 '16 at 19:42

After an edit the OP asks the following:

Using the suggestions in the answers provided and studying the rules some more, I have come up with this solution. Can you tell me whether it is acceptable?

One way to tell if a proof is likely acceptable is to put it in a proof checker. Since the OP is using a similar Fitch-style natural deduction system as presented by forallx, the proof checker associated with that text could be used to see if the proof is acceptable. Here is the result:

enter image description here

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/


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.