Modus Tollendo Ponens/Variant/Formulation 1

Theorem

$p \lor q \dashv \vdash \neg p \implies q$

This can be expressed as two separate theorems:

Forward Implication

$p \lor q \vdash \neg p \implies q$

Reverse Implication

$\neg p \implies q \vdash p \lor q$

Note that the latter proof requires Law of Excluded Middle.

Therefore it is not valid in intuitionistic logic.

Proof

We apply the Method of Truth Tables.

As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.

$\begin{array}{|ccc||cccc|} \hline p & \lor & q & \neg & p & \implies & q \\ \hline F & F & F & T & F & F & F \\ F & T & T & T & F & T & T \\ T & T & F & F & T & T & F \\ T & T & T & F & T & T & T \\ \hline \end{array}$

$\blacksquare$