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?

  • $\begingroup$ I find your step 3 very counter intuitive. Instead of $\neg \neg R$, I'd assume $P$ and then start a subproof with $Q$ as a premise, then find a contradiction and conclude. I didn't check if this makes it possible to prove it in eleven steps, but it would be my first try. Edit: On a totally unrelated matter, my parents have been to Natal and loved it ^_^ $\endgroup$
    – Git Gud
    Mar 26, 2016 at 21:40
  • $\begingroup$ @Git Gud. According to the author that is a little detail for properly applying modus tollens. He is making the point that ~~R (as opposed to R) is technically the negation of ~R. $\endgroup$
    – User4407
    Mar 26, 2016 at 22:34

2 Answers 2


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].

  • $\begingroup$ This is a nice solution, and very concise. I am not familiar with the book from the question - do you know whether it does have these rules? $\endgroup$ Mar 26, 2016 at 22:22
  • $\begingroup$ That's perfect! Thanks! $\endgroup$
    – User4407
    Mar 26, 2016 at 22:41
  • $\begingroup$ Yes @CarlMummert: the exercise in Tomassi's book is at page 82, after the "rule for negation": DNE, DNI and MT but (as you noted yesterday) before the RAA rule for managing contradictions. $\endgroup$ Mar 27, 2016 at 7:21

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)

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .