Algebraic Mereology

[Cha17] [Kri89] [Kri98] [Lin83]

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.

Algebraic Closure (*P)

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 [Lin83] (D.32); formulation follows [Cha17] 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.

Higher-Order Mereological Properties

@[reducible, inline]

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

Cumulative reference (CUM): P is closed under join. Grounded in mathlib's SupClosed — CUM P is SupClosed {x | P x} (the sup-closed-set predicate). Apply a CUM hypothesis directly (hC hx hy : P (x ⊔ y)); construct one with a direct lambda (fun _ hx _ hy => …), as for any SupClosed (cf. mathlib IsUpperSet.supClosed). [Lin83] (T.11); [Kri89] D 12; [Cha17] §2.3.2: CUMₛ(P) ⇔ ∀x,y. P(x) ∧ P(y) → P(x ∪ₛ y). Activities and states are canonically cumulative.

Equations

• Mereology.CUM P = SupClosed {x : α | P x}

@[reducible, inline]

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

Divisive reference (DIV): P is closed downward under ≤. Grounded in mathlib's IsLowerSet — DIV P is IsLowerSet {x | P x}. Apply a DIV hypothesis directly (hDiv hle hz : P w from hle : w ≤ z, hz : P z); construct one with a direct lambda (fun _ _ hba ha => …). Equivalently DIV P ↔ Antitone P via mathlib's isLowerSet_setOf. [Cha17] §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 = IsLowerSet {x : α | P x}

@[reducible, inline]

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

Quantized reference (QUA): no proper part of a P-entity is also P.

[Kri89] D 14: QUAₛ(P) ⇔ ∀x,y. P(x) ∧ P(y) → ¬ y ⊂ₛ x. [Cha17] §2.3.5 reformulates as ∀x,y. P(x) ∧ y < x → ¬P(y), which is propositionally equivalent ((A → B → ¬C) ↔ (A → C → ¬B)). Grounded in mathlib's IsAntichain — QUA P is IsAntichain (· ≤ ·) {x | P x} (a quantized predicate's extension is an antichain: its members are pairwise incomparable). A QUA hypothesis is applied directly as an antichain (hQ hPx hPy hne : ¬ x ≤ y); to build one from Champollion's paper form, use qua_of_forall.

Equations

• Mereology.QUA P = IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) {x : α | P x}

theorem Mereology.qua_of_forall {α : Type u_1} [PartialOrder α] {P : α → Prop} (h : ∀ (x y : α), P x → y < x → ¬P y) : QUA P

Converge Champollion's paper condition into the mathlib IsAntichain normal form: if no P-element sits strictly below another P-element, the extension is an antichain. This is the construction direction (paper form ⟹ QUA); to use a QUA hypothesis, apply it directly as an antichain. There is no QUA ⟹ ∀ x y unfold by design — that runs against the simp grain.

@[reducible, inline]

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

Mereological atom: x has no proper part — grounded as mathlib's IsMin (minimal element). [Lin83] (D.10); [Cha17] §2.2: Atom(x) ⇔ ¬∃y. y < x. This is the absolute (P-independent) notion; the P-relative one (Krifka D17, "no proper P-part") is atomize / mathlib Minimal P. No OrderBot needed — many mereological domains lack a bottom.

Equations

• Mereology.Atom x = IsMin x

theorem Mereology.Atom.eq {α : Type u_1} [PartialOrder α] {x y : α} (h : Atom x) (hy : y ≤ x) : y = x

An atom's only part is itself — the y = x elimination form of IsMin.

Key Theorems

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). [Cha17] §2.3.5: QUA and CUM are incompatible for non-singletons.

theorem Mereology.isAntichain_setOf_atom {α : Type u_1} [PartialOrder α] : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) {x : α | Atom x}

Atoms form an antichain — the absolute case of mathlib's setOf_minimal_antichain (atoms are the Minimal (fun _ => True) elements, via minimal_true). The engine behind qua_of_atom.

theorem Mereology.qua_of_atom {α : Type u_1} [PartialOrder α] {P : α → Prop} (h : ∀ ⦃x : α⦄, P x → Atom x) : QUA P

Combinator: a predicate holding only of atoms is quantized — its extension is a subset of the atoms, which form an antichain (IsAntichain.subset). Factors the recurring "atomic ⟹ QUA" pattern (mass-noun part predicates, classifier atoms).

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.cum_qua_disjoint {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hne : ∃ (x : α) (y : α), P x ∧ P y ∧ x ≠ y) : ¬(CUM P ∧ QUA P)

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

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, ⊆), grounded in mathlib's ClosureOperator via its three axioms:

• 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 := ⋯ }

Sum Homomorphism

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

A sum homomorphism preserves the join operation. [Cha17] §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' := ⋯ }

@[reducible]

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.

Overlap and Extensive Measures ([Kri98])

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

Mereological overlap: x and y share a common part. [Kri98] 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.

Classical (extensional) mereology ([Hov09])

[Hov09] catalogs the equivalent axiomatizations of classical mereology. We adopt his headline characterization: classical mereology is the partial-order parthood axioms together with type-2 fusion existence (Fusion2E) and weak supplementation (WeakSup); equivalently (Tarski) a complete Boolean algebra with the zero element removed. Overlap is Hovda's ∘, proper part is the order <, and disjointness is ¬ Overlap. Mathlib's IsLUB plays the role of Hovda's minimal upper bound Mub (minimal coincides with least under antisymmetry), so the fusion-existence axiom delivers binary sums for free.

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

Type-2 (Tarski) fusion ([Hov09] §1.1.2): t fuses the P-things iff t is an upper bound on P and every part of t overlaps some P-thing.

Equations

• Mereology.IsFusion P t = ((∀ (x : α), P x → x ≤ t) ∧ ∀ y ≤ t, ∃ (x : α), P x ∧ Mereology.Overlap y x)

class Mereology.ClassicalMereology (α : Type u_1) [PartialOrder α] : Prop

Classical (extensional) mereology ([Hov09] §3): parthood is a partial order closed under type-2 fusion of every inhabited predicate (Fusion2E) and satisfying weak supplementation (WeakSup).

• fusion_exists (P : α → Prop) : (∃ (x : α), P x) → ∃ (t : α), IsFusion P t

  Fusion2E: every inhabited predicate has a type-2 fusion.

• weak_supplementation (x y : α) : x < y → ∃ z ≤ y, ¬Overlap z x

  WeakSup: a proper part is supplemented by a disjoint part.

theorem Mereology.IsFusion.isLUB {α : Type u_1} [PartialOrder α] [ClassicalMereology α] {P : α → Prop} {t : α} (h : IsFusion P t) : IsLUB {x : α | P x} t

A type-2 fusion of P is the least upper bound of P ([Hov09] Fu2MUB): weak supplementation forces the fusion (which is by definition an upper bound) to be the least one.

theorem Mereology.IsFusion.unique {α : Type u_1} [PartialOrder α] [ClassicalMereology α] {P : α → Prop} {s t : α} (hs : IsFusion P s) (ht : IsFusion P t) : s = t

Type-2 fusions are unique ([Hov09] Fu2Uniqueness): immediate from IsFusion.isLUB and antisymmetry of the parthood order.

theorem Mereology.ClassicalMereology.exists_isLUB_pair {α : Type u_1} [PartialOrder α] [ClassicalMereology α] (a b : α) : ∃ (s : α), IsLUB {a, b} s

In a classical mereology every pair has a least upper bound (the binary sum a ⊕ b), obtained by fusing {a, b}.

@[reducible]

noncomputable def Mereology.ClassicalMereology.toSemilatticeSup {α : Type u_1} [PartialOrder α] [ClassicalMereology α] : SemilatticeSup α

The binary-sum (join-semilattice) structure carried by every classical mereology, with parthood ≤ as its order. The join a ⊔ b is the unique type-2 fusion of {a, b}; noncomputable because it is extracted by choice from the fusion-existence axiom.

Equations

• Mereology.ClassicalMereology.toSemilatticeSup = { toPartialOrder := inst✝¹, sup := fun (a b : α) => Classical.choose ⋯, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

Atomic domains (discrete orders)

The sort-level, instance-resolvable companion of QUA. An IsAtomicDomain is a PartialOrder every element of which is an Atom (IsMin) — equivalently a discrete order (a ≤ b ↔ a = b), equivalently a sort on which QUA (fun _ => True) holds. It is the single consolidation point for the "flat/atomic domain" that recurs across studies (the Student-style fixtures) and that distributive determiners (English each, the ONE_AT presupposition) require of their restrictor sort: a sort with a non-atomic element (time intervals) simply has no instance. Everything below reduces to the existing Atom/QUA/IsAntichain machinery — this class adds resolution ergonomics, not a new notion.

class Mereology.IsAtomicDomain (α : Type u_1) [PartialOrder α] : Prop

A PartialOrder all of whose elements are atoms (IsMin) — a discrete order / a ≤-antichain on the whole type.

• all_atoms (x : α) : Atom x

  Every element is an atom.

theorem Mereology.isAtomicDomain_of_le_iff_eq {α : Type u_1} [PartialOrder α] (h : ∀ (a b : α), a ≤ b ↔ a = b) : IsAtomicDomain α

A discrete order (a ≤ b ↔ a = b) is an atomic domain — the canonical way to discharge the instance for Student-style flat fixtures.

theorem Mereology.IsAtomicDomain.qua_true {α : Type u_1} [PartialOrder α] [IsAtomicDomain α] : QUA fun (x : α) => True

The whole type of an atomic domain is quantized — the sort-level face of QUA, routed through qua_of_atom.

theorem Mereology.IsAtomicDomain.eq_of_overlap {α : Type u_1} [PartialOrder α] [IsAtomicDomain α] {x y : α} (h : Overlap x y) : x = y

In an atomic domain, overlapping elements are equal (atoms are disjoint).

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

Extensive measure function: additive over non-overlapping entities. [Kri98] §2.2, eq. (7): μ(x ⊕ y) = μ(x) + μ(y) when ¬O(x,y). Examples: weight, volume, number (cardinality). Order-interval sibling: IsIntervalContent (Core/Order/IntervalContent.lean) — disjoint intervals have no interval join, so the two substrates coexist.

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

Measure phrases create QUA predicates: {x : μ(x) = n} is QUA whenever μ is an extensive measure ([Kri98] §2.2: "two kilograms of flour" is QUA because no proper part of a 2kg entity also weighs 2kg). The theorem extMeasure_qua is stated in §9 below, derived via qua_pullback.

QMOD: Quantizing Modification ([Kri89])

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. [Kri89]: 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)

@[reducible, inline]

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

Equations

• Mereology.atomize P = Minimal P

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: the P-minimal elements form an antichain (mathlib's setOf_minimal_antichain).

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

Count atoms below x, as the cardinality of the (classically finite) set of atomic parts. Used by [Cha21] for cardinality tests on plural individuals.

Equations

• Mereology.atomCount α x = {a : α | Mereology.Atom a ∧ a ≤ x}.ncard

theorem Mereology.cum_maximal_unique {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hCum : CUM P) {x y : α} (hx : Maximal P x) (hy : Maximal 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.qua_pullback {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {d : α → β} (hd : StrictMono d) {P : β → Prop} (hP : QUA P) : QUA (P ∘ d)

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 a sum homomorphism: CUM P → CUM (P ∘ d). The CUM twin of qua_pullback; wraps IsSumHom.cum_preimage.

ExtMeasure → StrictMono Bridge

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: {x | x = n} is QUA on any partial order (a subsingleton is an antichain).

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

Measure phrases are quantized: {x | μ x = n} is QUA when μ is an extensive measure ([Kri98] §2.2) — singleton_qua pulled back along μ.

theorem Mereology.qmod_qua {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [ExtMeasure α μ] (R : α → Prop) (n : ℚ) : QUA (QMOD R μ n)

Combinator: a measure-quantizing modification is quantized. QMOD R μ n ⊆ {μ = n}, an antichain by extMeasure_qua, so any subset is too (IsAntichain.subset).

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

Functional QUA propagation

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: the functional case of [Kri98] §3.3 (SINC reduces to IsSumHom + injective), where the relational qua_propagation (Krifka1998.lean) becomes qua_pullback.

CUM/QUA Pullback Interaction

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

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

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

Equations

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

Predicate disjointness and individuation perspectives

A predicate is overlapping if two distinct members share a part, and disjoint otherwise; a maximally disjoint subset is an individuation perspective ([Lan11]'s variants; [Lan20]'s disjointness thesis: counting requires a disjoint base). The null schema unions all perspectives ([SF21]). Parameterized over an arbitrary overlap relation ov (mereologically, x ⊓ y ≠ ⊥); graduated from Studies/SuttonFilip2021.lean on gaining its second consumer (Studies/Landman2020.lean).

def Mereology.OverlapPred {α : Type u_1} (ov : α → α → Prop) (P : Set α) : Prop

Two distinct members of P share a part.

Equations

• Mereology.OverlapPred ov P = ∃ x ∈ P, ∃ y ∈ P, x ≠ y ∧ ov x y

def Mereology.DisjointPred {α : Type u_1} (ov : α → α → Prop) (P : Set α) : Prop

No two distinct members of P share a part.

Equations

• Mereology.DisjointPred ov P = ¬Mereology.OverlapPred ov P

theorem Mereology.overlapPred_mono {α : Type u_1} (ov : α → α → Prop) {P Q : Set α} (h : P ⊆ Q) (hP : OverlapPred ov P) : OverlapPred ov Q

OverlapPred is monotone under inclusion.

theorem Mereology.DisjointPred.anti {α : Type u_1} (ov : α → α → Prop) {P Q : Set α} (h : P ⊆ Q) (hQ : DisjointPred ov Q) : DisjointPred ov P

A subset of a disjoint predicate is disjoint.

def Mereology.IsMaxDisjointIn {α : Type u_1} (ov : α → α → Prop) (D P : Set α) : Prop

A maximally disjoint subset of P: disjoint, and unextendable within P — an individuation perspective.

Equations

• Mereology.IsMaxDisjointIn ov D P = (D ⊆ P ∧ Mereology.DisjointPred ov D ∧ ∀ x ∈ P, x ∉ D → Mereology.OverlapPred ov (insert x D))

def Mereology.nullSchema {α : Type u_1} (ov : α → α → Prop) (P : Set α) : Set α

The null individuation schema: the union of all maximally disjoint subsets — what counts as 'one' under any perspective ([SF21] (32), after [Lan11]).

Equations

• Mereology.nullSchema ov P = {x : α | ∃ (D : Set α), Mereology.IsMaxDisjointIn ov D P ∧ x ∈ D}

theorem Mereology.overlapPred_union_of_maxDisjoint_ne {α : Type u_1} (ov : α → α → Prop) {D₁ D₂ P : Set α} (h₁ : IsMaxDisjointIn ov D₁ P) (h₂ : IsMaxDisjointIn ov D₂ P) (hne : D₁ ≠ D₂) : OverlapPred ov (D₁ ∪ D₂)

The union of two distinct maximal disjoint subsets overlaps: if x distinguishes D₂ from D₁, then D₁'s maximality makes insert x D₁ overlap, and the offending pair lies in D₁ ∪ D₂.

theorem Mereology.overlapPred_nullSchema {α : Type u_1} (ov : α → α → Prop) {D₁ D₂ P : Set α} (h₁ : IsMaxDisjointIn ov D₁ P) (h₂ : IsMaxDisjointIn ov D₂ P) (hne : D₁ ≠ D₂) : OverlapPred ov (nullSchema ov P)

If two distinct maximal disjoint subsets exist, the null schema is overlapping: null-schema counting bases are mass exactly when individuation is perspectival.

theorem Mereology.nullSchema_eq_of_disjoint {α : Type u_1} (ov : α → α → Prop) {P : Set α} (h : DisjointPred ov P) : nullSchema ov P = P

A disjoint predicate is its own unique perspective: the null schema returns it unchanged.

Conjunctive Parthood ([JR26])

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 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 ([JR26] 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

Mereological dimensions

Strictly monotone maps along which QUA pulls back — the dimension chains of [Kri89]'s linking theory (Events →θ Entities →μ ℚ), bundling the three sources of StrictMono (ExtMeasure, injective IsSumHom, compositions).

class Mereology.MereoDim {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (d : α → β) : Prop

• toStrictMono : StrictMono d

  The underlying strict monotonicity proof.

@[reducible]

def Mereology.MereoDim.ofInjSumHom {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} [hf : IsSumHom f] (hinj : Function.Injective f) : MereoDim f

Equations

• ⋯ = ⋯

theorem Mereology.MereoDim.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : β → γ} {g : α → β} (hf : MereoDim f) (hg : MereoDim g) : MereoDim (f ∘ g)

Composition of MereoDim morphisms. Captures Krifka's dimension chains: Events →θ Entities →μ ℚ gives MereoDim (μ ∘ θ) when both components are MereoDim.

Stated as a theorem (not an instance) to avoid typeclass inference loops from decomposing arbitrary composed functions.

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

QUA pullback via MereoDim: typeclass-dispatched version of qua_pullback. When [MereoDim d] is available (automatically for any ExtMeasure), QUA pulls back without manual StrictMono threading.

structure Mereology.DimensionChain {Source : Type u_1} {Inter : Type u_2} {Measure : Type u_3} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] (f : Source → Inter) (μ : Inter → Measure) : Prop

• leg₁ : MereoDim f
• leg₂ : MereoDim μ

@[reducible]

def Mereology.DimensionChain.composed {Source : Type u_1} {Inter : Type u_2} {Measure : Type u_3} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) : MereoDim (μ ∘ f)

The composed map is a MereoDim.

Equations

• ⋯ = ⋯

theorem Mereology.DimensionChain.cum_measure_unbounded {α : Type u_4} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] {P : α → Prop} (hCum : CUM P) {δ : ℚ} (hδ : 0 < δ) (hSupply : ∀ (x : α), P x → ∃ (y : α), P y ∧ ¬Overlap x y ∧ δ ≤ μ y) (x₀ : α) (hx₀ : P x₀) (M : ℚ) : ∃ (z : α), P z ∧ μ z > M