Plurality — Shared substrate

[KS21b] [HRSW25]

Substrate primitives shared across all theoretical accounts of plural predication in this directory: a tolerance relation on Finset Atom (controlling exception tolerance), the basic distribution operators distMaximal/allSatisfy/someSatisfy/noneSatisfy, and their decidability instances. Specialised operators (distTolerant, trivalent K&S apparatus, Bar-Lev existPL, etc.) live in sibling files.

Main declarations

• Tolerance — reflexive, sub-plurality-respecting relation on Finset Atom.
• Tolerance.identity, Tolerance.trivial — the two anchor instances used by downstream Studies.
• distMaximal — ∀ a ∈ x, P a w. The maximal-distribution predicate.
• allSatisfy — alias of distMaximal (kept under its K&S-paper-faithful name for legibility in study files).
• someSatisfy, noneSatisfy — existential and universal-negation duals.

Implementation notes

This file sits under namespace Semantics.Plurality (the directory umbrella) rather than Semantics.Plurality.Basic (filename pattern). Consumers open Semantics.Plurality for substrate access; specific theoretical accounts (Distributivity, Trivalent, Implicature, Cumulativity, …) live under sub-namespaces and are opened separately.

Tolerance relations

structure Semantics.Plurality.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 sub-plurality.

@[implicit_reducible]

instance Semantics.Plurality.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.Tolerance.identity {Atom : Type u_1} [DecidableEq Atom] : Tolerance Atom

Identity tolerance: only x ⪯ x (forces maximal reading).

Equations

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

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

Trivial tolerance: any sub-plurality is tolerated (allows existential reading). [KS21b] call this the trivial tolerance — the relation is just sub-pluralityhood, with no further restriction.

Equations

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

Basic plural predicates

def Semantics.Plurality.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. The semantics of English each, German jeder.

Equations

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

@[implicit_reducible]

instance Semantics.Plurality.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.distMaximal.instDecidable P x w = id inferInstance

def Semantics.Plurality.allSatisfy {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

All atoms in x satisfy P at w. Alias of distMaximal — kept under its K&S-paper-faithful name for legibility in study files; consumers may use either.

Equations

• Semantics.Plurality.allSatisfy P x w = Semantics.Plurality.distMaximal P x w

@[implicit_reducible]

instance Semantics.Plurality.allSatisfy.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 (allSatisfy P x w)

Equations

• Semantics.Plurality.allSatisfy.instDecidable P x w = Semantics.Plurality.allSatisfy.instDecidable._aux_1 P x w

def Semantics.Plurality.someSatisfy {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

Some atom in x satisfies P at w.

Equations

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

@[implicit_reducible]

instance Semantics.Plurality.someSatisfy.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 (someSatisfy P x w)

Equations

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

def Semantics.Plurality.noneSatisfy {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

No atom in x satisfies P at w.

Equations

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

@[implicit_reducible]

instance Semantics.Plurality.noneSatisfy.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 (noneSatisfy P x w)

Equations

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