**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

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 15:19:33. See the history of this page for a list of all contributions to it.