On the application of Modus Tollens rule

Question

Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 166, exercise B.2). When I enter this proof into an automatic checker, it says that application of MT rule is not correct ? Am I missing something ?

Answer 1

If the MT rule is from $\alpha \to \beta$ and $\neg\beta$ infer $\neg\alpha$, then to apply it here, with $\alpha \to \beta$ the conditional $\neg N \to \neg M$, you will need the second input to MT to be $\neg\neg M$. Note the double negation!

So (if you do want a proof via MT) you will need to introduce the required double negation before you can apply MT and continue the proof, derive $\neg\neg N$ and then eliminate that double negation.

A general principle here: although in classical logic $\beta$ and $\neg\neg\beta$ entail each other, every time you want to move between $\beta$ and $\neg\neg\beta$ one way or the other [in a standard natural deduction system for classical logic] you do need to do the required little derivations. Why insist on this palaver? Because later you will meet non-classical logics with a non-classical understanding of negation where, in particular, you can't always make the move from $\neg\neg\beta$ to $\beta$ -- so you need to get used to the idea that there is a non-trivial [in some contexts, disputable] principle at stake in making the classically admissible move!

Answer 2

You need as step 4 $\lnot \lnot M$ from 3. Then Modus tollens on 4 and 2 to get $\lnot \lnot N$. Then conclude $N$ (in two-valued logic).

Answer 3

The MT rule of your text has the content of {($\alpha$$\rightarrow$$\beta$), $\lnot$$\beta$} $\vdash$ $\lnot$$\alpha$ as described on p. 170. So, your proof checker matches your text in not allowing you to use MT in this way.

Instead of using MT though, you might show that (M$\rightarrow$N) holds since ($\lnot$N$\rightarrow$$\lnot$M) holds.