From a book I'm reading for logic and computer science, the nested proof is as follows:

  1. {$q \rightarrow r$ assumption

  2. [$\neg q \rightarrow \neg p$ assumption

  3. ( $p$ assumption

  4. $\neg \neg p$ $\neg \neg i $ 3

  5. $\neg \neg q$ $MT$ 2,4 (applying Modus Tollens)

  6. $q$ $\neg \neg e$ 5

  7. $r$ $\rightarrow e 1,6$ )

  8. ... ]

  9. ...

  10. final proof}

note: sorry about the different brackets it was my attempt to show a nested proof.

my question is concerning how r in line number seven is derived. So, my first instinct tells me to apply the Modus Tollen rule to lines 2 and 3 and we can obtain $q$ that way, but I don't understand why do they apply the double negation rule to $p$ and didn't apply MT rule directly.

So, it would be

given the assumption of $\neg q \rightarrow \neg p$ given $p$

then we could derive $\vdash q$


1 Answer 1


Remember that modus tollens says that from $A\to B$ and $\neg B$ you can infer $\neg A$. So from $\neg q\to\neg p$ and $\neg \neg p$ you can infer $\neg\neg q$. That's why you need to use the rules to add (and then remove) the double negations even though those rules seem unnecessary to us in natural language.

  • $\begingroup$ OK, so the modus tollens doesn't apply to when a given assumption/premise is not a type of negation? hence why we need to convert to $\neg \neg p$ $\endgroup$
    – KetDog
    Commented Oct 6, 2019 at 17:10
  • $\begingroup$ please see if you can reply to my question in the comment above. $\endgroup$
    – KetDog
    Commented Oct 7, 2019 at 1:55
  • 1
    $\begingroup$ @SimonGarfe Yes, that is what Matthew said. $\endgroup$ Commented Oct 7, 2019 at 3:33

You must log in to answer this question.

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