Foundation·F04
Negation
Not A is an abbreviation: A implies falsum.
Defined from implication and falsum: to refute
is to show that
leads to absurdity.
In words
Not A holds when, if A is assumed, then a contradiction follows.
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
Negation is not primitive; it is notation for
, and its rules are inherited from those of implication. From
and
, modus ponens yields
, and then ex falso yields anything. Note what the definition does not give: double negation elimination,
, is not derivable from the rules alone. It is exactly as strong as excluded middle and is what makes the logic classical. In Lean, Not is defined verbatim as
False.
Used by
Propose an edit4 published revisions
- 7/12/2026 · Benjamin· Spell out the if/then structure explicitly and highlight the arrow, A, and falsum separately.what changed →
- 7/12/2026 · Benjamin· Add word-notation highlight markup linking "Not A" and its defining condition to the statement.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 →