Link 1983: The Logical Analysis of Plurals and Mass Terms

[Lin83] [Kri89]

Link's model structure for the ontology of plurals and mass terms: a complete (complementary) join semi-lattice without bottom element E of individuals, with a designated subset of atoms (singular objects); a join semi-lattice D of portions of matter; and a materialization homomorphism h : E → D connecting them. The two-level structure separates individual part (the lattice ordering on E) from material part (induced by h).

(The "complete atomic Boolean algebra" framing common in subsequent literature — e.g. [Lan00], [Cha17] — is a later simplification, not Link 1983's actual ontology; see [Kri89] pp.77, 91 for the original reading.)

Main declarations

• star, properPlural, IsDistr, Inv — Link's predicate operators.
• Materialization, mPart, mEquiv — the constitution relation.
• pred_iff_star_of_atom, star_has_base_part, distr_atom_part — Link's theorems on the closure operator.

Implementation notes

Link's * IS Mereology.AlgClosure; Link's cumulative reference IS Mereology.CUM; Link's atom IS Mereology.Atom. The notation in this file (star, IsDistr, etc.) is preserved for paper-faithful legibility but is definitionally identical to the Semantics/Mereology.lean substrate. Materialization homomorphism Materialization corresponds to mathlib's SupHom and could be folded into it (Todo).

Link	Definition	Linglib
*P	closure of P under ⊔ᵢ	Mereology.AlgClosure
⊕P	*P ∧ ¬At (proper plural)	properPlural
IsDistr(P)	∀x. P x → At x	IsDistr
Inv(P)	closed under m-equivalent substitution	Inv

Todo

• Materialization could be mathlib's SupHom (a IsSumHom-carrying bundled function); the bespoke struct adds no fields beyond the hom property.
• Bridge to Distributivity.distMaximal: the Finset-side operator is the join-prime atom specialisation of distr_atom_part. Currently prose-only (§6 below); a formal distMaximal_iff_star_atoms theorem requires aligning Finset Atom with Type*-lattice carriers.

Link's predicate operators

@[reducible, inline]

abbrev Semantics.Plurality.Algebra.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.Plurality.Algebra.star P = Mereology.AlgClosure P

def Semantics.Plurality.Algebra.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.Plurality.Algebra.properPlural P x = (Mereology.AlgClosure P x ∧ ¬Mereology.Atom x)

def Semantics.Plurality.Algebra.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

• Semantics.Plurality.Algebra.IsDistr P = ∀ (x : E), P x → Mereology.Atom x

def Semantics.Plurality.Algebra.Inv {E : Type u_1} {M : Type u_2} [Preorder M] (h : E → M) (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.Plurality.Algebra.Inv h P = ∀ (x y : E), h x = h y → (P x ↔ P y)

def Semantics.Plurality.Algebra.D {E : Type u_1} [SemilatticeSup E] (P : E → Prop) (x : E) : Prop

ᴰP: Link's D operator ([Lin87b] eq. 48, p. 171): converts a (possibly non-distributive) predicate P into the distributive predicate that holds of x iff every atomic part of x satisfies P. Link's formulation ᴰVP := λx∀y[y*Πx → VP(y)] where y*Πx is "y is an atomic i-part of x", here Atom y ∧ y ≤ x.

Companion to star: where star P = AlgClosure P extends a predicate UPWARD (closure under join), D P extends it DOWNWARD to atomic parts. [Cha19a] eq. (12) recapitulates this definition and uses it as the canonical VP-level distributivity operator.

Equations

• Semantics.Plurality.Algebra.D P x = ∀ y ≤ x, Mereology.Atom y → P y

theorem Semantics.Plurality.Algebra.D_self_of_atom {E : Type u_1} [SemilatticeSup E] {P : E → Prop} {x : E} (hAtom : Mereology.Atom x) (hP : P x) : D P x

D of a P-atom is just P itself.

theorem Semantics.Plurality.Algebra.D_mono {E : Type u_1} [SemilatticeSup E] {P Q : E → Prop} (h : ∀ (x : E), P x → Q x) {x : E} (hD : D P x) : D Q x

D is monotone in P: weakening P weakens D P.

def Semantics.Plurality.Algebra.DJR {E : Type u_1} [SemilatticeSup E] (VP : E → E → Prop) (x : E) : Prop

ᴰᴶᴿVP: Link's DJR operator ([Lin87b] eq. 56, p. 173): the each-other operator. Converts a binary predicate VP (the verb relation) into a unary predicate that holds of x iff every distinct pair of atomic parts of x stands in VP. Link's formulation ᴰᴶᴿVP(x) := ∀y∀z[y, z*Πx ∧ y ≠ z → VP(y, z)].

This is the lattice-level reciprocity operator: DJR VP x IS the strong-reciprocity condition on VP over the atomic parts of x, just as D P x is the strong-distributivity condition on P. The Finset-level analog is Plurality.Reciprocal.StrongReciprocity.

Equations

• Semantics.Plurality.Algebra.DJR VP x = ∀ y ≤ x, ∀ z ≤ x, Mereology.Atom y → Mereology.Atom z → y ≠ z → VP y z

theorem Semantics.Plurality.Algebra.DJR_mono {E : Type u_1} [SemilatticeSup E] {VP VP' : E → E → Prop} (h : ∀ (y z : E), VP y z → VP' y z) {x : E} (hDJR : DJR VP x) : DJR VP' x

DJR is monotone in VP: weakening the verb relation weakens the reciprocity claim.

theorem Semantics.Plurality.Algebra.DJR_and {E : Type u_1} [SemilatticeSup E] {VP VP' : E → E → Prop} {x : E} : DJR (fun (y z : E) => VP y z ∧ VP' y z) x ↔ DJR VP x ∧ DJR VP' x

DJR distributes over conjunction in the verb relation.

The constitution relation

@[reducible, inline]

abbrev Semantics.Plurality.Algebra.Materialization (E : Type u_3) (M : Type u_4) [SemilatticeSup E] [SemilatticeSup M] : Type (max u_3 u_4)

Link's materialization (D.22): a join-homomorphism E → M from individuals to their material constitution. Defined as an abbreviation for mathlib's SupHom E M to inherit the bundled sup-preserving function API; the alias preserves the paper-faithful name used throughout [Lin83].

Equations

• Semantics.Plurality.Algebra.Materialization E M = SupHom E M

def Semantics.Plurality.Algebra.mPart {E : Type u_1} [SemilatticeSup E] {M : Type u_2} [SemilatticeSup M] (mat : Materialization E M) (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.Plurality.Algebra.mPart mat x y = (mat x ≤ mat y)

def Semantics.Plurality.Algebra.mEquiv {E : Type u_1} [SemilatticeSup E] {M : Type u_2} [SemilatticeSup M] (mat : Materialization E M) (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.Plurality.Algebra.mEquiv mat x y = (mat x = mat y)

theorem Semantics.Plurality.Algebra.iPart_implies_mPart {E : Type u_1} [SemilatticeSup E] {M : Type u_2} [SemilatticeSup M] (mat : Materialization E M) {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.Plurality.Algebra.mEquiv_equivalence {E : Type u_1} [SemilatticeSup E] {M : Type u_2} [SemilatticeSup M] (mat : Materialization E M) : Equivalence (mEquiv mat)

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

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

Material equivalence ↔ mutual material part.

theorem Semantics.Plurality.Algebra.inv_mEquiv {E : Type u_1} [SemilatticeSup E] {M : Type u_2} [SemilatticeSup M] {mat : Materialization E M} {P : E → Prop} (hInv : Inv (⇑mat) P) {x y : E} (hEq : mEquiv mat x y) : P x ↔ P y

Invariant predicates respect material equivalence by definition.

Link's theorems

theorem Semantics.Plurality.Algebra.star_of_pred {E : Type u_1} [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.Plurality.Algebra.cum_star {E : Type u_1} [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.Plurality.Algebra.pred_of_atom_star {E : Type u_1} [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.Plurality.Algebra.pred_iff_star_of_atom {E : Type u_1} [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.Plurality.Algebra.star_has_base_part {E : Type u_1} [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.Plurality.Algebra.distr_disjoint_properPlural {E : Type u_1} [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).

theorem Semantics.Plurality.Algebra.properPlural_not_base {E : Type u_1} [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.

Distributive inference (join-prime atoms)

def Semantics.Plurality.Algebra.AtomJoinPrime (E : Type u_2) [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, and follows from Link's relative- complementarity assumption on E.

Equations

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

theorem Semantics.Plurality.Algebra.distr_atom_part {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 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).

Predicate classification

theorem Semantics.Plurality.Algebra.distr_properPlural_extends {E : Type u_1} [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.

theorem Semantics.Plurality.Algebra.properPlural_cum {E : Type u_1} [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.

Connection to Finset-based distributivity

Link's IsDistr(P) (P applies to atoms only) is the mereological foundation for distMaximal in Distributivity.lean. The Finset-based 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 is correct. The connection is structural — Link works with a lattice E and atoms; distMaximal works with Finset Atom. The pointwise correspondence:

• 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

The formal bridge is proved in Distributivity.lean: distMaximal_iff_star_atoms (star form) and distMaximal_iff_forall_atom (atom form). It runs through mathlib's IsAtom, not the bespoke Atom above: over an OrderBot carrier like Finset Atom the bespoke Atom x := ∀ y ≤ x, y = x degenerates to {⊥} (only ∅ satisfies it, since ∅ ≤ x ∧ ∅ ≠ x for nonempty x), so distr_atom_part does not instantiate at the free model. IsAtom excludes ⊥, so the atoms are the singletons (Finset.isAtom_iff).

theorem Semantics.Plurality.Algebra.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

Restatement of distr_atom_part under the star alias, anticipating the Finset-side distMaximal_forces_all consumer.