Documentation

Linglib.Semantics.Plurality.Groups

Group formation and dissolution #

[Lan89] [Lan00b]

Landman's group operators over a part-of domain: up packs a plural sum into a group atom — the committee as a singular entity over its members — and down dissolves the group back into the underlying sum. The carrier is any SemilatticeSup, so the operators serve the domain of individuals and the domain of events alike ([Lan00b]); in the event domain, a symmetric verb's atomic event dissolves into the sum of its directional sub-events ([Sil12] §4.1).

Main declarations #

source
structure Semantics.Plurality.GroupStructure (E : Type u_1) [SemilatticeSup E] :
Type u_1

Landman's group structure: up packs a sum into a group atom, down recovers the underlying sum. The two laws are the operative core of [Lan89]'s postulates.

  • up : E → E

    Group formation (Landman's ↑).

  • down : E → E

    Group dissolution (Landman's ↓).

  • atom_up (x : E) : Mereology.Atom (self.up x)

    A group is an atom: it has no proper parts.

  • down_up (x : E) : self.down (self.up x) = x

    Dissolution inverts formation.

Instances For
    source
    theorem Semantics.Plurality.GroupStructure.up_injective {E : Type u_1} [SemilatticeSup E] (G : GroupStructure E) :
    Function.Injective G.up

    Distinct sums form distinct group atoms.

    A model #

    Nonempty finite subsets of β ⊕ ℕ, with sum as union: the β-singletons are the ordinary atoms, and packing recruits a fresh ℕ-marked singleton for each plurality, so groups are atoms of the same domain.

    source
    @[instance_reducible]
    instance Semantics.Plurality.GroupStructure.instSemilatticeSupSubtypeFinsetNonemptyOfDecidableEq {α : Type u_2} [DecidableEq α] :
    SemilatticeSup { F : Finset α // F.Nonempty }
    Equations
    source
    @[simp]
    theorem Semantics.Plurality.GroupStructure.coe_sup {α : Type u_2} [DecidableEq α] (x y : { F : Finset α // F.Nonempty }) :
    ↑(x ⊔ y) = ↑x ∪ ↑y
    source
    @[instance_reducible]
    instance Semantics.Plurality.GroupStructure.instDecidablePredFinsetNonempty {α : Type u_3} :
    DecidablePred fun (F : Finset α) => F.Nonempty
    Equations
    source
    def Semantics.Plurality.GroupStructure.modelUp {β : Type u_2} [Encodable β] (x : { F : Finset (β ⊕ ℕ) // F.Nonempty }) :
    { F : Finset (β ⊕ ℕ) // F.Nonempty }

    Group formation in the model: the fresh marker singleton indexed by the plurality's code.

    Equations
    Instances For
      source
      theorem Semantics.Plurality.GroupStructure.modelUp_injective {β : Type u_2} [Encodable β] :
      Function.Injective modelUp
      source
      noncomputable def Semantics.Plurality.GroupStructure.finsetModel (β : Type u_3) [DecidableEq β] [Encodable β] :
      GroupStructure { F : Finset (β ⊕ ℕ) // F.Nonempty }

      Landman's group operators are consistent: the nonempty finite subsets of β ⊕ ℕ carry a GroupStructure, with dissolution recovering the packed plurality from the marker's code.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Semantics.Plurality.GroupStructure.finsetModel_up {β : Type u_2} [Encodable β] [DecidableEq β] (x : { F : Finset (β ⊕ ℕ) // F.Nonempty }) :
        (finsetModel β).up x = modelUp x