Plural Distributivity and Non-Maximality

Formalizes the independence of distributivity and maximality, following Križ & @cite{kriz-spector-2021} and @cite{haslinger-etal-2025}.

Insight

Distributivity (predicate applies to each atom) and maximality (no exceptions allowed) are orthogonal semantic properties. The tolerance relation ⪯ (which pluralities count as "similar enough") is a contextual parameter—essentially a QUD on the plurality domain.

Connection to QUD Infrastructure

A tolerance relation induces a partition on pluralities:

• Identity tolerance → exact QUD (every distinction matters)
• Coarser tolerance → coarser QUD (some exceptions irrelevant)

This parallels how QUDs partition propositions in Core/QUD.lean.

structure Semantics.Plurality.Distributivity.Tolerance (Atom : Type u_3) [DecidableEq Atom] : Type u_3

A tolerance relation determines which sub-pluralities count as "similar enough" to the whole for current conversational purposes.

Formally: ⪯ is reflexive and respects mereological structure.

• rel : Finset Atom → Finset Atom → Prop

  y ⪯ x: y is similar enough to x

• decRel (x y : Finset Atom) : Decidable (self.rel x y)

  Decidability of the tolerance relation.

• refl (x : Finset Atom) : self.rel x x

  Reflexivity

• sub (x y : Finset Atom) : self.rel x y → x ⊆ y

  Tolerance implies part-of

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.Tolerance.instDecidableRel {Atom : Type u_3} [DecidableEq Atom] (tol : Tolerance Atom) (x y : Finset Atom) : Decidable (tol.rel x y)

Per-Tolerance decidability instance for the relation.

Equations

• tol.instDecidableRel x y = tol.decRel x y

def Semantics.Plurality.Distributivity.Tolerance.identity {Atom : Type u_1} [DecidableEq Atom] : Tolerance Atom

Identity: only x ⪯ x (forces maximal reading)

Equations

• Semantics.Plurality.Distributivity.Tolerance.identity = { rel := fun (x y : Finset Atom) => x = y, decRel := fun (x y : Finset Atom) => decEq x y, refl := ⋯, sub := ⋯ }

def Semantics.Plurality.Distributivity.Tolerance.trivial {Atom : Type u_1} [DecidableEq Atom] : Tolerance Atom

Trivial: any part is tolerated (allows existential reading). @cite{kriz-spector-2021} call this the trivial tolerance — the relation is just sub-pluralityhood, with no further restriction.

Equations

• Semantics.Plurality.Distributivity.Tolerance.trivial = { rel := fun (x y : Finset Atom) => x ⊆ y, decRel := fun (x y : Finset Atom) => Finset.decidableDforallFinset, refl := ⋯, sub := ⋯ }

def Semantics.Plurality.Distributivity.distMaximal {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Prop

Maximal distributive: ⟦each P⟧(x) = ∀a ∈ x. P(a)

This is the semantics of English "each", German "jeder".

Equations

• Semantics.Plurality.Distributivity.distMaximal P x w = ∀ a ∈ x, P a w

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.distMaximal.instDecidable {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Decidable (distMaximal P x w)

Equations

• Semantics.Plurality.Distributivity.distMaximal.instDecidable P x w = id inferInstance

def Semantics.Plurality.Distributivity.distTolerant {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (tol : Tolerance Atom) (x : Finset Atom) (w : W) : Prop

Tolerant distributive: ⟦each* P⟧^⪯(x) = ∃z. z ⪯ x ∧ z ≠ ∅ ∧ ∀a ∈ z. P(a)

This is the semantics of German "jeweils" (for non-max speakers). The nonemptiness constraint prevents the empty set from vacuously witnessing truth (∀a ∈ ∅, P a w is trivially true).

Equations

• Semantics.Plurality.Distributivity.distTolerant P tol x w = ∃ z ∈ x.powerset, z.Nonempty ∧ tol.rel z x ∧ ∀ a ∈ z, P a w

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.distTolerant.instDecidable {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (tol : Tolerance Atom) (x : Finset Atom) (w : W) : Decidable (distTolerant P tol x w)

Equations

• Semantics.Plurality.Distributivity.distTolerant.instDecidable P tol x w = id inferInstance

theorem Semantics.Plurality.Distributivity.distMaximal_iff_identity {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : distMaximal P x w ↔ distTolerant P Tolerance.identity x w

Maximal distributive ↔ tolerant distributive with identity tolerance (on nonempty pluralities).

theorem Semantics.Plurality.Distributivity.distMaximal_forces_all {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : distMaximal P x w → ∀ a ∈ x, P a w

Maximal distributive forces all atoms to satisfy P

theorem Semantics.Plurality.Distributivity.distTolerant_allows_exceptions {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (a : Atom) (ha : a ∈ x) (hPa : P a w) : distTolerant P Tolerance.trivial x w

Tolerant distributive with trivial tolerance allows exceptions

The Križ & @cite{kriz-spector-2021} Account

@cite{kriz-spector-2021}

The K&S theory explains both homogeneity and non-maximality through:

1. Candidate interpretations: For "the Xs are P", generate propositions {∀a∈z. P(a) | z ⊆ X} for all sub-pluralities z.

2. Trivalent semantics:

   • TRUE at w: all candidates true at w
   • FALSE at w: all candidates false at w
   • GAP: some true, some false

3. Homogeneity: The gap is symmetric under negation. This explains why "the Xs are P" (quasi-universal) and "the Xs aren't P" (quasi-existential) have the same undefined region.

4. Non-maximality: QUD-based relevance filtering reduces the candidate set, allowing sentences to be judged true even when not all candidates hold.

def Semantics.Plurality.Distributivity.allSatisfy {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Prop

All atoms in x satisfy P at w

Equations

• Semantics.Plurality.Distributivity.allSatisfy P x w = ∀ a ∈ x, P a w

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.allSatisfy.instDecidable {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Decidable (allSatisfy P x w)

Equations

• Semantics.Plurality.Distributivity.allSatisfy.instDecidable P x w = id inferInstance

def Semantics.Plurality.Distributivity.someSatisfy {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Prop

Some atom in x satisfies P at w

Equations

• Semantics.Plurality.Distributivity.someSatisfy P x w = ∃ a ∈ x, P a w

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.someSatisfy.instDecidable {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Decidable (someSatisfy P x w)

Equations

• Semantics.Plurality.Distributivity.someSatisfy.instDecidable P x w = id inferInstance

def Semantics.Plurality.Distributivity.noneSatisfy {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Prop

No atom in x satisfies P at w

Equations

• Semantics.Plurality.Distributivity.noneSatisfy P x w = ∀ a ∈ x, ¬P a w

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.noneSatisfy.instDecidable {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Decidable (noneSatisfy P x w)

Equations

• Semantics.Plurality.Distributivity.noneSatisfy.instDecidable P x w = id inferInstance

def Semantics.Plurality.Distributivity.pluralTruthValue {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Core.Duality.Truth3

The trivalent truth value for plural predication "the Xs are P".

• TRUE: all atoms satisfy P
• FALSE: no atoms satisfy P
• GAP: some but not all satisfy P

This is the core of @cite{kriz-spector-2021} Section 2, instantiated as a supervaluation over the atoms of the plurality: each atom is a "specification point", and predication is super-true iff the predicate holds at all of them.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Semantics.Plurality.Distributivity.pluralTruthValue_eq_true_iff {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.true ↔ allSatisfy P x w

pluralTruthValue is .true iff allSatisfy holds

@[simp]

theorem Semantics.Plurality.Distributivity.pluralTruthValue_eq_false_iff {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.false ↔ x.Nonempty ∧ noneSatisfy P x w

pluralTruthValue is .false iff noneSatisfy holds (and x is nonempty)

@[simp]

theorem Semantics.Plurality.Distributivity.pluralTruthValue_eq_gap_iff {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.indet ↔ (∃ a ∈ x, P a w) ∧ ∃ a ∈ x, ¬P a w

pluralTruthValue is .indet iff witnesses on both sides exist

theorem Semantics.Plurality.Distributivity.pluralTruthValue_eq_dist {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.dist x fun (a : Atom) => P a w

pluralTruthValue is Core.Duality.dist on the plurality.

Bridge from Križ-Spector trivalent plural predication to the canonical trivalent classifier. Both are Fine super-truth (van Fraassen 1966 supervaluation) — pluralTruthValue parameterized over an atom-world predicate, dist over an arbitrary Finset α + (α → Prop). The nonempty case routes through superTrue_eq_dist; the empty case matches because both give .true (vacuous super-truth).

theorem Semantics.Plurality.Distributivity.allSatisfy_imp_noneSatisfy_neg {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allSatisfy P x w → noneSatisfy (fun (a : Atom) (w : W) => ¬P a w) x w

If all satisfy P, then none satisfy ¬P

theorem Semantics.Plurality.Distributivity.noneSatisfy_imp_allSatisfy_neg {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : noneSatisfy P x w → allSatisfy (fun (a : Atom) (w : W) => ¬P a w) x w

If none satisfy P, then all satisfy ¬P

def Semantics.Plurality.Distributivity.inGap {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Prop

The gap condition: some but not all atoms satisfy P

Equations

• Semantics.Plurality.Distributivity.inGap P x w = ((∃ a ∈ x, P a w) ∧ ∃ a ∈ x, ¬P a w)

theorem Semantics.Plurality.Distributivity.homogeneity_gap_symmetric {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : inGap P x w ↔ inGap (fun (a : Atom) (w : W) => ¬P a w) x w

Homogeneity Theorem (Križ & @cite{kriz-spector-2021}, Section 2.1).

The gap is symmetric under negation: a world is in the gap for P iff it's in the gap for ¬P.

This explains why:

• "The Xs are P" is undefined when some but not all Xs are P
• "The Xs aren't P" is ALSO undefined in exactly those worlds

Proof: The gap for P is {∃a.P(a) ∧ ∃a.¬P(a)}. The gap for ¬P is {∃a.¬P(a) ∧ ∃a.¬¬P(a)} = {∃a.¬P(a) ∧ ∃a.P(a)}. These are identical (in classical logic; uses Decidable on P).

theorem Semantics.Plurality.Distributivity.pluralTruthValue_gap_iff_neg_gap {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (_hne : x.Nonempty) : pluralTruthValue P x w = Core.Duality.Truth3.indet ↔ pluralTruthValue (fun (a : Atom) (w : W) => ¬P a w) x w = Core.Duality.Truth3.indet

Corollary: pluralTruthValue is gap iff negated version is gap.

theorem Semantics.Plurality.Distributivity.pluralTruthValue_neg {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : pluralTruthValue (fun (a : Atom) (w : W) => ¬P a w) x w = match pluralTruthValue P x w with | Core.Duality.Truth3.true => Core.Duality.Truth3.false | Core.Duality.Truth3.false => Core.Duality.Truth3.true | Core.Duality.Truth3.indet => Core.Duality.Truth3.indet

Homogeneity Polarity Theorem: Truth and falsity swap under negation.

If "the Xs are P" is TRUE, then "the Xs are ¬P" is FALSE, and vice versa.

Note: Requires x to be nonempty. For empty x, both allSatisfy P and allSatisfy ¬P are vacuously true, so the theorem doesn't hold.

theorem Semantics.Plurality.Distributivity.distMaximal_singleton {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (a : Atom) (w : W) : distMaximal P {a} w ↔ P a w

On singletons, distMaximal reduces to the predicate itself.

This is WHY each/jeder forces maximality: when it distributes P to individual atoms, the result is just P(a) — there's no plurality for tolerance to weaken. @cite{haslinger-etal-2025} §2.3, the argument below the four-way classification.

theorem Semantics.Plurality.Distributivity.distMaximal_pair {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (a b : Atom) (w : W) : distMaximal P {a, b} w ↔ P a w ∧ P b w

On pairs, distMaximal reduces to conjunction of individual checks.

This is the two-atom instance of Link's distributive inference (distr_atom_part in Link1983.lean): for a distributive P, checking *P on a two-atom plurality {a, b} reduces to P(a) ∧ P(b).

When a = b, {a, b} = {a} (Finset dedup) and the result degenerates to P a w (= P a w ∧ P a w by and_self).

theorem Semantics.Plurality.Distributivity.distTolerant_singleton {Atom : Type u_3} [DecidableEq Atom] {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (tol : Tolerance Atom) (a : Atom) (w : W) : distTolerant P tol {a} w ↔ P a w

Atom Vacuity Theorem (general).

On singletons, distTolerant reduces to the predicate itself for ANY tolerance relation — not just identity tolerance.

This is because {a} has exactly one nonempty subset (itself), and tol.refl guarantees tol.rel {a} {a} holds. The tolerance parameter literally has nothing to vary over.

theorem Semantics.Plurality.Distributivity.distTolerant_singleton_independent {Atom : Type u_3} [DecidableEq Atom] {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (tol₁ tol₂ : Tolerance Atom) (a : Atom) (w : W) : distTolerant P tol₁ {a} w ↔ distTolerant P tol₂ {a} w

Corollary: on singletons, all tolerance relations agree.

theorem Semantics.Plurality.Distributivity.distTolerant_identity_singleton {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (a : Atom) (w : W) : distTolerant P Tolerance.identity {a} w ↔ P a w

Special case: identity tolerance on singletons.

structure Semantics.Plurality.Distributivity.DistMaxClass : Type

Classification by [±distributive] × [±maximal].

@cite{haslinger-etal-2025} present a four-cell typology in which the two properties are argued to be orthogonal: all four cells are attested or predicted.

• isDistributive : Bool

  Does this operator force the predicate to apply to each atom separately?

• isMaximal : Bool

  Does this operator block exception tolerance (force all atoms to satisfy P)?

def Semantics.Plurality.Distributivity.instDecidableEqDistMaxClass.decEq (x✝ x✝¹ : DistMaxClass) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.instDecidableEqDistMaxClass : DecidableEq DistMaxClass

Equations

• Semantics.Plurality.Distributivity.instDecidableEqDistMaxClass = Semantics.Plurality.Distributivity.instDecidableEqDistMaxClass.decEq

def Semantics.Plurality.Distributivity.instReprDistMaxClass.repr : DistMaxClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.instReprDistMaxClass : Repr DistMaxClass

Equations

• Semantics.Plurality.Distributivity.instReprDistMaxClass = { reprPrec := Semantics.Plurality.Distributivity.instReprDistMaxClass.repr }

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.instBEqDistMaxClass : BEq DistMaxClass

Equations

• Semantics.Plurality.Distributivity.instBEqDistMaxClass = { beq := Semantics.Plurality.Distributivity.instBEqDistMaxClass.beq }

def Semantics.Plurality.Distributivity.instBEqDistMaxClass.beq : DistMaxClass → DistMaxClass → Bool

Equations

• Semantics.Plurality.Distributivity.instBEqDistMaxClass.beq { isDistributive := a, isMaximal := a_1 } { isDistributive := b, isMaximal := b_1 } = (a == b && a_1 == b_1)
• Semantics.Plurality.Distributivity.instBEqDistMaxClass.beq x✝¹ x✝ = false

def Semantics.Plurality.Distributivity.DistMaxClass.distMax : DistMaxClass

each, jeder (DP and distance): +dist, +max

Equations

• Semantics.Plurality.Distributivity.DistMaxClass.distMax = { isDistributive := true, isMaximal := true }

def Semantics.Plurality.Distributivity.DistMaxClass.distNonMax : DistMaxClass

jeweils: +dist, -max

Equations

• Semantics.Plurality.Distributivity.DistMaxClass.distNonMax = { isDistributive := true, isMaximal := false }

def Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax : DistMaxClass

all/alle: -dist, +max

Equations

• Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax = { isDistributive := false, isMaximal := true }

def Semantics.Plurality.Distributivity.DistMaxClass.nonDistNonMax : DistMaxClass

definite plurals: -dist, -max

Equations

• Semantics.Plurality.Distributivity.DistMaxClass.nonDistNonMax = { isDistributive := false, isMaximal := false }

def Semantics.Plurality.Distributivity.distTolerantQuant {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (restrictor scope : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (restrictor a w)] [(a : Atom) → (w : W) → Decidable (scope a w)] (tol : Tolerance Atom) (x : Finset Atom) (w : W) : Prop

Hypothetical exception-tolerant DP quantifier. @cite{haslinger-etal-2025} flag this as a typology cell predicted possible by the Križ & @cite{kriz-spector-2021} framework but not attested in any known language. The non-attestation is a typological puzzle — the formal tools for non-maximality (tolerance relations) don't inherently block DP-internal quantifiers from using them.

⟦[jeder* P] Q⟧^≤ = λw.∃z[z ≤ ⊕P ∧ ∀y[y ∈ AT ∧ y ⊑ z → ⟦Q⟧^≤(w)(y)]]

Equations

• Semantics.Plurality.Distributivity.distTolerantQuant restrictor scope tol x w = ∃ z ∈ x.powerset, z.Nonempty ∧ tol.rel z x ∧ (∀ a ∈ z, restrictor a w) ∧ ∀ a ∈ z, scope a w