Can anyone solve (s→p)→r, ~r, (p→q)→(t→r)//~t

I've been at it for hours. The only tools I'm allowed to use are as follows:

Indirect derivation
Direct derivation
Conditional derivation
Modus ponens
Modus tollens
Double negation
Repetition

(s→p)→r
~r
(p→q)→(t→r)
//~t

• I love it! They are like brain teasers. I wish they had them in the paper. Apr 11 '16 at 22:05
• I can get pretty close but I'm having some trouble accomplishing a disjunction introduction to get (p → q) from ~p. Apr 11 '16 at 23:44

(s → p) → r, ~r, (p → q) → (t → r) : ~t

```{1}      1.   (s → p) → r                      Prem.
{2}      2.   ~r                               Prem.
{3}      3.   (p → q) → (t → r)                Prem.
{1,2}    4.   ~(s → p)                         1,2 MT
{5}      5.   p                                Assum.
{6}      6.   s                                Assum.
{5,6}    7.   p & s                            5,6 &I
{5,6}    8.   p                                7 &E
{5}      9.   s → p                            6,8 CP
{1,2,5}  10.  ~(s → p) & (s → p)               4,9 &I
{1,2}    11.  ~p                               5,10 RAA
{12}     12.  ~q                               Assum.
{5,12}   13.  p & ~q                           5,12 &I
{5,12}   14.  p                                13 &E
{5}      15.  ~q → p                           12,14 CP
{1,2,5}  16.  ~~q                              11,15 MT
{1,2,5}  17.  q                                16 DNE
{1,2}    18.  p → q                            5,17 CP
{1,2,3}  19.  t → r                            3,18 MP
{1,2,3}  20.  ~t                               2,19 MT
```

Abbreviations:

```&I = & Introduction
&E = & Elimination
DNE = Double negative elimination
MP = Modus ponens
MT = Modus tollens
CP = → Introduction
```
• I'm not so sure this answers the proof using the limited rules of inference I've been provided with, but thank you! It's still very useful. Apr 12 '16 at 0:31
• @user321275. I'm not familiar with the names of the rules you provided, but if you find a rule that doesn't conform to your constraints, let me know and I can update my answer.
– user3017
Apr 12 '16 at 0:34
• @user321275. I added a list of abbreviations.
– user3017
Apr 12 '16 at 1:15
• Beautiful. Thank you so much. I honestly don't think the question can be answered using the limited rules of inference I was provided. The entire class couldn't finish the proof under the restrictions. I think your answer outlines what I will be learning in my next class. Apr 12 '16 at 1:21
• It looks like you're lacking a contradiction rule. Is that right? If so, I can try to do it without that.
– user3017
Apr 12 '16 at 1:22

It can be answered using the provided rules of inference: DN and ID can take the place of the missing RAA.

1) (s → p) → r --- premise

2) ~r --- premise

3) (p → q) → (t → r) --- premise

4) ~(s → p) --- from 1) and 2) by MT

5) p --- assumed [a]

6) s --- assumed [a1]

7) ~p --- assumed [a2]

8) ~~p --- from 5) and 7) by ID, discharging [a2]

9) p --- from 8) by DN

10) s → p --- from 6) and 9) by CD, discharging [a1]

11) ~p --- from 4), 5) and 10) by ID, discharging [a]

12) p --- assumed [b]

13) ~q --- assumed [c]

14) ~~q --- from 11), 12) and 13), discharging [c]

15) q --- from 14) by DN

16) p → q --- from 12) and 15) by CD, discharging [b]

17) t → r --- from 3) and 16) by MP

18) ~t --- from 2) and 17) by MT.