Documentation

Linglib.Semantics.Plurality.Cover

Schwarzschild Covers and Partitions #

[Sch96b] [Cha17]

A cover of a plurality P is a set of nonempty subpluralities of P that jointly exhaust it ([Sch96b]). [Sch96b]'s Part operator distributes a predicate over a contextually-supplied cover (the free variable Cov), generalizing [Hig80]'s partition-based distributivity to overlapping covers — so that [Gil87]'s the men wrote musicals (Rodgers, Hammerstein, Hart; no partition works, but the overlapping cover {Rodgers⊕Hammerstein, Rodgers⊕Hart} does) comes out true.

Here covers are recast mereologically: parts are join-semilattice elements and "jointly exhaust" becomes "least upper bound = whole" — the ⊕C = X form of [Sau03] (the downstream consumer, Studies/Sauerland2003.lean), which [Cha17] also adopts, extending it to the temporal domain via stratified reference. IsFinCover and algClosure_of_finCover are the substrate [Sau03]'s distributive ∗-operator uses.

Main declarations #

Implementation notes #

A cover is an EXPLICIT decomposition; AlgClosure is the IMPLICIT closure. algClosure_iff_exists_finCover makes the two interconvertible in the finite case. Stratified reference (Semantics/Aspect/Stratified.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). The closure does not fix a unique cover — the inductive sum constructor can be applied in many orders — which is why the forward bridge yields some cover (∃), not a canonical one.

Cover #

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

Cover (mereological form): a set of parts whose least upper bound is the whole. [Sch96b] defines a cover set-theoretically — a set of nonempty subsets of the whole, with every atom in some cell; over a join-semilattice that exhaustion condition is IsLUB parts whole (isCover_iff_isLUB), the ⊕C = X form of [Sau03]. Parts may overlap; the "every part ≤ whole" condition is automatic, since the whole is by definition an upper bound.

Equations
Instances For
    source
    @[simp]
    theorem Semantics.Plurality.Cover.isCover_iff_isLUB {α : Type u_1} [Preorder α] {parts : Set α} {whole : α} :
    IsCover parts whole ↔ IsLUB parts whole

    Partition #

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

    [Sch96b] partition: a cover whose parts pairwise don't overlap — [Hig80]'s original partition-based distributivity domain, which [Sch96b] generalizes to arbitrary (possibly overlapping) covers to handle readings like [Gil87]'s the men wrote musicals. The Set-valued, possibly-infinite analogue of mathlib's Finpartition; not the Setoid-based Questions.Partition.IsPartition. Disjointness is meet-bottom, so the carrier needs Lattice + OrderBot.

    Equations
    Instances For

      Finite covers #

      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. Formalises [Sau03]'s cover condition "⊕C = X" with Finset.sup', which avoids 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
        source
        theorem Semantics.Plurality.Cover.isFinCover_iff_isCover {α : Type u_1} [SemilatticeSup α] {parts : Finset α} (h : parts.Nonempty) {whole : α} :
        IsFinCover parts h whole ↔ IsCover (↑parts) whole

        A finite cover is a cover of its underlying set, via isLUB_sup'.

        Bridge to Mereology.AlgClosure #

        AlgClosure C x (the implicit ∗-closure of C) holds iff x admits an explicit finite cover whose cells all satisfy C — [Cha17]'s Theorem 14, the algebraic core of his stratified-reference ∗-operator (∗P holds of a whole iff some cover has all cells in P). The forward direction collects the base-leaves of the closure derivation into a Finset; the reverse is Finset.sup'_induction.

        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. The reverse direction of algClosure_iff_exists_finCover.

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

        Every AlgClosure P witness is covered by an explicit finite cover whose cells satisfy P: the base-leaves of the closure derivation, merged along each sum. The forward direction of algClosure_iff_exists_finCover ([Cha17] Theorem 14).

        source
        theorem Semantics.Plurality.Cover.algClosure_iff_exists_finCover {α : Type u_1} [SemilatticeSup α] [DecidableEq α] {P : α → Prop} {whole : α} :
        Mereology.AlgClosure P whole ↔ ∃ (parts : Finset α) (hne : parts.Nonempty), IsFinCover parts hne whole ∧ ∀ p ∈ parts, P p

        [Cha17] Theorem 14. AlgClosure P x ⇔ x has an explicit finite cover with all cells in P. The implicit ∗-closure and explicit Schwarzschild decomposition coincide in the finite case.