From ⊥ (absurdity), derive anything.
Ex falso quodlibet — "from falsehood, anything follows." If you have a proof of ⊥, you can conclude any proposition P whatsoever. This rule has no restrictions on what P can be: once you have a contradiction, every statement becomes provable.
⊥ ————— ⊥-Elim P
Note that ⊥ has no introduction rule — there is no direct way to prove absurdity. You can only derive ⊥ by applying ¬P to P (i.e., using the fact that ¬P is P → ⊥).
| Prover | Syntax |
|---|---|
| Lean 4 | exact absurd hp hnp or contradiction |
| Coq | contradiction or exfalso |
| Agda | ⊥-elim |
The principle of explosion is a defining feature of classical and intuitionistic logic. Paraconsistent logics reject this rule, allowing contradictions to exist without everything becoming provable. In standard mathematics, however, ex falso is universally accepted and plays a crucial role in proofs by contradiction.
Prove ⊥ → P ∧ Q. You will need ⊥-Elim and what else?
Start with →-Intro to assume ⊥. To build P ∧ Q you need ∧-Intro, which requires proofs of both P and Q. Use ⊥-Elim twice — once to get P and once to get Q.
[⊥]¹ [⊥]¹
————— ⊥-Elim ————— ⊥-Elim
P Q
————————————— ∧-Intro
P ∧ Q
——————————————— →-Intro¹
⊥ → P ∧ Q
You need ⊥-Elim (twice, to produce P and Q from ⊥) and ∧-Intro (to combine them), plus →-Intro to close the assumption.
See also: Logic §06 — Negation