Documentation

Linglib.Semantics.Plurality.Distributivity

Plural Distributivity and Non-Maximality #

[KS21b] [HRSW25]

Tolerant-distributive operators and the four-cell typology of distributivity × maximality. The substrate primitives (Tolerance, distMaximal, allSatisfy, someSatisfy, noneSatisfy) live in Plurality/Basic.lean; the trivalent K&S apparatus (pluralTruthValue, homogeneity_gap_symmetric, pluralTruthValue_neg) lives in Plurality/Trivalent.lean.

Main declarations #

Implementation notes #

A tolerance relation induces a partition on pluralities: identity tolerance → exact QUD, coarser tolerance → coarser QUD.

Tolerant-distributive operator #

source
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
Instances For
    source
    @[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

    Key theorems #

    source
    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).

    source
    theorem Semantics.Plurality.Distributivity.distMaximal_forces_all {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) :
    distMaximal P x w → ∀ a ∈ x, P a w

    Maximal distributive forces all atoms to satisfy P

    source
    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

    Atom vacuity #

    source
    theorem Semantics.Plurality.Distributivity.distMaximal_singleton {Atom : Type u_1} {W : Type u_2} (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. [HRSW25] §2.3, the argument below the four-way classification.

    source
    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 Plurality/Algebra.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).

    source
    theorem Semantics.Plurality.Distributivity.distTolerant_singleton {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) (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.

    source
    theorem Semantics.Plurality.Distributivity.distTolerant_singleton_independent {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (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.

    source
    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.

    The independence result #

    source
    inductive Semantics.Plurality.Distributivity.DistMaxClass :
    Type

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

    [HRSW25] present a four-cell typology in which the two properties are argued to be orthogonal: all four cells are attested or predicted.

    Constructors:

    • .distMax — +dist, +max (English each, German jeder)
    • .distNonMax — +dist, −max (German jeweils)
    • .nonDistMax — −dist, +max (English all, German alle)
    • .nonDistNonMax — −dist, −max (definite plurals)
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Plurality.Distributivity.instDecidableEqDistMaxClass :
      DecidableEq DistMaxClass
      Equations
      source
      def Semantics.Plurality.Distributivity.instReprDistMaxClass.repr :
      DistMaxClass → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[implicit_reducible]
        instance Semantics.Plurality.Distributivity.instReprDistMaxClass :
        Repr DistMaxClass
        Equations
        source
        def Semantics.Plurality.Distributivity.DistMaxClass.isDistributive :
        DistMaxClass → Prop

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

        Equations
        Instances For
          source
          @[implicit_reducible]
          instance Semantics.Plurality.Distributivity.instDecidablePredDistMaxClassIsDistributive :
          DecidablePred DistMaxClass.isDistributive
          Equations
          source
          def Semantics.Plurality.Distributivity.DistMaxClass.isMaximal :
          DistMaxClass → Prop

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

          Equations
          Instances For
            source
            @[implicit_reducible]
            instance Semantics.Plurality.Distributivity.instDecidablePredDistMaxClassIsMaximal :
            DecidablePred DistMaxClass.isMaximal
            Equations
            source
            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. [HRSW25] flag this as a typology cell predicted possible by the Križ & [KS21b] 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
            Instances For

              distMaximal over the free Finset Atom model is exactly Link's distributive inference / star-closure ([Lin83]; Algebra.star = Mereology.AlgClosure). These two theorems discharge the distMaximal_iff_star_atoms Todo flagged in Plurality/Algebra.lean §6.

              The Algebra.distr_atom_part route does not instantiate at this carrier: the bespoke Mereology.Atom x := ∀ y ≤ x, y = x degenerates over an OrderBot lattice — only ⊥/∅ satisfies it (for nonempty x, ∅ ≤ x ∧ ∅ ≠ x falsifies it). The faithful bridge therefore runs through mathlib's IsAtom (which excludes ⊥); over Finset Atom the atoms are the singletons (Finset.isAtom_iff).

              source
              theorem Semantics.Plurality.Distributivity.distMaximal_iff_forall_atom {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) :
              distMaximal P x w ↔ ∀ (s : Finset Atom), IsAtom s → s ≤ x → ∀ a ∈ s, P a w

              distMaximal is Link's distributive inference: P holds maximally on x iff every atomic part of x satisfies P. Grounded in mathlib's IsAtom — over Finset Atom the atoms are singletons, so this is the Atom-correct restatement of distMaximal_forces_all. Holds for every x (the empty plurality has no atomic parts, so both sides are vacuous).

              source
              theorem Semantics.Plurality.Distributivity.distMaximal_iff_star_atoms {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 ↔ Mereology.AlgClosure (fun (s : Finset Atom) => ∃ (a : Atom), s = {a} ∧ P a w) x

              distMaximal is Link's star-closure ([Lin83]'s *, Algebra.star = Mereology.AlgClosure): a nonempty plurality satisfies P maximally iff it is a join of P-atoms (singletons). Discharges the Plurality/Algebra.lean §6 distMaximal_iff_star_atoms Todo; the Nonempty hypothesis carries the ⊥-exclusion (AlgClosure cannot build ∅).