Exclusive satisfaction of a predicate

Pure-logic facts about exclusive satisfiers of a predicate P : D → Prop: the property "d is the unique element where P holds." These show up constantly in formalizations of free-choice / exhaustification (where each "pre-exhaustified domain alternative" says "only this d satisfies the prejacent") but the facts themselves are framework-agnostic.

Main results

• exclusive_pairwise_inconsistent — two distinct elements cannot both be the exclusive satisfier.
• neg_all_exclusive_alts — if at least one element satisfies P and no element is the exclusive satisfier, then at least two distinct elements satisfy P.
• exclusive_false_of_universal — if every element satisfies P (and D has at least two elements), then no element is the exclusive satisfier.

Naming follows mathlib idiom: theorems describe what they prove rather than the EFCI-literature label, so non-EFCI consumers can find them.

theorem Quantification.exclusive_pairwise_inconsistent {D : Type u_1} (P : D → Prop) {d₁ d₂ : D} (hne : d₁ ≠ d₂) : ¬((P d₁ ∧ ∀ (e : D), e ≠ d₁ → ¬P e) ∧ P d₂ ∧ ∀ (e : D), e ≠ d₂ → ¬P e)

Pairwise inconsistency of exclusive alternatives: two distinct elements cannot simultaneously be the unique satisfier of P. This is the structural fact behind Spector's closure-failure observation for free-choice item alternative sets: the pre-exhaustified domain alternatives (each saying "only this element satisfies the prejacent") are pairwise incompatible.

theorem Quantification.neg_all_exclusive_alts {D : Type u_1} (P : D → Prop) (hExist : ∃ (d : D), P d) (hNegExcl : ∀ (d : D), ¬(P d ∧ ∀ (e : D), e ≠ d → ¬P e)) : ∃ (d₁ : D), ∃ (d₂ : D), d₁ ≠ d₂ ∧ P d₁ ∧ P d₂

Existence plus no-exclusive-satisfier forces plurality: if P holds somewhere and no element is the exclusive satisfier, then at least two distinct elements satisfy P.

theorem Quantification.exclusive_false_of_universal {D : Type u_1} {a b : D} (hab : a ≠ b) (P : D → Prop) (hAll : ∀ (d : D), P d) (d : D) : ¬(P d ∧ ∀ (e : D), e ≠ d → ¬P e)

Universality kills exclusive satisfiers: if every element of a non-trivial domain satisfies P, then no element is the exclusive satisfier (there's always some other e ≠ d that also satisfies P).

theorem Quantification.uniqueness_precludes_universality {D : Type u_1} {a b : D} (hab : a ≠ b) (P : D → Prop) (hUniq : ∃ (d : D), P d ∧ ∀ (e : D), P e → e = d) : ¬∀ (d : D), P d

Uniqueness precludes universality (contrapositive of exclusive_false_of_universal): in a non-trivial domain, if exactly one element satisfies P, then not every element does.