Foundation·F10
Existential quantifier
There is an x: prove it with a witness, use it via an arbitrary one.
Introduction: any witness
satisfying
proves the existential. Elimination, stated with the universal quantifier and implication: if
follows from
for arbitrary
, then
follows from bare existence.
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
Classically the existential is expressible through the universal:
, "not everything fails
", with negation and, for the right-to-left direction, excluded middle. Intuitionistically
is strictly stronger than
: it demands an actual witness. Most ZFC axioms are existentials: pairing, union, power set, infinity, separation and replacement all assert that some set exists. In Lean, Exists is an inductive proposition whose single constructor Exists.intro packages a witness with its proof.
Used by
Propose an edit4 published revisions
- 7/12/2026 · Benjamin· Remove the In words reading and its highlight markup: this article states two inference rules, not a single formula with a natural plain-English translation.what changed →
- 7/12/2026 · Benjamin· Rewrite the In words reading with clearer introduction (witness) / elimination (unnamed witness) phrasing.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 →