nLab contrapositive

In propositional logic, the contrapositive rule states that it is valid to derive $\neg{Q} \to \neg{P}$ from $P \to Q$ (where $\neg$ is negation and $\to$ is implication). In symbols:

$$\frac {P \to Q} {\neg{Q} \to \neg{P}} \;CP$$

The combination of this rule, followed by modus ponens (the elimination rule for implication) was traditionally called modus tollens:

$$\frac {\displaystyle\frac{P \to Q} {\neg{Q} \to \neg{P}} \;CP \;\;\; \neg{Q}} {\neg{P}} \; \to\mathcal{E}$$

The contrapositive rule is valid in intuitionistic logic, not just in classical logic; however, the reverse rule is valid only in classical logic.

Another intuitionistically valid rule, this one reversible, is

$$\frac {P \to \neg{Q}} {Q \to \neg{P}}$$

as both statements are equivalent to the negation of $P \wedge Q$ (where $\wedge$ is conjunction). However, the superficially similar

$$\frac {\neg{P} \to Q} {\neg{Q} \to P}$$

is again valid only classically.