Mathematics & AI

Exploring the frontier of automated discovery.

← Back to all articles

Working with Existential Quantifiers, Universal Quantifiers, and Classical Reasoning in Lean

November 27, 2025 • Sham Prop Lean4 TPiL4 propositional-logic

This note collects a series of Lean examples from TPiL4, that involve existential quantifiers, universal quantifiers, implications, conjunctions, disjunctions, negation, and classical reasoning. Each example is written in Lean4. When classical logic is used, I specify it.

We assume open Classical at the top to allow classical reasoning such as double negation elimination and byContradiction.

From existence of a witness to a proposition

example : (∃ x : α, r) → r :=
  fun h : (∃ x : α, r) =>
    Exists.elim h (
      fun w (hr:r )=> hr
    )

Explanation: If there exists a witness w such that r holds, then r is true. Eliminating the existential gives the witness and the proof of r, so we simply return the proof.

Introducing an existential witness

example (a : α) : r → (∃ x : α, r) :=
  fun hr : r => Exists.intro a hr

Explanation: If r holds, we can create an existential statement by choosing any element a and pairing it with the proof of r.

Existential with conjunction distributes over existential and r

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
Iff.intro
  (fun h : (∃ x, p x ∧ r) =>
    Exists.elim h (fun w => fun hpr : p w ∧ r =>
      And.intro (Exists.intro w hpr.left) hpr.right))
  (fun h : (∃ x, p x) ∧ r =>
    Exists.elim h.left (fun w => fun hp : p w =>
      Exists.intro w (And.intro hp h.right)))

Explanation: Existential distributes over a conjunction. One direction extracts the witness and splits the conjunction. The other direction reassembles a witness whose property contains both parts.

Existential distributes over disjunction

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
Iff.intro
  (fun h : (∃ x, p x ∨ q x) =>
    Exists.elim h ( fun w => fun hpw : p w ∨ q w =>
      Or.elim hpw
        (fun hp : p w => Or.inl (Exists.intro w  hp))
        (fun hq : q w => Or.inr (Exists.intro w  hq))
    ))
  (
    fun h : (∃ x, p x) ∨ (∃ x, q x) =>
      Or.elim h
        (fun h1 : (∃ x, p x) =>
          Exists.elim h1 (fun w => fun hw : p w => Exists.intro w (Or.inl hw)))
        (fun h2 : (∃ x, q x) =>
          Exists.elim h2 (fun w => fun hw : q w => Exists.intro w (Or.inr hw)))
  )

Explanation: An existential over a disjunction is equivalent to a disjunction of existentials. Both directions are constructive and follow from inspecting which side of the disjunction holds.

Universal quantifier and negation of an existential

example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
  Iff.intro
    (fun h : (∀ x, p x) =>
      fun h1 : (∃ x, ¬ p x) =>
        Exists.elim h1 (fun w => fun h2 : ¬ p w => show False from h2 (h w)))
    (fun h : ¬ (∃ x, ¬ p x) => fun x =>
      byContradiction (fun hpx =>  h ⟨x, hpx⟩))

Explanation: The forward direction is constructive: if everything satisfies p, then no witness of ¬p exists. The reverse direction is classical. It uses byContradiction to convert ¬¬p x into p x. This step needs classical logic.

Double negation elimination

example (t : Prop): ¬¬t → t :=
  fun h : ¬¬t => byContradiction (fun ht : ¬t => h ht)

Explanation: Double negation elimination is not constructive. It requires classical logic, and Lean uses byContradiction here.

Existential and double negation

example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
Iff.intro
  (fun h : (∃ x, p x) => fun h1 :  (∀ x, ¬ p x) =>
    Exists.elim h (fun w => fun hpw : p w => show False from (h1 w) hpw))
  (fun hn : ¬ (∀ x, ¬ p x) =>
    byContradiction (fun h : ¬ (∃ x, p x) =>
      hn (fun x (hx:p x )=> h ⟨x, hx⟩)))

Explanation: The first direction is constructive. The second direction uses classical reasoning to convert ¬¬∃ x p x into ∃ x p x.

Negation of an existential is equivalent to a universal negation

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
Iff.intro
  (fun h : ¬ (∃ x, p x) => fun x (hx: p x) => h ⟨x, hx ⟩)
  (fun h : (∀ x, ¬ p x) => fun hex : ∃ x, p x =>
    Exists.elim hex (fun w => fun hw : p w => show False from (h w) hw))

Explanation: Both directions are constructive. Eliminating the existential allows you to compute the contradiction directly.

Negating a universal is equivalent to an existential negation

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
Iff.intro
  (fun h : ¬ (∀ x, p x) =>
    byContradiction (fun hn : ¬ (∃ x, ¬ p x) =>
      h (fun x => byContradiction (fun hpx => hn ⟨x, hpx ⟩))
    ))
  (fun h : (∃ x, ¬ p x) => fun hn :  (∀ x, p x) =>
    Exists.elim h (fun x => fun hpx : ¬ p x => show False from hpx (hn x))
  )

Explanation: The right direction is constructive. The left direction uses classical logic because it depends on double negation elimination and the classical equivalence between ¬∀ and ∃¬.

Relationship between universal implication and existential implication

example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
Iff.intro
  (fun h: (∀ x, p x → r) => fun hp : (∃ x, p x) =>
    Exists.elim hp (fun w => fun hw : p w => (h w) hw))
  (fun h : (∃ x, p x) → r =>
    fun w => fun hp : p w => h ⟨w, hp ⟩)

Explanation: Both directions are constructive.

Left to right: If every p w implies r, then an existential witness gives p w, and therefore r.

Right to left: Fix w and assume p w. You can always build an existential witness ⟨w, hp⟩ and then apply h to obtain r. This direction works because an existential can always be introduced from a single p w.

Thanks for reading!