Foundation·F06
Disjunction
A or B, inclusively: it follows from either, and is used by cases.
Either disjunct proves the disjunction. Elimination is proof by cases, stated with implication: if each disjunct leads to
, then
follows from the disjunction.
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
Mathematical "or" is inclusive:
does not exclude both holding at once. Classically it is definable as
, but the rules are primary (see the logical framework), and the abbreviation hides the real content of proof by cases. Intuitionistically a proof of
is a proof of one side together with a tag saying which; classical logic, via excluded middle, asserts disjunctions without providing the tag. In Lean, Or is an inductive proposition with constructors Or.inl and Or.inr, and proof by cases is Or.elim.
Used by
Propose an edit4 published revisions
- 7/12/2026 · Benjamin· Remove the In words reading and its highlight markup: this article states three inference rules, not a single formula with a natural plain-English translation.what changed →
- 7/12/2026 · Benjamin· Rewrite the In words reading to cover both introduction and proof-by-cases elimination.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 →