Documentation

Linglib.Theories.Semantics.Plurality.Cover

Schwarzschild Covers and Partitions #

@cite{schwarzschild-1996} @cite{champollion-2017}

A cover of a plural entity x is a set of parts of x whose least upper bound is x itself. @cite{schwarzschild-1996} introduces covers to model nonatomic distributivity: when "the shoes cost fifty dollars" distributes over PAIRS of shoes (not individual shoes), the distributivity operator is anaphoric on a contextually-salient cover of the shoes by pairs.

@cite{champollion-2017} Ch 8 §8.1: "[Schwarzschild] models this by making the distributivity operator anaphoric on such a cover, and renaming it the Part operator." Champollion adopts this strategy and extends it to the temporal domain in Ch 8 §8.3.

Mathlib grounding #

A cover is mathematically just IsLUB parts whole: every member of parts is below whole (upper bound) and whole is the least such. The "cover" terminology is preserved here for direct grounding in the linguistics literature. Partitions add pairwise disjointness via Set.PairwiseDisjoint.

For finite covers (the typical linguistic case where the salient set of parts is enumerable), use IsFinCover which avoids the LUB abstraction in favor of Finset.sup'.

Relation to Mereology.AlgClosure #

A cover is an EXPLICIT decomposition; AlgClosure is the IMPLICIT closure. Champollion's stratified reference (StratifiedReference.lean) uses AlgClosure because the strata are existentially closed; covers are the right primitive when the parts must be supplied (anaphoric distributivity, contextually-salient partitions).

Consumer status #

This file currently has no Lean import consumers — only a docstring mention in Phenomena/Anaphora/Studies/Sternefeld1998.lean. The substrate is structurally sound (the @cite{schwarzschild-1996}-AlgClosure bridge algClosure_of_finCover is the natural API any anaphoric-distributivity Studies file would consume). Queued: a Studies file landing the Schwarzschild-style anaphoric distributivity examples would activate this substrate (@cite{champollion-2017} Ch 8 §8.1 on the Part operator is the natural anchor).

source
@[reducible, inline]
abbrev Semantics.Plurality.Cover.IsCover {α : Type u_1} [Preorder α] (parts : Set α) (whole : α) :
Prop

@cite{schwarzschild-1996} cover: a set of parts whose least upper bound is the whole. Parts may overlap.

Mathematically equivalent to mathlib's IsLUB parts whole; the cover terminology is preserved for the linguistics literature.

The "every part is ≤ whole" condition is automatic from IsLUB (whole is by definition an upper bound).

Equations
Instances For
    source
    theorem Semantics.Plurality.Cover.isCover_singleton {α : Type u_1} [Preorder α] (x : α) :
    IsCover {x} x

    The whole is its own one-element cover (trivial cover).

    source
    theorem Semantics.Plurality.Cover.isCover_pair {α : Type u_1} [SemilatticeSup α] (x y : α) :
    IsCover {x, y} (x ⊔ y)

    Two-part cover: when whole = x ⊔ y in a join semilattice, {x, y} is a cover of whole. The minimal nontrivial case.

    source
    def Semantics.Plurality.Cover.IsPartition {α : Type u_1} [Lattice α] [OrderBot α] (parts : Set α) (whole : α) :
    Prop

    @cite{schwarzschild-1996} partition: a cover whose parts are pairwise disjoint. Used by atomic distributivity (the special atomic case of @cite{schwarzschild-1996}) where each plural element distributes to a unique cell of the partition.

    "Disjoint" here is meet-bottom; requires the carrier to have a SemilatticeInf and OrderBot.

    Equations
    Instances For
      source
      def Semantics.Plurality.Cover.IsFinCover {α : Type u_1} [SemilatticeSup α] (parts : Finset α) (h : parts.Nonempty) (whole : α) :
      Prop

      Finite cover: the typical linguistic case where the contextually salient set of parts is enumerable. Uses Finset.sup' to avoid the OrderBot requirement of Finset.sup.

      Example: in the shoes cost fifty dollars with the salient cover "by pairs of shoes", the cover is the finite set of pairs.

      Equations
      Instances For

        Cover-witness implies AlgClosure-membership #

        If parts is a finite cover of whole and every part satisfies a predicate P, then whole is in the algebraic closure of P. This is the bridge from explicit Schwarzschild-style decomposition (covers) to Champollion-style implicit closure (*P).

        The reverse direction (AlgClosure → cover) is non-trivial — AlgClosure witnesses are not unique covers, since the inductive sum constructor can be applied in many orders.

        source
        theorem Semantics.Plurality.Cover.algClosure_of_finCover {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {parts : Finset α} {h : parts.Nonempty} {whole : α} (hCover : IsFinCover parts h whole) (hP : ∀ p ∈ parts, P p) :
        Mereology.AlgClosure P whole

        A finite cover whose parts all satisfy P witnesses AlgClosure P whole.