structure Semantics.Lexical.Plural.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 → Bool

  y ⪯ x: y is similar enough to x

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

  Reflexivity

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

  Tolerance implies part-of

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

Identity: only x ⪯ x (forces maximal reading)

Equations

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

def Semantics.Lexical.Plural.Distributivity.Tolerance.full {Atom : Type u_1} [DecidableEq Atom] : Tolerance Atom

Full: any part is tolerant (allows existential reading)

Equations

• Semantics.Lexical.Plural.Distributivity.Tolerance.full = { rel := fun (x y : Finset Atom) => decide (x ⊆ y), refl := ⋯, sub := ⋯ }

def Semantics.Lexical.Plural.Distributivity.distMaximal {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Bool) (x : Finset Atom) (w : W) : Bool

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

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

Equations

• Semantics.Lexical.Plural.Distributivity.distMaximal P x w = decide (∀ a ∈ x, P a w = true)

def Semantics.Lexical.Plural.Distributivity.distTolerant {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Bool) (tol : Tolerance Atom) (x : Finset Atom) (w : W) : Bool

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

This is the semantics of German "jeweils" (for non-max speakers).

Equations

• Semantics.Lexical.Plural.Distributivity.distTolerant P tol x w = decide (∃ z ∈ x.powerset, tol.rel z x = true ∧ ∀ a ∈ z, P a w = true)

theorem Semantics.Lexical.Plural.Distributivity.distMaximal_eq_identity {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) : distMaximal P x w = distTolerant P Tolerance.identity x w

Maximal distributive = tolerant distributive with identity tolerance

theorem Semantics.Lexical.Plural.Distributivity.distMaximal_forces_all {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Bool) (x : Finset Atom) (w : W) : distMaximal P x w = true → ∀ a ∈ x, P a w = true

Maximal distributive forces all atoms to satisfy P

theorem Semantics.Lexical.Plural.Distributivity.distTolerant_allows_exceptions {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) (a : Atom) (ha : a ∈ x) (hPa : P a w = true) : distTolerant P Tolerance.full x w = true

Tolerant distributive with full 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.Lexical.Plural.Distributivity.allSatisfy {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Bool) (x : Finset Atom) (w : W) : Bool

All atoms in x satisfy P at w

Equations

• Semantics.Lexical.Plural.Distributivity.allSatisfy P x w = decide (∀ a ∈ x, P a w = true)

def Semantics.Lexical.Plural.Distributivity.someSatisfy {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Bool) (x : Finset Atom) (w : W) : Bool

Some atom in x satisfies P at w

Equations

• Semantics.Lexical.Plural.Distributivity.someSatisfy P x w = decide (∃ a ∈ x, P a w = true)

def Semantics.Lexical.Plural.Distributivity.noneSatisfy {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Bool) (x : Finset Atom) (w : W) : Bool

No atom in x satisfies P at w

Equations

• Semantics.Lexical.Plural.Distributivity.noneSatisfy P x w = decide (∀ a ∈ x, P a w = false)

def Semantics.Lexical.Plural.Distributivity.pluralTruthValue {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Bool) (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.Lexical.Plural.Distributivity.pluralTruthValue_eq_true_iff {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.true ↔ allSatisfy P x w = true

pluralTruthValue is .true iff allSatisfy holds

@[simp]

theorem Semantics.Lexical.Plural.Distributivity.pluralTruthValue_eq_false_iff {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.false ↔ allSatisfy P x w = false ∧ noneSatisfy P x w = true

pluralTruthValue is .false iff noneSatisfy holds (and not allSatisfy)

@[simp]

theorem Semantics.Lexical.Plural.Distributivity.pluralTruthValue_eq_gap_iff {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.gap ↔ allSatisfy P x w = false ∧ noneSatisfy P x w = false

pluralTruthValue is .gap iff neither all nor none satisfy

theorem Semantics.Lexical.Plural.Distributivity.allSatisfy_imp_noneSatisfy_neg {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) : allSatisfy P x w = true → noneSatisfy (fun (a : Atom) (w : W) => !P a w) x w = true

If all satisfy P, then none satisfy ¬P

theorem Semantics.Lexical.Plural.Distributivity.noneSatisfy_imp_allSatisfy_neg {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) : noneSatisfy P x w = true → allSatisfy (fun (a : Atom) (w : W) => !P a w) x w = true

If none satisfy P, then all satisfy ¬P

theorem Semantics.Lexical.Plural.Distributivity.not_allSatisfy_neg_imp_not_noneSatisfy {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) : allSatisfy (fun (a : Atom) (w : W) => !P a w) x w = false → noneSatisfy P x w = false

If not all satisfy ¬P, then not none satisfy P

theorem Semantics.Lexical.Plural.Distributivity.not_noneSatisfy_neg_imp_not_allSatisfy {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) : noneSatisfy (fun (a : Atom) (w : W) => !P a w) x w = false → allSatisfy P x w = false

If not none satisfy ¬P, then not all satisfy P

def Semantics.Lexical.Plural.Distributivity.inGap {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Bool) (x : Finset Atom) (w : W) : Prop

The gap condition: some but not all atoms satisfy P

Equations

• Semantics.Lexical.Plural.Distributivity.inGap P x w = ((∃ a ∈ x, P a w = true) ∧ ∃ a ∈ x, P a w = false)

theorem Semantics.Lexical.Plural.Distributivity.homogeneity_gap_symmetric {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (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.

theorem Semantics.Lexical.Plural.Distributivity.pluralTruthValue_gap_iff_neg_gap {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (x : Finset Atom) (w : W) (_hne : x.Nonempty) : pluralTruthValue P x w = Core.Duality.Truth3.gap ↔ pluralTruthValue (fun (a : Atom) (w : W) => !P a w) x w = Core.Duality.Truth3.gap

Corollary: pluralTruthValue is gap iff negated version is gap.

theorem Semantics.Lexical.Plural.Distributivity.pluralTruthValue_neg {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] (P : Atom → W → Bool) (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.

inductive Semantics.Lexical.Plural.Distributivity.DistMaxClass : Type

Classification by [±distributive] × [±maximal]

• distMax : DistMaxClass
• distNonMax : DistMaxClass
• nonDistMax : DistMaxClass
• nonDistNonMax : DistMaxClass

instance Semantics.Lexical.Plural.Distributivity.instDecidableEqDistMaxClass : DecidableEq DistMaxClass

Equations

• Semantics.Lexical.Plural.Distributivity.instDecidableEqDistMaxClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Plural.Distributivity.instReprDistMaxClass : Repr DistMaxClass

Equations

• Semantics.Lexical.Plural.Distributivity.instReprDistMaxClass = { reprPrec := Semantics.Lexical.Plural.Distributivity.instReprDistMaxClass.repr }

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

Equations

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

def Semantics.Lexical.Plural.Distributivity.classifyOperator (forcesDistributivity usesTolerance : Bool) : DistMaxClass

All four classes are instantiated by the formal operators

Equations

• Semantics.Lexical.Plural.Distributivity.classifyOperator true false = Semantics.Lexical.Plural.Distributivity.DistMaxClass.distMax
• Semantics.Lexical.Plural.Distributivity.classifyOperator true true = Semantics.Lexical.Plural.Distributivity.DistMaxClass.distNonMax
• Semantics.Lexical.Plural.Distributivity.classifyOperator false false = Semantics.Lexical.Plural.Distributivity.DistMaxClass.nonDistMax
• Semantics.Lexical.Plural.Distributivity.classifyOperator false true = Semantics.Lexical.Plural.Distributivity.DistMaxClass.nonDistNonMax