# nLab contrapositive

(0,1)-category

(0,1)-topos

## Theorems

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.

Last revised on April 23, 2017 at 11:19:33. See the history of this page for a list of all contributions to it.