nLab contrapositive

Definition

In propositional logic, the contrapositive of an implication $P\to Q$ is the converse implication $(\neg Q) \to (\neg P)$ of negations.

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

$$\frac {P \to Q} {\neg{Q} \to \neg{P}} \;CP \mathrlap{\,.}$$

The combination of this rule, followed by modus ponens (MP, 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}} \;\; MP \mathrlap{\,.}$$

The contrapositive rule is valid in intuitionistic logic, not just in classical logic; however, the reverse rule is valid only in classical logic (apply the reverse rule to the consequent of $\neg{P}\to(\neg{Q}\to\neg{P})$; the dreaded $\neg\neg{P}\to{P}$ then easily follows from $\neg\neg{P}\to(\neg{P}\to\neg\neg\neg{P})$ with another use of the reverse rule).

Another intuitionistically valid rule, this one reversible, is

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

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.

Related concepts

• implication

• negation