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:

• E is a complete atomic Boolean algebra of individuals (join ⊔ᵢ, ordering ≤ᵢ)
• A ⊆ E are atoms — singular objects (this card, that ring)
• D is a join-semilattice of portions of matter
• h : E{0} → D is a semilattice homomorphism (materialization)

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

Link	Definition	Linglib
*P	Closure of P under ⊔ᵢ	Mereology.AlgClosure
⊕P	*P ∧ ¬At (proper plural)	properPlural
Distr(P)	∀x. Px → At x	Distr
Inv(P)	Closed under m-equivalent substitution	Inv
a Π b	a ≤ᵢ b (individual part)	≤
a ⊤ b	h(a) ≤ h(b) (material part)	mPart
a ~ b	h(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}.

@[reducible, inline]

abbrev Semantics.Lexical.Plural.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

• Semantics.Lexical.Plural.Link1983.star P = Mereology.AlgClosure P

def Semantics.Lexical.Plural.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

• Semantics.Lexical.Plural.Link1983.properPlural P x = (Mereology.AlgClosure P x ∧ ¬Mereology.Atom x)

def Semantics.Lexical.Plural.Link1983.Distr {E : Type u_1} [SemilatticeSup E] (P : E → Prop) : Prop

Distr(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

• Semantics.Lexical.Plural.Link1983.Distr P = ∀ (x : E), P x → Mereology.Atom x

def Semantics.Lexical.Plural.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

• Semantics.Lexical.Plural.Link1983.Inv h P = ∀ (x y : E), h x = h y → (P x ↔ P y)

structure Semantics.Lexical.Plural.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).

• h : E → D

  The materialization function.

• h_hom : Mereology.IsSumHom self.h

  h preserves join.

def Semantics.Lexical.Plural.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

• Semantics.Lexical.Plural.Link1983.mPart mat x y = (mat.h x ≤ mat.h y)

def Semantics.Lexical.Plural.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

• Semantics.Lexical.Plural.Link1983.mEquiv mat x y = (mat.h x = mat.h y)

theorem Semantics.Lexical.Plural.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.

theorem Semantics.Lexical.Plural.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.

theorem Semantics.Lexical.Plural.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.

theorem Semantics.Lexical.Plural.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.

theorem Semantics.Lexical.Plural.Link1983.T7_star_extends {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.

theorem Semantics.Lexical.Plural.Link1983.T11_star_cum {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.

theorem Semantics.Lexical.Plural.Link1983.T8_atom_of_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.

theorem Semantics.Lexical.Plural.Link1983.T8_atom_star_iff {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.

theorem Semantics.Lexical.Plural.Link1983.T9_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.

theorem Semantics.Lexical.Plural.Link1983.T6_distr_disjoint_properPlural {E : Type u_2} [SemilatticeSup E] {P : E → Prop} (hDistr : Distr 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).

theorem Semantics.Lexical.Plural.Link1983.properPlural_not_base {E : Type u_2} [SemilatticeSup E] {P : E → Prop} (hDistr : Distr P) {x : E} (hPP : properPlural P x) : ¬P x

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

def Semantics.Lexical.Plural.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

• Semantics.Lexical.Plural.Link1983.AtomJoinPrime E = ∀ (a : E), Mereology.Atom a → ∀ (x y : E), a ≤ x ⊔ y → a ≤ x ∨ a ≤ y

theorem Semantics.Lexical.Plural.Link1983.distr_atom_part {E : Type u_2} [SemilatticeSup E] {P : E → Prop} (hDistr : Distr 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).

theorem Semantics.Lexical.Plural.Link1983.distr_properPlural_extends {E : Type u_2} [SemilatticeSup E] {P : E → Prop} (_hDistr : Distr 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.

theorem Semantics.Lexical.Plural.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.