Documentation

Linglib.Theories.Semantics.Plurality.Link1983

Link 1983: The Logical Analysis of Plurals and Mass Terms #

@cite{link-1983}

Link introduces a model structure 𝔅 = ⟨E, A, D, h⟩ for the ontology of plurals and mass terms:

The two-level structure (E vs D, connected by h) is Link's key innovation. It separates individual part (Π, the lattice ordering on E) from material part (⊀, induced by h). "The cards" and "the deck of cards" may be made of the same matter (h-equivalent) while being distinct individuals in E.

Operators #

LinkDefinitionLinglib
*PClosure of P under βŠ”α΅’Mereology.AlgClosure
βŠ•P*P ∧ Β¬At (proper plural)properPlural
IsDistr(P)βˆ€x. Px β†’ At xIsDistr
Inv(P)Closed under m-equivalent substitutionInv
a Ξ  ba ≀ᡒ b (individual part)≀
a ⊀ bh(a) ≀ h(b) (material part)mPart
a ~ bh(a) = h(b) (material equivalence)mEquiv

Connection to Existing Infrastructure #

Link's * IS Mereology.AlgClosure. Link's cumulative reference IS Mereology.CUM. Link's atom IS Mereology.Atom. This file makes the connection explicit by stating Link's theorems in terms of the existing Core/Mereology.lean definitions, correcting attributions that had previously cited only @cite{champollion-2017}.

source
@[reducible, inline]
abbrev Semantics.Plurality.Link1983.star {E : Type u_1} [SemilatticeSup E] (P : E β†’ Prop) :
E β†’ Prop

*P: Link's star operator β€” plural closure under join. β€–*Pβ€– is the complete βŠ”α΅’-subsemilattice generated by β€–Pβ€–. This IS Mereology.AlgClosure.

Equations
Instances For
    source
    def Semantics.Plurality.Link1983.properPlural {E : Type u_1} [SemilatticeSup E] (P : E β†’ Prop) (x : E) :
    Prop

    βŠ•P: the proper plural predicate (D.12). βŠ•Pa ↔ *Pa ∧ Β¬At a. If P = child', then βŠ•P = children': non-atomic sums of child-individuals.

    Equations
    Instances For
      source
      def Semantics.Plurality.Link1983.IsDistr {E : Type u_1} [SemilatticeSup E] (P : E β†’ Prop) :
      Prop

      IsDistr(P): P is a distributive predicate (D.19). Distributive predicates are true of atoms only. Common nouns like "child" and intransitive verbs like "die" are distributive. Collective predicates like "gather" are not.

      Equations
      Instances For
        source
        def Semantics.Plurality.Link1983.Inv {E : Type u_1} {D : Type u_2} [Preorder D] (h : E β†’ D) (P : E β†’ Prop) :
        Prop

        Inv(P): P is an invariant predicate (D.21). Invariant predicates are closed under substitution of materially equivalent individuals. Spatio-temporal predicates like "be-on-the-table" are invariant: "the cards are on the table" iff "the deck of cards is on the table."

        Equations
        Instances For
          source
          structure Semantics.Plurality.Link1983.Materialization (E : Type u_3) (D : Type u_4) [SemilatticeSup E] [SemilatticeSup D] :
          Type (max u_3 u_4)

          Link's materialization: a semilattice homomorphism h : E β†’ D mapping individuals to their material constitution (D.22). h commutes with join: h(x βŠ” y) = h(x) βŠ” h(y).

          Instances For
            source
            def Semantics.Plurality.Link1983.mPart {E : Type u_1} [SemilatticeSup E] {D : Type u_2} [SemilatticeSup D] (mat : Materialization E D) (x y : E) :
            Prop

            Material part (m-part) relation (D.23): x β‰€β‚˜ y ↔ h(x) ≀ h(y). "The portion of matter constituting x is part of the portion constituting y." Coarser than individual part (≀ᡒ).

            Equations
            Instances For
              source
              def Semantics.Plurality.Link1983.mEquiv {E : Type u_1} [SemilatticeSup E] {D : Type u_2} [SemilatticeSup D] (mat : Materialization E D) (x y : E) :
              Prop

              Material equivalence (D.24): x ~ y ↔ h(x) = h(y). "x and y are made of the same stuff."

              Equations
              Instances For
                source
                theorem Semantics.Plurality.Link1983.iPart_implies_mPart {E : Type u_1} [SemilatticeSup E] {D : Type u_2} [SemilatticeSup D] (mat : Materialization E D) {x y : E} (h : x ≀ y) :
                mPart mat x y

                T.2: Individual part implies material part. a Ξ  b β†’ a ⊀ b. Follows from monotonicity of h.

                source
                theorem Semantics.Plurality.Link1983.mEquiv_equivalence {E : Type u_1} [SemilatticeSup E] {D : Type u_2} [SemilatticeSup D] (mat : Materialization E D) :
                Equivalence (mEquiv mat)

                T.4 (partial): Material equivalence is an equivalence relation.

                source
                theorem Semantics.Plurality.Link1983.mEquiv_iff_mPart_both {E : Type u_1} [SemilatticeSup E] {D : Type u_2} [SemilatticeSup D] (mat : Materialization E D) {x y : E} :
                mEquiv mat x y ↔ mPart mat x y ∧ mPart mat y x

                Material equivalence ↔ mutual material part.

                source
                theorem Semantics.Plurality.Link1983.inv_mEquiv {E : Type u_1} [SemilatticeSup E] {D : Type u_2} [SemilatticeSup D] {mat : Materialization E D} {P : E β†’ Prop} (hInv : Inv mat.h P) {x y : E} (hEq : mEquiv mat x y) :
                P x ↔ P y

                Invariant predicates respect material equivalence by definition.

                source
                theorem Semantics.Plurality.Link1983.star_of_pred {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} {x : E} (h : P x) :
                star P x

                T.7: P βŠ† *P β€” every predicate is contained in its plural closure.

                source
                theorem Semantics.Plurality.Link1983.cum_star {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} :
                Mereology.CUM (star P)

                T.11: CUM(*P) β€” *P is always cumulative. If *P(x) and *P(y) then *P(x βŠ” y). This is the formal content of Link's "homogeneous reference" property.

                source
                theorem Semantics.Plurality.Link1983.pred_of_atom_star {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} {x : E} :
                Mereology.Atom x β†’ Mereology.AlgClosure P x β†’ P x

                T.8 (backward): For atoms, *P implies P. An atom cannot arise as a proper join (since a ≀ a βŠ” b forces a = a βŠ” b for atoms), so the only way AlgClosure P x can hold for an atom is via the base case.

                source
                theorem Semantics.Plurality.Link1983.pred_iff_star_of_atom {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} {x : E} (hAtom : Mereology.Atom x) :
                P x ↔ star P x

                T.8: At x β†’ (Px ↔ *Px) β€” for atoms, P and *P coincide.

                source
                theorem Semantics.Plurality.Link1983.star_has_base_part {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} {x : E} (hStar : star P x) :
                βˆƒ (y : E), P y ∧ y ≀ x

                T.9 (partial): every element of *P has a P-individual as a part. Every plural individual contains at least one base individual.

                source
                theorem Semantics.Plurality.Link1983.distr_disjoint_properPlural {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} (hDistr : IsDistr P) {x : E} (hPx : P x) :
                Β¬properPlural P x

                T.6: Distributive predicates and proper plurals are disjoint. If P is distributive (true of atoms only), then no P-individual is a proper plural (non-atomic).

                source
                theorem Semantics.Plurality.Link1983.properPlural_not_base {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} (hDistr : IsDistr P) {x : E} (hPP : properPlural P x) :
                Β¬P x

                Contrapositive of T.6: proper plurals of distributive predicates are NOT in P itself.

                source
                def Semantics.Plurality.Link1983.AtomJoinPrime (E : Type u_3) [SemilatticeSup E] :
                Prop

                Atoms are join-prime: if an atom is below a join, it is below one of the joinands. This holds in Boolean algebras and distributive lattices. Link assumes E is a complete atomic Boolean algebra (D.22), so this is always available.

                Equations
                Instances For
                  source
                  theorem Semantics.Plurality.Link1983.distr_atom_part {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} (hDistr : IsDistr P) (hJP : AtomJoinPrime E) {x : E} :
                  star P x β†’ βˆ€ {y : E}, Mereology.Atom y β†’ y ≀ x β†’ P y

                  Link's distributive inference: If P is distributive and *P(x), then every atom below x satisfies P.

                  "John, Paul, George, and Ringo are pop stars" β†’ *popStar(jβŠ•pβŠ•gβŠ•r) "Paul is a pop star" β†’ popStar(p)

                  Requires atoms to be join-prime (holds in Link's Boolean algebra).

                  source
                  theorem Semantics.Plurality.Link1983.distr_properPlural_extends {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} (_hDistr : IsDistr P) {x y : E} (hx : P x) (hy : P y) (hne : x β‰  y) :
                  properPlural P (x βŠ” y)

                  If P is distributive, then βŠ•P extends P with genuinely new entities: the join of two distinct P-atoms is a proper plural.

                  source
                  theorem Semantics.Plurality.Link1983.properPlural_cum {E : Type u_2} [SemilatticeSup E] {P : E β†’ Prop} {x y : E} (hx : properPlural P x) (hy : properPlural P y) :
                  properPlural P (x βŠ” y)

                  CUM for the proper plural βŠ•P: sums of proper plurals are proper plurals.

                  Link's IsDistr(P) β€” P applies to atoms only β€” is the mereological foundation for distMaximal in Distributivity.lean. The Finset-based operator distMaximal P x w = βˆ€a ∈ x. P(a)(w) corresponds to Link's distributive inference (distr_atom_part): if P is distributive, distributing to every atom-part and checking each is correct.

                  The connection is structural: Link works with a lattice E and atoms,
while `distMaximal` works with `Finset Atom`. The correspondence is:
- Link's atoms A βŠ† E = the type `Atom` in `Distributivity.lean`
- Link's ≀ᡒ (individual part) = Finset membership `a ∈ x`
- Link's `*P(x)` (plural closure) = "the members of x all satisfy P"
- `IsDistr(P) ∧ *P(x)` β†’ `βˆ€a atom-part-of x. P(a)` = `distMaximal P x w`
                  source
                  theorem Semantics.Plurality.Link1983.distr_star_iff_all_atoms {E : Type u_1} [SemilatticeSup E] {P : E β†’ Prop} (hDistr : IsDistr P) (hJP : AtomJoinPrime E) {x : E} :
                  star P x β†’ βˆ€ {y : E}, Mereology.Atom y β†’ y ≀ x β†’ P y

                  Link's distr_atom_part is the mereological justification for Distributivity.distMaximal. In the Finset-based setting:

                  • A Finset Atom corresponds to a plurality x ∈ E
                  • Each element a ∈ x corresponds to an atom a ≀ᡒ x
                  • distMaximal P x w = βˆ€a ∈ x. P(a)(w) checks every atom

                  For distributive predicates (IsDistr P), distr_atom_part proves this is correct: *P(x) holds iff every atom-part of x satisfies P. For collective predicates (Β¬IsDistr P), distMaximal would be too strong β€” the predicate may hold of the plurality without holding of each atom (e.g., "gathered", "surrounded").

                  The key correspondence: