Modus tollens

Forma

A partir da condicional $P \rightarrow Q$ e da negação do consequente $\neg Q$, conclui-se $\neg P$.

Intuição

A contrapositiva em ação. Se $Q$ falha, então $P$ necessariamente falhou — é a contrapositiva de $P \rightarrow Q$ aplicada como inferência.

Registro computacional

Se uma função f: P → Q sempre produz $Q$, e observamos um caso sem $Q$, então a entrada não era $P$.