Link's algebra of plurals

Link models plural and mass reference with a join semilattice E of individuals, in which x ⊔ y is the sum of x and y. The plural closure *P of a predicate holds of the sums of its members, and the proper plural ⊕P holds of the sums that are not atoms. A materialization sends each individual to the matter it is made of and preserves sums. On finite sets of individuals, * reduces to distribution over members.

Definitions

• Mereology.properPlural P: the non-atomic elements of *P.
• Mereology.IsDistr P: P holds of atoms only.
• Mereology.Inv h P: P does not distinguish h-equivalent individuals.
• Mereology.D P x: Link's 1987 distributive operator.
• Mereology.Materialization E M: a SupHom E M, with Mereology.mPart and Mereology.mEquiv the preorder and equivalence it induces on E.
• Mereology.AtomJoinPrime E: an atom below a sum lies below a summand.
• Mereology.Individual α: Link's model, the nonempty sets of atoms under union.

Main results

• Mereology.algClosure_iff_of_atom: on an atom, *P and P agree.
• Mereology.IsDistr.of_algClosure_of_atom_le: Link's distributive inference, for join-prime atoms.
• Mereology.IsDistr.properPlural_sup, Mereology.cum_properPlural: the sum of two distinct atoms of a distributive predicate is a proper plural, and proper plurals are closed under sum.
• Mereology.algClosure_image_singleton: on finite sets of individuals, taken as singletons, * holds of exactly the nonempty subsets, Sternefeld's identification of *P with D P (15), and the full closure Mereology.FullAlgClosure, Bylinina and Nouwen's ×, of all subsets (fullAlgClosure_image_singleton).
• Mereology.card_image_fullAlgClosure, Mereology.card_image_algClosure: the pluralities of ×S have 0, …, |S| atoms and those of *S have 1, …, |S|, so only with the empty sum does a count's set of degrees reach 0.

Implementation notes

Link's model is a complete join semilattice with atoms and without a bottom; only SemilatticeSup E and Mereology.Atom are used here. The plural closure *P is Mereology.AlgClosure P, mathlib's supClosure of the extension of P. The complete atomic Boolean algebra of Landman and Champollion is a stronger assumption, which enters only through AtomJoinPrime. Schwarzschild's set-based ontology, where an individual is its singleton and sum is union, is the Finset α instance; Link's own model of nonempty sets of atoms has no bottom (Individual). Where the carrier has one, *P still excludes it unless P holds of it, and ×P adds it whatever P is.

References

• G. Link, The logical analysis of plurals and mass terms (1983)
• G. Link, Generalized quantifiers and plurals (1987)
• M. Krifka, Nominal reference, temporal constitution and quantification in event semantics (1989)
• F. Landman, Events and plurality (2000)
• L. Champollion, Parts of a whole (2017)
• L. Champollion, Distributivity in formal semantics (2019)
• R. Schwarzschild, Pluralities (1996)
• W. Sternefeld, Reciprocity and cumulative predication (1998)
• L. Bylinina and R. Nouwen, On 'zero' and semantic plurality (2018)

Predicate operators

def Mereology.properPlural {E : Type u_1} [SemilatticeSup E] (P : E → Prop) (x : E) : Prop

The proper plural ⊕P holds of the elements of *P that are not atoms (D.12).

Equations

• Mereology.properPlural P x = (Mereology.AlgClosure P x ∧ ¬Mereology.Atom x)

def Mereology.IsDistr {E : Type u_1} [SemilatticeSup E] (P : E → Prop) : Prop

A distributive predicate holds of atoms only (D.19).

Equations

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

def Mereology.Inv {E : Type u_1} {M : Type u_2} (h : E → M) (P : E → Prop) : Prop

An invariant predicate does not distinguish individuals that h identifies (D.21).

Equations

• Mereology.Inv h P = ∀ (x y : E), h x = h y → (P x ↔ P y)

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

The distributive operator D P holds of x when every atomic part of x satisfies P.

Equations

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

theorem Mereology.D_of_atom {E : Type u_1} [SemilatticeSup E] {P : E → Prop} {x : E} (hx : Atom x) (hP : P x) : D P x

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

Materialization

@[reducible, inline]

abbrev Mereology.Materialization (E : Type u_3) (M : Type u_4) [SemilatticeSup E] [SemilatticeSup M] : Type (max u_3 u_4)

A materialization (D.22) is a sum-preserving map from individuals to their portions of matter.

Equations

• Mereology.Materialization E M = SupHom E M

def Mereology.mPart {E : Type u_1} [SemilatticeSup E] {M : Type u_2} [SemilatticeSup M] (h : Materialization E M) (x y : E) : Prop

x is a material part of y (D.23) when the matter of x is part of the matter of y.

Equations

• Mereology.mPart h x y = (h x ≤ h y)

def Mereology.mEquiv {E : Type u_1} [SemilatticeSup E] {M : Type u_2} [SemilatticeSup M] (h : Materialization E M) (x y : E) : Prop

x and y are materially equivalent (D.24) when they are made of the same matter.

Equations

• Mereology.mEquiv h x y = (h x = h y)

theorem Mereology.mPart_of_le {E : Type u_1} [SemilatticeSup E] {x y : E} {M : Type u_2} [SemilatticeSup M] (h : Materialization E M) (hxy : x ≤ y) : mPart h x y

An individual part is a material part (T.2).

theorem Mereology.equivalence_mEquiv {E : Type u_1} [SemilatticeSup E] {M : Type u_2} [SemilatticeSup M] (h : Materialization E M) : Equivalence (mEquiv h)

theorem Mereology.mEquiv_iff {E : Type u_1} [SemilatticeSup E] {x y : E} {M : Type u_2} [SemilatticeSup M] (h : Materialization E M) : mEquiv h x y ↔ mPart h x y ∧ mPart h y x

theorem Mereology.Inv.iff_of_mEquiv {E : Type u_1} [SemilatticeSup E] {P : E → Prop} {x y : E} {M : Type u_2} [SemilatticeSup M] {h : Materialization E M} (hP : Inv (⇑h) P) (hxy : mEquiv h x y) : P x ↔ P y

Link's theorems

theorem Mereology.algClosure_iff_of_atom {E : Type u_1} [SemilatticeSup E] {P : E → Prop} {x : E} (hx : Atom x) : AlgClosure P x ↔ P x

On an atom, *P and P agree (T.8).

theorem Mereology.IsDistr.not_properPlural {E : Type u_1} [SemilatticeSup E] {P : E → Prop} {x : E} (hP : IsDistr P) (hx : P x) : ¬properPlural P x

No element of a distributive predicate is a proper plural (T.6).

theorem Mereology.IsDistr.properPlural_sup {E : Type u_1} [SemilatticeSup E] {P : E → Prop} {x y : E} (hP : IsDistr P) (hx : P x) (hy : P y) (hne : x ≠ y) : properPlural P (x ⊔ y)

The sum of two distinct atoms of a distributive predicate is a proper plural.

theorem Mereology.cum_properPlural {E : Type u_1} [SemilatticeSup E] {P : E → Prop} : CUM (properPlural P)

Proper plurals are closed under sum.

def Mereology.AtomJoinPrime (E : Type u_2) [SemilatticeSup E] : Prop

Atoms are join-prime when an atom below a sum lies below one of the summands, as in a Boolean algebra.

Equations

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

theorem Mereology.IsDistr.of_algClosure_of_atom_le {E : Type u_1} [SemilatticeSup E] {P : E → Prop} {x y : E} (hP : IsDistr P) (hJP : AtomJoinPrime E) (h : AlgClosure P x) (hy : Atom y) (hle : y ≤ x) : P y

If atoms are join-prime, every atomic part of an element of *P satisfies a distributive P.

Sets of individuals

In Schwarzschild's set-based ontology, pluralities are finite sets of individuals, an individual is its singleton, and sum is union.

theorem Mereology.algClosure_image_singleton {α : Type u_2} [DecidableEq α] (S : Set α) (x : Finset α) : AlgClosure (fun (x : Finset α) => x ∈ (fun (x : α) => {x}) '' S) x ↔ x.Nonempty ∧ ↑x ⊆ S

* of a set of individuals, taken as singletons, holds of exactly its nonempty subsets.

theorem Mereology.algClosure_iff_of_subset_range_singleton {α : Type u_2} [DecidableEq α] {P : Finset α → Prop} (hP : {x : Finset α | P x} ⊆ Set.range fun (x : α) => {x}) (x : Finset α) : AlgClosure P x ↔ x.Nonempty ∧ ∀ a ∈ x, P {a}

* of a predicate true of individuals only holds of the nonempty pluralities all of whose members satisfy it.

theorem Mereology.fullAlgClosure_image_singleton {α : Type u_2} [DecidableEq α] (S : Set α) (x : Finset α) : FullAlgClosure (fun (x : Finset α) => x ∈ (fun (x : α) => {x}) '' S) x ↔ ↑x ⊆ S

× of a set of individuals, taken as singletons, holds of exactly its subsets, the empty one among them.

theorem Mereology.card_image_fullAlgClosure {α : Type u_2} [DecidableEq α] {S : Set α} (h : S.Finite) : Finset.card '' {x : Finset α | FullAlgClosure (fun (x : Finset α) => x ∈ (fun (x : α) => {x}) '' S) x} = Set.Iic S.ncard

The pluralities of ×S for a finite S number 0, …, |S| atoms.

theorem Mereology.card_image_algClosure {α : Type u_2} [DecidableEq α] {S : Set α} (h : S.Finite) : Finset.card '' {x : Finset α | AlgClosure (fun (x : Finset α) => x ∈ (fun (x : α) => {x}) '' S) x} = Set.Icc 1 S.ncard

Those of *S number 1, …, |S|: without the empty sum no plurality has zero atoms.

Link's model

An individual is a nonempty set of atoms, an atom its singleton, and sum is union. The empty set is no individual, so the carrier has no bottom.

@[reducible, inline]

abbrev Mereology.Individual (α : Type u_3) : Type u_3

An individual of Link's model is a nonempty set of atoms.

Equations

• Mereology.Individual α = { s : Set α // s.Nonempty }

@[instance_reducible]

instance Mereology.instSemilatticeSupIndividual {α : Type u_2} : SemilatticeSup (Individual α)

Equations

• Mereology.instSemilatticeSupIndividual = Subtype.semilatticeSup ⋯

def Mereology.Individual.atom {α : Type u_2} (a : α) : Individual α

The atomic individual Individual.atom a is the singleton of a.

Equations

• Mereology.Individual.atom a = ⟨{a}, ⋯⟩