Proving Sequent using Natural Deduction

Question

RTP: $P \to Q, R \to \neg Q, (S\to \neg P)\to R \vdash (\neg T ∨ P)\to(T \to S)$ using primitive rules of natural deduction. I've attempted this question multiple times but keep getting stuck on trying to get $S$ so I can use a couple arrow introductions to get the conclusion.

Attempt:

1 (1) $P \to Q$ Assumption

2 (2) $R \to \neg Q$ Assumption

3 (3) $(S\to \neg P)\to R$ Assumption

4 (4) $(\neg T ∨ P)$ Assumption

5 (5) $T$ Assumption

4,5 (6) $P$ $4,5∨$E

1,4,5 (7) $Q$ $1,6\to$E

8 (8) $S$ Assumption

9 (9) $S\to \neg P$ Assumption

8,9 (10) $\neg P$ Assumption

4,5,9 (11) $\neg T$ 6,10RAA(8)

12 (12) R Assumption

2,12 (13) $\neg Q$ $2,12\to$E

1,2,4,5 (14) $~R$ 7,13RAA(12)

I realise now that I've eliminated almost all the necessary assumptions with only line 9 left over (those at lines 4 and 5 which will be eliminated via arrow introduction for the conclusion once I have $S$), but I don't know how I can proceed from here. Any help would be greatly appreciated.

Answer 1

The premise is a negation $\neg(S \to \neg P)$, so it is likely you need to perform negation elimination. For that you need to intermediately derive $S \to \neg P$, resulting in a contradiction from which you may infer anything.
That anything will be $S$, so you prove the conclusion by contradiction, assuming $\neg S$ earlier on and dropping that assumption in the last step.
Now you want to derive $S \to \neg P$; this is an implication, so you have to derive $\neg P$ from an assumption $S$. Given the other assumptions you have at your disposal, how do you think that subderivation can be plugged together?

Answer 2

Here is a proof using "primitive rules" of Natural Deduction.

From line (4) $(¬T ∨ P)$ --- Assumption, we apply $(\lor \text E)$ with two sub-proofs:

The first one is straightforward:

5. $\lnot T$ --- assumed [a] for $(\lor \text E)$

6. $T$ -assumed [b]

7. $\bot$ --- from 5) and 6) using $(\lnot \text E)$

8. $S$ --- from 7) using $(\bot \text E)$

9. $(T \to S)$ --- from 6) and 8) by $(\to \text I)$, discharging [b].

The second sub-proof:

10. $P$ --- assumed [d] for $(\lor \text E)$

11. $Q$ --- from 10) and 1) by $(\to \text E)$

12. $R$ --- assumed [e]

13. $\lnot Q$ --- from 12) and 2) by $(\to \text E)$

14. $\bot$ --- from 11) and 13) by $(\lnot \text E)$

15. $\lnot R$ --- from 12) by $(\lnot \text I)$, discharging [e]

16. $(S \to \lnot P)$ --- assumed [f]

17. $R$ --- from 16) and 3) by $(\to \text E)$

18. $\bot$ --- from 15) and 17) by $(\lnot \text E)$

19. $\lnot (S \to \lnot P)$ --- from 16) and 18) by $(\lnot \text I)$, discharging [f]

20. $\lnot S$ --- assumed [g]

21. $S$ --- assumed [h]

22. $\bot$ --- from 20) and 21) by $(\lnot \text E)$

23. $\lnot P$ --- from 22) by $(\bot \text E)$

24. $(S \to \lnot P)$ --- from 21) and 23) by $(\to \text I)$, discharging [h]

25. $\bot$ --- from 19) and 24) by $(\lnot \text E)$

26. $S$ --- from 20) and 25) by $(\neg \neg \text E)$: if $\Gamma , \neg \varphi \vdash \bot$, then $\Gamma \vdash \varphi$, discharging [g]

27. $(T \to S)$ --- from 26) by $(\to \text I)$.

Now we have derived $(T \to S)$ in the two sub-proofs and we can close the $(\lor \text E)$:

28. $(T \to S)$ --- from 4), 9) and 27) discharging assumptions [a] and [c]

$(\lnot T \lor P) \to (T \to S)$ --- from 4) and 28) by $(\to \text I)$.

---

Here is an alternative proof that uses Disjunctive syllogism:

4. $(¬T ∨ P)$ --- Assumption

5. $T$ --- assumed [a]

6. $P$ --- from 4) and 5)

Now we insert lines 10)-26) above to get:

26. $S$

and we conclude with:

$T \to S$ --- from 5) and 27) by $(\to \text I)$, discharging [a]

Answer 3

$\def\fitch#1#2{~~\begin{array}{|l|}\hline #1\\\hline#2\\\hline\end{array}~~}$

You seek to derive $S$ under the assumption of $T$, $\lnot T\vee P$, and the premises.

You can immediately derive $P$ and $Q$ using disjunctive syllogism and modus ponens.

Likewise you could there after derive $\neg R$ and $\neg(S\to\neg P)$ using modus tollens.

However, I'd rather use reduction to absurdity to derive $S$.

Discharge the necessary contradictions and you are done.

$$\fitch{~~1.~P\to Q\\~~2.~R\to\lnot Q\\~~3.~(S\to\lnot P)\to R}{\fitch{~~4.~\lnot T\lor P}{\fitch{~~5.~T}{~~6.~P\\~~7.~Q\\\fitch{~~8.~\lnot S}{\vdots\\14.~\lnot Q}\\15.~S}\\16.~T\to S}\\17.~(\lnot T\lor P)\to(T\to S)}$$

Using logic.tamu.edu/daemon.html

P->Q, R->~Q, (S->~P)->R |- (~TvP)->(T->S)
OK    1          (1)   P->Q           A         
OK    2          (2)   R->~Q          A         
OK    3          (3)   (S->~P)->R     A         
OK    4          (4)   ~TvP           A         
OK    5          (5)   T              A         
OK    4,5        (6)   P              4,5vE     
OK    1,4,5      (7)   Q              1,6->E    
OK    8          (8)   ~S             A         
:     :          :     :              :
OK    2,3,8      (14)  ~Q             ..,..->E   
OK    1,2,3,4,5  (15)  S              7,14RAA(8)
OK    1,2,3,4    (16)  T->S           15->I(5)  
OK    1,2,3      (17)  (~TvP)->(T->S) 16->I(4)