Existential Pluralization Operator (∃-PL)

[BL21] [Sch96b] [Kri96]

The existential pluralization operator ∃-PL gives definite plurals a basic existential meaning: "the kids laughed" ≈ "at least one kid laughed." This contrasts with Link's * (AlgClosure), which gives universal closure under join. The choice between ∃-PL and * distinguishes the two main families of homogeneity theories: implicature accounts ([Mag14], [BL21]) build on ∃-PL + Exh^{IE+II} strengthening; trivalent accounts ([Sch96b], [Kri15b]) build on */DIST + a truth-value gap.

Main declarations

• existPL — Bar-Lev's existential pluralization with a domain parameter D.
• existPL_full — collapse to plain existential when D ⊇ x.
• existPL_mono — monotonicity in D.
• existPL_singleton — singleton domain reduces to atomic predication.

Implementation notes

∃-PL takes a domain variable D; replacing D with D' ⊆ D generates subdomain alternatives — a set NOT closed under conjunction. This non-closure is the structural property shared with Free Choice disjunction ([Fox07]).

The plural individual x is modelled as Finset Atom with a ∈ x for "a is an atomic part of x". The paper uses mereological ≤_AT (atomic part-of) over Semantics/Mereology.lean's lattice-based Atom predicate. The Finset representation is simpler and adequate for the exhaustification proofs; a mereological formulation can be added as a bridge if needed.

Todo

• Bridge to CandidateInterpretation.malamudDisjunction — they agree on full domain: existPL x P x w ↔ malamudDisjunction P x w.
• Bridge to Plurality.Distributivity.pluralTruthValue (K&S divergence): ¬ (∀ P x w, existPL x P x w ↔ pluralTruthValue P x w = .true) — counterexample at any mixed-truth (P, x).
• Mereological reformulation against Mereology.Atom / Mereology.AlgClosure for unification with Link's *P family.

def Semantics.Plurality.Implicature.existPL {Atom : Type u_1} {W : Type u_2} (D : Finset Atom) (P : Atom → W → Prop) (x : Finset Atom) (w : W) : Prop

∃-PL: Bar-Lev's existential pluralization operator.

⟦∃-PL_D⟧ P x w ↔ ∃ a ∈ x, a ∈ D ∧ P a w

D is a domain variable restricting which atomic parts of x are "visible" for predication. Subdomain alternatives arise from replacing D with D' ⊆ D.

Equations

• Semantics.Plurality.Implicature.existPL D P x w = ∃ a ∈ x, a ∈ D ∧ P a w

@[implicit_reducible]

instance Semantics.Plurality.Implicature.instDecidableExistPLOfDecidableEq {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (D : Finset Atom) (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Decidable (existPL D P x w)

Equations

• Semantics.Plurality.Implicature.instDecidableExistPLOfDecidableEq D P x w = Semantics.Plurality.Implicature.instDecidableExistPLOfDecidableEq._aux_1 D P x w

theorem Semantics.Plurality.Implicature.existPL_full {Atom : Type u_1} {W : Type u_2} (D x : Finset Atom) (P : Atom → W → Prop) (w : W) (h : x ⊆ D) : existPL D P x w ↔ ∃ a ∈ x, P a w

When D contains all atoms of x, ∃-PL reduces to plain existential quantification over atomic parts.

theorem Semantics.Plurality.Implicature.existPL_mono {Atom : Type u_1} {W : Type u_2} (D D' x : Finset Atom) (P : Atom → W → Prop) (w : W) (h : D' ⊆ D) : existPL D' P x w → existPL D P x w

∃-PL is monotone in D: larger domain variable ⇒ weaker (easier to satisfy).

theorem Semantics.Plurality.Implicature.existPL_singleton {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (a : Atom) (P : Atom → W → Prop) (x : Finset Atom) (w : W) (hx : a ∈ x) : existPL {a} P x w ↔ P a w

Singleton domain variable: ∃-PL reduces to individual predication.