Foundation·F03
Falsum
The absurd proposition: it has no proof, and from it anything follows.
Equivalently, as a statement of implication:
for every proposition
.
Part of the logical framework beneath ZFC (classical first-order logic with equality): taken as given rather than proven, it belongs to the language the set-theoretic axioms are stated in.
Remarks
has no introduction rule, and that absence is its meaning (see the logical framework). Its role is to make refutation expressible: negation is defined as implication into
. A theory is consistent exactly when
is not derivable in it. In Lean, False is the inductive proposition with no constructors, and ex falso is its eliminator, False.elim.
Used by
Propose an edit3 published revisions
- 7/12/2026 · Benjamin· Remove the In words reading and its highlight markup: this article states an inference rule (ex falso), not a single formula with a natural plain-English translation.what changed →
- 7/11/2026 · Benjamin· Fix Mathlib link: add the #doc fragment doc-gen4's find endpoint requires (old link 404'd). Content unchanged.what changed →
- 7/11/2026 · Benjamin· Logic layer: connectives and quantifierswhat changed →