Algebraic Mereology

@cite{champollion-2017} @cite{krifka-1989} @cite{krifka-1998} @cite{link-1983}

Framework-agnostic mereological infrastructure formalized over Mathlib's SemilatticeSup (binary join = mereological sum ⊕) and PartialOrder (part-of = ≤). All definitions are polymorphic over any semilattice, making them usable for entities, events, times, paths, or any domain with part-whole structure.

Sections

1. Algebraic Closure (*P)
2. Higher-Order Properties: CUM, DIV, QUA, Atom
3. Key Theorems (CUM/DIV/QUA interactions)
4. Sum Homomorphism
5. Overlap and Extensive Measures (@cite{krifka-1998} §2.2)
6. QMOD: Quantizing Modification
7. Maximality and Atom Counting
8. QUA/CUM Pullback (contravariant functoriality)
9. ExtMeasure → StrictMono Bridge
10. IsSumHom + Injective → StrictMono
11. Functional QUA propagation
12. CUM/QUA Pullback Interaction

inductive Mereology.AlgClosure {α : Type u_1} [SemilatticeSup α] (P : α → Prop) : α → Prop

Algebraic closure of a predicate P under join (⊔): *P is the smallest set containing P and closed under ⊔. Originates in @cite{link-1983} (D.32); formulation follows @cite{champollion-2017} Ch. 2.

• base {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {x : α} : P x → AlgClosure P x

  Base case: everything in P is in *P.

• sum {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {x y : α} : AlgClosure P x → AlgClosure P y → AlgClosure P (x ⊔ y)

  Closure: if x, y ∈ *P then x ⊔ y ∈ *P.

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

Cumulative reference (CUM): P is closed under join. @cite{link-1983} (T.11); @cite{champollion-2017} §2.3.2: CUM(P) ⇔ ∀x,y. P(x) ∧ P(y) → P(x ⊕ y). Activities and states are canonically cumulative.

Equations

• Mereology.CUM P = ∀ (x y : α), P x → P y → P (x ⊔ y)

def Mereology.DIV {α : Type u_1} [PartialOrder α] (P : α → Prop) : Prop

Divisive reference (DIV): P is closed downward under ≤. @cite{champollion-2017} §2.3.3: DIV(P) ⇔ ∀x,y. P(x) ∧ y ≤ x → P(y). This is the mereological analog of the subinterval property.

Equations

• Mereology.DIV P = ∀ (x y : α), P x → y ≤ x → P y

def Mereology.QUA {α : Type u_1} [PartialOrder α] (P : α → Prop) : Prop

Quantized reference (QUA): no proper part of a P-entity is also P. @cite{champollion-2017} §2.3.5: QUA(P) ⇔ ∀x,y. P(x) ∧ y < x → ¬P(y). Telic predicates are canonically quantized.

Equations

• Mereology.QUA P = ∀ (x y : α), P x → y < x → ¬P y

def Mereology.Atom {α : Type u_1} [PartialOrder α] (x : α) : Prop

Mereological atom: x has no proper part. @cite{link-1983} (D.10, D.22 condition 2); @cite{champollion-2017} §2.2: Atom(x) ⇔ ¬∃y. y < x. Defined without OrderBot since many domains lack a natural bottom element.

Equations

• Mereology.Atom x = ∀ y ≤ x, y = x

theorem Mereology.algClosure_cum {α : Type u_1} [SemilatticeSup α] {P : α → Prop} : CUM (AlgClosure P)

*P is always cumulative. This is the fundamental property of algebraic closure.

theorem Mereology.subset_algClosure {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {x : α} (h : P x) : AlgClosure P x

P ⊆ *P: algebraic closure extends the original predicate.

theorem Mereology.algClosure_has_base {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {x : α} (h : AlgClosure P x) : ∃ (a : α), P a ∧ a ≤ x

Every element of *P has a base element below it: if x ∈ *P, then ∃ a ∈ P, a ≤ x. Useful for extracting witnesses from algebraic closures.

theorem Mereology.algClosure_of_cum {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hCUM : CUM P) {x : α} : AlgClosure P x ↔ P x

Closure of a cumulative predicate is itself: *P = P when CUM(P). Mass nouns and bare plurals are already cumulative, so closure is a no-op — the key to Krifka's absorption rule ⊔⊔S = ⊔S.

theorem Mereology.qua_cum_incompatible {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hQ : QUA P) {x y : α} (hx : P x) (hy : P y) (hne : x ≠ y) : ¬CUM P

QUA predicates cannot be cumulative (for predicates with ≥ 2 elements). @cite{champollion-2017} §2.3.5: QUA and CUM are incompatible for non-singletons.

theorem Mereology.atom_qua {α : Type u_1} [PartialOrder α] {x : α} (hAtom : Atom x) : QUA fun (x_1 : α) => x_1 = x

Atoms are trivially quantized: the singleton {x} is QUA when x is an atom.

theorem Mereology.div_closed_under_le {α : Type u_1} [PartialOrder α] {P : α → Prop} (hDiv : DIV P) {z : α} (hz : P z) {w : α} (hle : w ≤ z) : P w

DIV allows extracting parts: if P is DIV and P(z), then P(w) for any w ≤ z.

theorem Mereology.cum_qua_disjoint {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hne : ∃ (x : α) (y : α), P x ∧ P y ∧ x ≠ y) : ¬(CUM P ∧ QUA P)

CUM and QUA partition event predicates (for non-trivial predicates): a predicate with ≥ 2 distinct elements cannot be both CUM and QUA. @cite{champollion-2017} §2.3.5.

theorem Mereology.algClosure_of_mem {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {x : α} (h : P x) : AlgClosure P x

AlgClosure preserves membership: if P x, then AlgClosure P x.

theorem Mereology.algClosure_mono {α : Type u_1} [SemilatticeSup α] {P Q : α → Prop} (h : ∀ (x : α), P x → Q x) (x : α) : AlgClosure P x → AlgClosure Q x

AlgClosure is monotone: P ⊆ Q implies *P ⊆ *Q.

theorem Mereology.algClosure_idempotent {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (x : α) : AlgClosure (AlgClosure P) x → AlgClosure P x

AlgClosure is idempotent: *(∗P) = *P.

def Mereology.algClosureOp {α : Type u_1} [SemilatticeSup α] : ClosureOperator (α → Prop)

AlgClosure is a closure operator on the predicate lattice (α → Prop, ⊆).

The three axioms — extensive, monotone, idempotent — are grounded in Mathlib's ClosureOperator. This is the mereological analog of CausalClosure.PositiveDynamics.closureOp: both are monads on Pos (the category of posets and monotone maps).

• subset_algClosure → le_closure' (extensive)
• algClosure_mono → monotone' (monotone)
• algClosure_idempotent + subset_algClosure → idempotent'

Equations

• Mereology.algClosureOp = { toFun := Mereology.AlgClosure, monotone' := ⋯, le_closure' := ⋯, idempotent' := ⋯, isClosed_iff := ⋯ }

class Mereology.IsSumHom {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : α → β) : Prop

A sum homomorphism preserves the join operation. @cite{champollion-2017} §2.5: thematic roles and τ are sum homomorphisms. f(x ⊕ y) = f(x) ⊕ f(y).

• map_sup (x y : α) : f (x ⊔ y) = f x ⊔ f y

  f preserves binary join.

def Mereology.IsSumHom.toSupHom {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : IsSumHom f) : SupHom α β

Convert an IsSumHom witness to Mathlib's bundled SupHom.

This grounds linglib's unbundled IsSumHom typeclass in Mathlib's bundled SupHom α β, the hom-set in SLat (join semilattices with join-preserving maps).

Equations

• hf.toSupHom = { toFun := f, map_sup' := ⋯ }

def Mereology.SupHom.toIsSumHom {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) : IsSumHom f.toFun

Every Mathlib SupHom satisfies IsSumHom.

Equations

• ⋯ = ⋯

theorem Mereology.IsSumHom.monotone {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : IsSumHom f) : Monotone f

Sum homomorphisms are order-preserving (monotone). If x ≤ y then f(x) ≤ f(y).

theorem Mereology.IsSumHom.cum_preimage {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : IsSumHom f) {P : β → Prop} (hCum : CUM P) : CUM (P ∘ f)

Sum homomorphisms preserve CUM: if P is CUM then P ∘ f⁻¹ is CUM. More precisely: if P is CUM then (fun x => P (f x)) is CUM.

def Mereology.Overlap {γ : Type u_1} [PartialOrder γ] (x y : γ) : Prop

Mereological overlap: x and y share a common part. @cite{krifka-1998} eq. (1e): O(x, y) ⇔ ∃z. z ≤ x ∧ z ≤ y.

Equations

• Mereology.Overlap x y = ∃ z ≤ x, z ≤ y

class Mereology.ExtMeasure (α : Type u_1) [SemilatticeSup α] (μ : α → ℚ) : Prop

Extensive measure function: additive over non-overlapping entities. @cite{krifka-1998} §2.2, eq. (7): μ(x ⊕ y) = μ(x) + μ(y) when ¬O(x,y). Examples: weight, volume, number (cardinality).

• additive (x y : α) : ¬Overlap x y → μ (x ⊔ y) = μ x + μ y

  Additivity: μ is additive over non-overlapping entities.

• positive (x : α) : 0 < μ x

  Positivity: every entity has positive measure.

• strict_mono (x y : α) : y < x → μ y < μ x

  Strict monotonicity: proper parts have strictly smaller measure. In a CEM with complementation, this follows from additivity + positivity: y < x implies x = y ⊔ z with ¬O(y,z), so μ(x) = μ(y) + μ(z) > μ(y). We axiomatize it directly since SemilatticeSup lacks complementation.

theorem Mereology.extMeasure_qua {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] (n : ℚ) (_hn : 0 < n) : QUA fun (x : α) => μ x = n

Measure phrases create QUA predicates: {x : μ(x) = n} is QUA whenever μ is an extensive measure. @cite{krifka-1998} §2.2: "two kilograms of flour" is QUA because no proper part of a 2kg entity also weighs 2kg.

def Mereology.QMOD {α : Type u_1} {μTy : Type u_2} (R : α → Prop) (μ : α → μTy) (n : μTy) : α → Prop

Quantizing modification: intersect predicate R with a measure constraint. @cite{krifka-1989}: QMOD(R, μ, n) = λx. R(x) ∧ μ(x) = n. "three kilos of rice" = QMOD(rice, μ_kg, 3). This is the operation that turns a CUM mass noun into a QUA measure phrase.

Equations

• Mereology.QMOD R μ n x = (R x ∧ μ x = n)

theorem Mereology.qmod_sub {α : Type u_1} {μTy : Type u_2} {R : α → Prop} {μ : α → μTy} {n : μTy} {x : α} (h : QMOD R μ n x) : R x

QMOD(R, μ, n) ⊆ R: quantizing modification restricts the base predicate.

def Mereology.isMaximal {α : Type u_1} [PartialOrder α] (P : α → Prop) (x : α) : Prop

Maximal in P under ≤: x is in P and no proper extension of x is in P. Used by @cite{charlow-2021} for the M_v operator (mereological maximization).

Equations

• Mereology.isMaximal P x = (P x ∧ ∀ (y : α), P y → x ≤ y → x = y)

noncomputable def Mereology.atomCount (α : Type u_1) [PartialOrder α] [Fintype α] (x : α) : ℕ

Count atoms below x, using classical decidability. Used by @cite{charlow-2021} for cardinality tests on plural individuals.

Equations

• Mereology.atomCount α x = {a : α | decide (Mereology.Atom a ∧ a ≤ x) = true}.card

theorem Mereology.cum_maximal_unique {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hCum : CUM P) {x y : α} (hx : isMaximal P x) (hy : isMaximal P y) : x = y

If P is CUM and x, y are both maximal in P, then x = y. Cumulative predicates have at most one maximal element: the join of all P-elements.

theorem Mereology.atomCount_sup_disjoint (α : Type u_1) [SemilatticeSup α] [Fintype α] (hJP : ∀ (a : α), Atom a → ∀ (u v : α), a ≤ u ⊔ v → a ≤ u ∨ a ≤ v) {x y : α} (hDisj : ¬Overlap x y) : atomCount α (x ⊔ y) = atomCount α x + atomCount α y

Atom count is additive over non-overlapping sums, provided atoms are join-prime (i.e., a ≤ x ⊔ y → a ≤ x ∨ a ≤ y for atoms a). Join-primality holds in distributive lattices but fails in general semilattices (e.g., the M₃ lattice).

theorem Mereology.qua_pullback {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {d : α → β} (hd : StrictMono d) {P : β → Prop} (hP : QUA P) : QUA (P ∘ d)

QUA pullback along strictly monotone maps.

If d : α → β is strictly monotone and P is quantized over β, then P ∘ d is quantized over α. This is the general theorem subsuming both extMeasure_qua (where d = μ) and the functional version of qua_propagation (where d = θ as a function).

Categorically: QUA is a contravariant functor from the category of partially ordered types with StrictMono morphisms to Prop.

The relational qua_propagation in Krifka1998.lean (using MSO + UP on a binary relation θ) is genuinely different — it operates on relations, not functions. Both coexist: the functional case is a special case of this theorem.

theorem Mereology.cum_pullback {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {d : α → β} (hd : IsSumHom d) {P : β → Prop} (hP : CUM P) : CUM (P ∘ d)

CUM pullback along sum homomorphisms.

If d : α → β is a sum homomorphism and P is cumulative over β, then P ∘ d is cumulative over α. Wrapper for IsSumHom.cum_preimage, named for symmetry with qua_pullback.

Categorically: CUM is a contravariant functor from the category of join semilattices with IsSumHom morphisms to Prop.

theorem Mereology.extMeasure_strictMono {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} (hμ : ExtMeasure α μ) : StrictMono μ

Extract StrictMono from an extensive measure. ExtMeasure.strict_mono axiomatizes that proper parts have strictly smaller measure; this is exactly StrictMono μ.

theorem Mereology.singleton_qua {α : Type u_1} [PartialOrder α] (n : α) : QUA fun (x : α) => x = n

Singleton predicates are quantized on any partial order. {x | x = n} is QUA because y < n → y ≠ n (by irreflexivity of < after substitution).

This generalizes atom_qua, which required Atom x. The Atom hypothesis is unnecessary for singletons.

theorem Mereology.extMeasure_qua' {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] (n : ℚ) : QUA fun (x : α) => μ x = n

extMeasure_qua derived from qua_pullback + singleton_qua. This shows that extMeasure_qua is a special case of QUA pullback:

{x | μ(x) = n} = (· = n) ∘ μ

and QUA pulls back along the StrictMono map μ.

Note: unlike the original extMeasure_qua, this derivation does not require 0 < n. The positivity hypothesis was an artifact of the direct proof; the pullback route is strictly more general.

The original extMeasure_qua is preserved for backward compatibility.

theorem Mereology.qua_pullback_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {d₁ : α → β} {d₂ : β → γ} (hd₁ : StrictMono d₁) (hd₂ : StrictMono d₂) {P : γ → Prop} (hP : QUA P) : QUA (P ∘ d₂ ∘ d₁)

QUA pullback composes: if d₁ : α → β and d₂ : β → γ are both StrictMono, then QUA P → QUA (P ∘ d₂ ∘ d₁).

This captures the Krifka dimension chain: Events →θ Entities →μ ℚ where θ extracts the incremental theme and μ measures it. The composition μ ∘ θ is StrictMono, so QUA predicates on ℚ (measure phrases like "two kilograms") pull back to QUA predicates on Events (telic VPs like "eat two kilograms of flour").

theorem Mereology.IsSumHom.strictMono_of_injective {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : IsSumHom f) (hinj : Function.Injective f) : StrictMono f

A sum homomorphism that is injective is strictly monotone.

IsSumHom.monotone gives Monotone f (x ≤ y → f(x) ≤ f(y)). Adding injectivity strengthens this: x < y means x ≤ y ∧ x ≠ y, so f(x) ≤ f(y) ∧ f(x) ≠ f(y), i.e., f(x) < f(y).

This bridges IsSumHom (the CUM pullback morphism class) to StrictMono (the QUA pullback morphism class): an injective sum homomorphism supports both CUM and QUA pullback.

Linguistically: a sum-homomorphic thematic role that is also injective (unique participant assignment, Krifka's UE/UO conditions) supports telicity transfer via qua_pullback.

theorem Mereology.qua_of_injective_sumHom {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : IsSumHom f) (hinj : Function.Injective f) {P : β → Prop} (hP : QUA P) : QUA (P ∘ f)

QUA propagation through an injective sum homomorphism.

When the relational θ in Krifka's qua_propagation (Krifka1998.lean) is actually a function f with IsSumHom + injectivity, the relational proof (needing UP + MSO) reduces to functional qua_pullback via StrictMono.

This is the functional special case of @cite{krifka-1998} §3.3: SINC(θ) ∧ QUA(OBJ) → QUA(VP θ OBJ), where θ is a function rather than a relation, and SINC reduces to IsSumHom + Injective.

See also: qua_propagation in Krifka1998.lean for the relational version using UP + MSO + UO.

theorem Mereology.cum_qua_dimension_disjoint {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} {P : β → Prop} {x y : α} (hx : (P ∘ f) x) (hy : (P ∘ f) y) (hne : x ≠ y) : ¬(CUM (P ∘ f) ∧ QUA (P ∘ f))

CUM/QUA incompatibility is preserved through composition.

If P ∘ f has two distinct witnesses x ≠ y, then P ∘ f cannot be both CUM and QUA. This is cum_qua_disjoint instantiated to the composed predicate.

def Mereology.convexClosure {α : Type u_1} [PartialOrder α] (S : Set α) : Set α

Convex closure under a partial order: add all elements "in between" existing members. z is in-between x and y if x ≤ z ≤ y. @cite{kriz-spector-2021} def. 21: Conv_⊑(A) is the smallest superset of A such that for any x, y ∈ A, every z with x ⊑ z ⊑ y is also in Conv_⊑(A). One step suffices because ⊑ is transitive.

Equations

• Mereology.convexClosure S = {c : α | ∃ a ∈ S, ∃ b ∈ S, a ≤ c ∧ c ≤ b}

theorem Mereology.subset_convexClosure {α : Type u_1} [PartialOrder α] (S : Set α) : S ⊆ convexClosure S

S ⊆ convexClosure S.

theorem Mereology.convexClosure_idempotent {α : Type u_1} [PartialOrder α] (S : Set α) : convexClosure (convexClosure S) = convexClosure S

convexClosure is idempotent: Conv(Conv(S)) = Conv(S). If c ∈ Conv(Conv(S)), then a₁ ≤ c ≤ b₂ for some a₁, b₂ ∈ S.

theorem Mereology.convexClosure_mono {α : Type u_1} [PartialOrder α] {S T : Set α} (h : S ⊆ T) : convexClosure S ⊆ convexClosure T

Convex closure is monotone: S ⊆ T → Conv(S) ⊆ Conv(T).