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{krifka-1989} D 12; @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} [Preorder α] (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. Only requires Preorder since the definition only uses ≤.

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{krifka-1989} D 14: QUAₛ(P) ⇔ ∀x,y. P(x) ∧ P(y) → ¬ y ⊂ₛ x. @cite{champollion-2017} §2.3.5 reformulates as ∀x,y. P(x) ∧ y < x → ¬P(y), which is propositionally equivalent ((A → B → ¬C) ↔ (A → C → ¬B)). Linglib uses Champollion's form because its introduction pattern fits intro-style proofs more cleanly (assume P x and y < x, derive ¬ 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. (Compare with the causal-SEM operator Core.Causal.SEM.developDet: that operator is info-extensive but NOT order-monotone, per Schulz @cite{schulz-2011} footnote 7, so it does NOT instantiate ClosureOperator. The mereological case is genuinely closure-operator-shaped.)

• 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

theorem Mereology.Overlap.refl {γ : Type u_1} [PartialOrder γ] (x : γ) : Overlap x x

Overlap is reflexive: every element overlaps itself (via x ≤ x).

theorem Mereology.Overlap.symm {γ : Type u_1} [PartialOrder γ] {x y : γ} (h : Overlap x y) : Overlap y x

Overlap is symmetric.

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.atomize {α : Type u_1} [PartialOrder α] (P : α → Prop) : α → Prop

Atomize a predicate: restrict P to its atomic members. @cite{little-moroney-royer-2022} eq. (13): ⟦CLF⟧ = λPλx.[P(x) ∧ ¬∃y[P(y) ∧ y < x]]

In classifier-for-noun theories (@cite{chierchia-1998}; @cite{jenks-2011}; @cite{dayal-2012}; @cite{nomoto-2013}), the classifier atomizes the noun denotation so the numeral can count individual entities. This is the semantic contribution that distinguishes CLF-for-N from CLF-for-NUM.

Equations

• Mereology.atomize P x = (P x ∧ Mereology.Atom x)

theorem Mereology.atomize_sub {α : Type u_1} [PartialOrder α] {P : α → Prop} {x : α} (h : atomize P x) : P x

Atomize restricts: atomize P ⊆ P.

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

Atomized predicates are quantized: no proper part of an atom is an atom.

theorem Mereology.atomize_of_cum_is_qua {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (_hCum : CUM P) : QUA (atomize P)

Atomize turns cumulative predicates into quantized ones. This is the core of CLF-for-N semantics: the classifier takes a cumulative noun denotation (an atomic join-semilattice) and produces a quantized set of atoms suitable for counting.

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.gHomogeneous {α : Type u_1} [PartialOrder α] (P : α → Prop) : Prop

g-homogeneous reference (@cite{deal-2017}): every proper part of a P-entity has a P-part below it.

DIV → g-homogeneous (proved: div_implies_gHomogeneous)

g-Homogeneity and CUM are independent: a predicate can be g-homogeneous without being CUM (e.g., {a, b} where atoms have no proper parts — vacuously g-homogeneous — but a ⊔ b ∉ P), and CUM without being g-homogeneous (fake mass nouns, see FakeMass).

NOTE: this is a simplified version of @cite{deal-2017}'s full definition, which involves CUM conjoined with one of four conditions about minimal parts (divisive, lacking stable/non-overlapping/ non-strongly-connected minimal parts). Our formalization captures the intuitive core that Deal extracts as the common thread.

Mass nouns are g-homogeneous: every part of water contains water. Fake mass nouns (English "furniture", Shan bare nouns per @cite{moroney-2021}) are CUM but NOT g-homogeneous: a leg of a chair is part of the furniture but is not itself furniture.

Equations

• Mereology.gHomogeneous P = ∀ (x y : α), P x → y < x → ∃ z ≤ y, P z

theorem Mereology.div_implies_gHomogeneous {α : Type u_1} [PartialOrder α] {P : α → Prop} (hDiv : DIV P) : gHomogeneous P

DIV implies g-homogeneity: if every part of a P-entity is P, then a fortiori every proper part has a P-part (itself).

theorem Mereology.atom_gHomogeneous_trivial {α : Type u_1} [PartialOrder α] {P : α → Prop} {a : α} (_hP : P a) (hAtom : Atom a) (y : α) : y < a → ∃ z ≤ y, P z

g-Homogeneity is vacuously satisfied at atoms: since atoms have no proper parts, the universal condition ∀ y < a, ∃ z ≤ y, P z holds trivially.

This means g-homogeneity failures arise at non-atomic P-entities whose proper parts include non-P elements. For fake mass nouns like "furniture", the sum of two chairs is a non-atomic furniture-entity whose proper part (a chair leg) has no furniture-part below it.

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

A predicate that is cumulative but NOT g-homogeneous has "fake mass" behavior (@cite{deal-2017}; @cite{moroney-2021} §2.4): sums of P-entities are P-entities (CUM), but parts of P-entities need not contain any P-entity (failure of g-homogeneity). English "furniture" and Shan bare nouns exhibit this pattern: the sum of two chairs is furniture (CUM), but a chair leg is part of furniture without itself being furniture (¬g-homogeneous).

This is a definitional wrapper for naming the property combination.

Equations

• Mereology.FakeMass P = (Mereology.CUM P ∧ ¬Mereology.gHomogeneous P)

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).

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

A set is convex under the partial order: every element between two members is itself a member. The fixed-point of convexClosure.

Equations

• Mereology.IsConvex S = ∀ ⦃s u : α⦄, s ∈ S → u ∈ S → ∀ ⦃t : α⦄, s ≤ t → t ≤ u → t ∈ S

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

def Mereology.convexClosureOp {α : Type u_1} [PartialOrder α] : ClosureOperator (Set α)

convexClosure as a mathlib ClosureOperator (Set α). Sibling to algClosureOp.

Equations

• Mereology.convexClosureOp = { toFun := Mereology.convexClosure, monotone' := ⋯, le_closure' := ⋯, idempotent' := ⋯, isClosed_iff := ⋯ }

def Mereology.IsSubsumedBy {α : Type u_1} [Preorder α] (q p : α → Prop) : Prop

Down clause of conjunctive parthood: every element of p has a part in q. Generic poset relation; specialized in Theories/Semantics/Truthmaker/Basic.lean to content parthood.

Equations

• Mereology.IsSubsumedBy q p = ∀ (s : α), p s → ∃ (t : α), q t ∧ t ≤ s

def Mereology.Subserves {α : Type u_1} [Preorder α] (q p : α → Prop) : Prop

Up clause of conjunctive parthood: every element of q extends to an element of p.

Equations

• Mereology.Subserves q p = ∀ (s : α), q s → ∃ (t : α), p t ∧ s ≤ t

def Mereology.IsContentPart {α : Type u_1} [Preorder α] (q p : α → Prop) : Prop

Conjunctive parthood (@cite{jago-2026} Def 5): q is a content part of p iff both Down (IsSubsumedBy) and Up (Subserves) clauses hold.

Equations

• Mereology.IsContentPart q p = (Mereology.IsSubsumedBy q p ∧ Mereology.Subserves q p)

theorem Mereology.IsSubsumedBy.refl {α : Type u_1} [Preorder α] (p : α → Prop) : IsSubsumedBy p p

theorem Mereology.IsSubsumedBy.trans {α : Type u_1} [Preorder α] {p q r : α → Prop} (hpq : IsSubsumedBy p q) (hqr : IsSubsumedBy q r) : IsSubsumedBy p r

theorem Mereology.Subserves.refl {α : Type u_1} [Preorder α] (p : α → Prop) : Subserves p p

theorem Mereology.Subserves.trans {α : Type u_1} [Preorder α] {p q r : α → Prop} (hpq : Subserves p q) (hqr : Subserves q r) : Subserves p r

theorem Mereology.IsContentPart.refl {α : Type u_1} [Preorder α] (p : α → Prop) : IsContentPart p p

theorem Mereology.IsContentPart.trans {α : Type u_1} [Preorder α] {p q r : α → Prop} (hpq : IsContentPart p q) (hqr : IsContentPart q r) : IsContentPart p r

theorem Mereology.IsContentPart.subsumed {α : Type u_1} [Preorder α] {q p : α → Prop} (h : IsContentPart q p) : IsSubsumedBy q p

theorem Mereology.IsContentPart.subserves {α : Type u_1} [Preorder α] {q p : α → Prop} (h : IsContentPart q p) : Subserves q p

def Mereology.StrictPartReflecting {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → Option β) : Prop

Strict-part reflection for a partial function. A partial map f : α → Option β reflects proper parthood when every proper sub-image q' < f(x) is the image of some proper sub-input x' < x. Generic reusable formulation; specialized in Phenomena/Attitudes/Studies/BondarenkoElliott2026.lean to MSI (Mapping to Sub-parts of the Input).

Equations

• Mereology.StrictPartReflecting f = ∀ ⦃x : α⦄ ⦃q q' : β⦄, f x = some q → q' < q → ∃ x' < x, f x' = some q'

def Mereology.StrictPartPreserving {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → Option β) : Prop

Strict-part preservation for a partial function. A partial map f : α → Option β preserves proper parthood when every proper sub-input x' < x (with f x defined) yields a proper sub-image of f(x). Generic reusable formulation; specialized in Phenomena/Attitudes/Studies/BondarenkoElliott2026.lean to MSO (Mapping to Sub-parts of the Output).

Equations

• Mereology.StrictPartPreserving f = ∀ ⦃x x' : α⦄ ⦃qx : β⦄, x' < x → f x = some qx → ∃ qx' < qx, f x' = some qx'

theorem Mereology.not_isContentPart_of_singleton_not_le {α : Type u_1} [Preorder α] {q : α} {p : α → Prop} {q' : α} (hq' : p q') (h : ¬q ≤ q') : ¬IsContentPart (fun (x : α) => x = q) p

A singleton {q} is not a conjunctive part of p whenever some q' ∈ p lacks q as a sub-element (i.e., ¬ q ≤ q'). The Down clause of IsContentPart requires every p-element to have a {q}-element below it; with only q available, q ≤ q' must hold for every q' ∈ p.

Used for paper @cite{bondarenko-elliott-2026} eq. 95 to discriminate classical entailment from conjunctive parthood.