# 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 ND

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$

• 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. Sep 4 '16 at 13:37
• 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$. Sep 4 '16 at 13:45
• @Mauro ALLEGRANZA: indeed Sep 4 '16 at 13:48
• 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. 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)$.

• I'm having trouble understanding how to reach the contradiction we want using 3) and 4). Sep 4 '16 at 14:55
• @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. Sep 4 '16 at 15:01
• 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$. Sep 4 '16 at 15:22
• @diliad - I've assumed it. Then I've discharged it in 7). 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$ ?

• 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. Sep 4 '16 at 15:35
• 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$. 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.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

• 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. Sep 4 '16 at 14:53
• 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. Sep 4 '16 at 16:27
• I don't understand can you please further explain
– 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:

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/