Modus Tollens Proof

Question

I came across the following proof in the book Logic, by Paul Tomassi:

(P & Q) → ~R : R → (P → ~Q)

According to the author, the proof should be a simple application of modus tollens. The following is perhaps the most obvious way of proving it:

 1.   (P & Q) → ~R         Premise
 2.   R                    Assumption
 3.   ~~R                  Double Negative Ins.
 4.   ~(P & Q)             1,3 Modus Tollens
 5.   ~P ∨ ~Q              4 DeMorgen
 6.   P → ~Q               5 Implication Ident.
 7.   R → (P → ~Q)         2,6 Conditional Proof

The only problem is that the author hasn't yet introduced DeMorgen's identity or any other identities. The following is a list of all the resources that have so far been introduced:

• Conjunction Introduction & Elimination
• Conditional Introduction & Elimination (Modus Ponens)
• Biconditional Introduction & Elimination
• Double Negative Introduction & Elimination
• Modus Tollens

However, I don't see any way to do the proof without identity rules. The following is a possible strategy for trying to solve it without identies:

1.   (P & Q) → ~R         Premise
2.   R                    Assumption
3.   ~~R                  Double Negative Ins.
4.   ~(P & Q)             1,3 Modus Tollens
5.   ~(P → ~Q)            Assumption
...
15.  ~(P → ~Q) → (P & Q)  5,14 Conditional Proof
16.  P → ~Q               4,15 Modus Tollens
17.  R → (P → ~Q)         2,16 Conditional Proof

But I don't see how it's possible to get to my theoretical step 15 without deriving the identies from scratch. According to the author, the proof is possible in 11 steps.

How can it be done?

Answer 1

1) $(P \land Q) \to \lnot R$ --- premise

2) $R$ --- assumed [a]

3) $\lnot \lnot R$ --- from 2) by DNI

4) $\lnot (P \land Q)$ --- from 1) and 3) by MT

5) $P$ --- assumed [b]

6) $Q$ --- assumed [c]

7) $P \land Q$ --- from 5) and 6) by $\land$-intro

8) $Q \to (P \land Q)$ --- from 6) and 7) by $\to$-intro, discharging [c]

9) $\lnot Q$ --- from 4) and 8) by MT

10) $P \to \lnot Q$ --- from 5) and 9) by $\to$-intro, discharging [b]

11) $R \to (P \to \lnot Q)$ --- from 2) and 10) by $\to$-intro, discharging [a].

Answer 2

Let's ignore the issue of the specific deductive system in the text. The principle in question, $$ (P \land Q) \to \lnot R \vdash R \to (P \to \lnot Q), $$ is a simple application of currying and uncurrying, and so is provable in a very constructive way, without any rule of contradiction and without double negation elimination. If we temporarily ignore the associativity and commutativity of conjunction, only four steps are needed.

• $(P \land Q) \to R \to \bot $
• $(P \land Q \land R) \to \bot \qquad$ (uncurrying)
• $R \to (P \land Q \to \bot) \qquad$ (currying)
• $R \to P \to Q \to \bot \qquad$ (currying)