Algebraic mereology

Algebraic semantics models parthood as a partial order and mereological sum as join. The reference properties of predicates are then mathlib set predicates: cumulativity is SupClosed, divisiveness IsLowerSet and quantization IsAntichain (· ≤ ·), and Link's closure *P is supClosure. A carrier may have a null individual, as a Boolean algebra does, or none, as a classical mereology does. Atoms and overlap are stated relative to mathlib's IsBot, so on an OrderBot carrier they are IsAtom and ¬ Disjoint.

Main definitions

• CUM, DIV, QUA: cumulative, divisive and quantized reference.
• AlgClosure P: the closure of P under binary sum, and FullAlgClosure P with the empty sum.
• Atom, Overlap, IsPlural, atomCount: atoms, overlap, proper pluralities, and the number of atoms below an element.
• HasRemainders α: every proper part is completed to the whole by a non-overlapping part.
• IsClassicalMereology α: classical extensional mereology, in which every inhabited predicate has a unique sum.
• IsExtensiveMeasure μ: extensive measure functions, and the measure phrases QMOD they build.
• OverlapPred, DisjointPred, IsMaxDisjointIn, nullSchema: individuation perspectives.

Main results

• qua_cum_incompatible: a quantized predicate with two members is not cumulative.
• IsClassicalMereology.existsUnique_remainder: in a classical mereology a proper part has a unique remainder, so classical mereologies, like Boolean algebras, have remainders.
• IsExtensiveMeasure.strictMono: over a carrier with remainders an extensive measure is strictly monotone, so the measure phrases it builds are quantized (qmod_qua); the atom count is likewise extensive on sums of atoms (qua_algClosure_atomCount).
• nullSchema_eq: every member of a predicate lies in some individuation perspective.

Implementation notes

AlgClosure closes under binary sums, which agrees with closure under sums of arbitrary nonempty subsets only for finite sums. Classical mereology is defined, as in [Cha17], by unique sums in Tarski's sense; [Hov09] compares the alternative axiomatizations. Since Overlap excludes null parts, the element of a one-point carrier is null, so the trivial model is not a classical mereology.

References

• [BN18], [CK16], [Cha17], [Hov09], [Kri89], [Kri98], [Lan11], [Lan20], [Lin83], [SF21]

Reference properties

Cumulative, divisive and quantized reference are the mathlib set predicates SupClosed, IsLowerSet and IsAntichain (· ≤ ·) on the extension of a predicate, so hypotheses of these forms are applied directly: hC hx hy : P (x ⊔ y), hD hle hx : P y, hQ hx hy hne : ¬ x ≤ y.

@[reducible, inline]

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

A predicate has divisive reference if every part of a P-element is P.

Equations

• Mereology.DIV P = IsLowerSet {x : α | P x}

@[reducible, inline]

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

A predicate has quantized reference ([Kri89]) if no proper part of a P-element is P.

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

Quantization in the paper's form holds if no P-element lies strictly below another.

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

A singleton predicate is quantized ([Kri89] (T 1)).

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

Quantization pulls back along strictly monotone maps.

@[reducible, inline]

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

The P-atoms ([Kri89]) are the minimal P-elements.

Equations

• Mereology.atomize P = Minimal P

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

The P-atoms are quantized.

@[reducible, inline]

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

A predicate has cumulative reference ([Lin83], [Kri89]) if it is closed under sum. [Kri98] also requires two distinct members, and [CK16] give a form closed under sums of arbitrary nonempty subsets.

Equations

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

@[instance_reducible]

instance Mereology.instDecidableCUMOfFintypeOfDecidablePred {α : Type u_1} [SemilatticeSup α] {P : α → Prop} [Fintype α] [DecidablePred P] : Decidable (CUM P)

Equations

• Mereology.instDecidableCUMOfFintypeOfDecidablePred = decidable_of_iff (∀ (x : α), P x → ∀ (y : α), P y → P (x ⊔ y)) ⋯

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

A quantized predicate with two members is not cumulative ([Kri89] (T 3)).

theorem Mereology.cum_maximal_iff_isGreatest {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hCum : CUM P) {x : α} : Maximal P x ↔ IsGreatest {y : α | P y} x

A maximal element of a cumulative predicate is its greatest element, the supremum of [CK16].

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

A cumulative predicate has at most one maximal element.

Algebraic closure

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

The algebraic closure *P of P ([Lin83]) is the least predicate containing P and closed under binary sum. The inductive presentation supports induction on sums; setOf_algClosure identifies it with mathlib's supClosure.

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

  Every P-element is in *P.

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

  *P is closed under sum.

theorem Mereology.algClosure_cum {α : Type u_1} [SemilatticeSup α] {P : α → Prop} : CUM (AlgClosure 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_finsetSup' {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {ι : Type u_3} {s : Finset ι} (hs : s.Nonempty) {f : ι → α} (hf : ∀ i ∈ s, AlgClosure P (f i)) : AlgClosure P (s.sup' hs f)

*P contains the sum of every nonempty finite family from *P.

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 P-element below it.

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

A cumulative predicate is its own closure ([CK16]).

theorem Mereology.setOf_algClosure {α : Type u_1} [SemilatticeSup α] (P : α → Prop) : {x : α | AlgClosure P x} = supClosure {x : α | P x}

*P is mathlib's supClosure of the extension of P.

theorem Mereology.algClosure_iff_exists_sup' {α : Type u_1} [SemilatticeSup α] (P : α → Prop) (x : α) : AlgClosure P x ↔ ∃ (t : Finset α) (ht : t.Nonempty), (∀ y ∈ t, P y) ∧ t.sup' ht id = x

*P holds of exactly the sums of nonempty finite families of P-elements, the finite case of the closure of [CK16] and [Cha17] under sums of nonempty subsets.

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

The full algebraic closure ×P adds the empty sum ⊥ to *P, closing P under the sums of all finite families, the empty one included ([BN18]'s (30)).

Equations

• Mereology.FullAlgClosure P x = (Mereology.AlgClosure P x ∨ x = ⊥)

theorem Mereology.fullAlgClosure_bot {α : Type u_1} [SemilatticeSup α] [OrderBot α] (P : α → Prop) : FullAlgClosure P ⊥

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

theorem Mereology.fullAlgClosure_iff_exists_sup {α : Type u_1} [SemilatticeSup α] [OrderBot α] (P : α → Prop) (x : α) : FullAlgClosure P x ↔ ∃ (t : Finset α), (∀ y ∈ t, P y) ∧ t.sup id = x

×P holds of exactly the sums of finite families of P-elements.

Atoms and overlap

The null individual of a carrier, if it has one, is its IsBot element: ⊥ on an OrderBot carrier, and nothing on a NoBotOrder carrier or a classical mereology.

@[instance_reducible]

instance Mereology.instDecidableIsBotOfOrderBotOfDecidableEq_linglib {α : Type u_1} [PartialOrder α] [OrderBot α] [DecidableEq α] (x : α) : Decidable (IsBot x)

Equations

• Mereology.instDecidableIsBotOfOrderBotOfDecidableEq_linglib x = decidable_of_iff (x = ⊥) ⋯

@[instance_reducible]

instance Mereology.instDecidableIsBotOfFintypeOfDecidableLE_linglib {α : Type u_1} [PartialOrder α] [Fintype α] [DecidableLE α] (x : α) : Decidable (IsBot x)

Equations

• Mereology.instDecidableIsBotOfFintypeOfDecidableLE_linglib x = { decide := decide (∀ a ∈ Finset.univ, x ≤ a), reflects_decide := ⋯ }

@[reducible, inline]

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

An atom ([Lin83]) is a non-null element with no non-null proper part, that is, a minimal non-null element. The P-relative notion is atomize.

Equations

• Mereology.Atom x = Minimal (fun (x : α) => ¬IsBot x) x

theorem Mereology.Atom.not_isBot {α : Type u_1} [PartialOrder α] {x : α} (h : Atom x) : ¬IsBot x

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

An atom's only non-null part is itself.

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

A predicate holding only of atoms is quantized.

theorem Mereology.exists_atom_le {α : Type u_1} [PartialOrder α] {y : α} [WellFoundedLT α] (hy : ¬IsBot y) : ∃ (a : α), Atom a ∧ a ≤ y

In a well-founded part order every non-null element has an atom below it, so finite carriers are atomic ([CK16]).

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

atomCount α x is the number of atoms below x ([CK16]).

Equations

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

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

Two elements overlap ([Kri98]) if they share a non-null part.

Equations

• Mereology.Overlap x y = ∃ (z : α), ¬IsBot z ∧ z ≤ x ∧ z ≤ y

theorem Mereology.Overlap.refl {α : Type u_1} [PartialOrder α] {x : α} (h : ¬IsBot x) : Overlap x x

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

theorem Mereology.Overlap.not_isBot_left {α : Type u_1} [PartialOrder α] {x y : α} (h : Overlap x y) : ¬IsBot x

theorem Mereology.Overlap.not_isBot_right {α : Type u_1} [PartialOrder α] {x y : α} (h : Overlap x y) : ¬IsBot y

theorem Mereology.Overlap.of_le {α : Type u_1} [PartialOrder α] {x y : α} (hx : ¬IsBot x) (h : x ≤ y) : Overlap x y

A non-null part of y overlaps y.

theorem Mereology.Overlap.mono {α : Type u_1} [PartialOrder α] {x y x' y' : α} (hx : x ≤ x') (hy : y ≤ y') (h : Overlap x y) : Overlap x' y'

theorem Mereology.not_atom_sup_of_ne {α : Type u_1} [SemilatticeSup α] {x y : α} (hx : Atom x) (hy : Atom y) (hne : x ≠ y) : ¬Atom (x ⊔ y)

The sum of two distinct atoms is not an atom.

Pluralities

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

A proper plurality of Ps ([Lin83]) is a sum of P-elements with two distinct proper P-parts.

Equations

• Mereology.IsPlural P x = (Mereology.AlgClosure P x ∧ ∃ a < x, ∃ b < x, P a ∧ P b ∧ a ≠ b)

theorem Mereology.not_isPlural_of_subsingleton {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (h : ∀ (a b : α), P a → P b → a = b) (x : α) : ¬IsPlural P x

A predicate with at most one member has no plurality.

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

An atom in the closure of a predicate is one of its members, since an atom is not a proper sum.

theorem Mereology.isPlural_iff_of_atom {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {x : α} (hP : ∀ ⦃a : α⦄, P a → Atom a) : IsPlural P x ↔ AlgClosure P x ∧ ¬Atom x

For a predicate holding only of atoms, a plurality is a non-atomic element of the closure.

Bounded and bottomless carriers

theorem Mereology.atom_iff_isAtom {α : Type u_1} [PartialOrder α] [OrderBot α] {x : α} : Atom x ↔ IsAtom x

theorem Mereology.overlap_iff_not_disjoint {α : Type u_1} [PartialOrder α] [OrderBot α] {x y : α} : Overlap x y ↔ ¬Disjoint x y

theorem Mereology.atomize_ne_bot {α : Type u_1} [PartialOrder α] [OrderBot α] : (atomize fun (x : α) => x ≠ ⊥) = IsAtom

The atoms of the non-null predicate on a bounded carrier are its IsAtoms.

theorem Mereology.atom_iff_isMin {α : Type u_1} [PartialOrder α] [NoBotOrder α] {x : α} : Atom x ↔ IsMin x

Without a null individual, the atoms are the minimal elements.

The remainder principle

A proper part of a whole is completed to the whole by a remainder that does not overlap it. This is the remainder principle of [Kri98], the relative complementarity of [Kri89], and the unique separation of [Cha17]. Boolean algebras satisfy it with the difference y \ x, and so do classical mereologies (IsClassicalMereology.exists_remainder). The sources also require the remainder to be unique; the results below need only existence.

class Mereology.HasRemainders (α : Type u_3) [SemilatticeSup α] : Prop

A part structure has remainders if every proper part x of y is completed to y by a part that does not overlap x.

• exists_remainder ⦃x y : α⦄ : x < y → ∃ (z : α), ¬Overlap z x ∧ x ⊔ z = y

instance Mereology.instHasRemainders {α : Type u_1} [GeneralizedBooleanAlgebra α] : HasRemainders α

Classical mereology

Classical extensional mereology is the system of [CK16] and [Cha17]: a partial order in which every inhabited predicate has a unique sum in Tarski's sense. Weak and strong supplementation, the remainder principle and the absence of a null individual are theorems; [Hov09] compares this axiomatization with others. Binary sums are fusions of pairs (IsClassicalMereology.toSemilatticeSup), and the nonempty subsets of a set with two elements or more form a classical mereology.

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

t is a sum of the P-elements in Tarski's sense if it lies above each of them and each of its parts overlaps one of them.

Equations

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

class Mereology.IsClassicalMereology (α : Type u_3) [PartialOrder α] : Prop

A partial order is a classical extensional mereology if every inhabited predicate has a unique sum.

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

theorem Mereology.IsClassicalMereology.exists_isFusion {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] (P : α → Prop) (h : ∃ (x : α), P x) : ∃ (t : α), IsFusion P t

theorem Mereology.IsClassicalMereology.not_isBot {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] (x : α) : ¬IsBot x

A classical mereology has no null individual, since the predicate true of it alone would have no sum.

theorem Mereology.IsClassicalMereology.overlap_iff {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] {x y : α} : Overlap x y ↔ ∃ z ≤ x, z ≤ y

In a classical mereology, overlap is sharing a part.

theorem Mereology.IsClassicalMereology.isFusion_eq {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] (x : α) : IsFusion (fun (x_1 : α) => x_1 = x) x

Each element is the sum of itself.

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

Sums are unique.

theorem Mereology.IsClassicalMereology.weak_supplementation {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] {x y : α} (h : x < y) : ∃ z ≤ y, ¬Overlap z x

A proper part of y leaves a part of y that does not overlap it (weak supplementation), since otherwise y would be a second sum of the part alone.

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

A sum is a least upper bound, since weak supplementation forces the sum, an upper bound by definition, to be the least one.

theorem Mereology.IsClassicalMereology.strong_supplementation {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] {y u : α} (h : ¬y ≤ u) : ∃ v ≤ y, ¬Overlap v u

If y is not part of u, some part of y does not overlap u (strong supplementation).

theorem Mereology.IsClassicalMereology.exists_remainder {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] {x y : α} (h : x < y) : ∃ (z : α), ¬Overlap z x ∧ IsLUB {x, z} y

A classical mereology satisfies the remainder principle, since the sum of the parts of y that do not overlap x completes x to y.

instance Mereology.IsClassicalMereology.instNoBotOrder {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] : NoBotOrder α

A classical mereology has no bottom element.

theorem Mereology.IsClassicalMereology.le_of_forall_overlap {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] {y u : α} (h : ∀ v ≤ y, Overlap v u) : y ≤ u

An element all of whose parts overlap u is part of u (extensionality).

theorem Mereology.IsClassicalMereology.remainder_unique {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] {x y z z' : α} (hz : ¬Overlap z x) (hlub : IsLUB {x, z} y) (hz' : ¬Overlap z' x) (hlub' : IsLUB {x, z'} y) : z = z'

The remainder of a proper part is unique, since each of two remainders lies in y and so has every part overlapping x or the other remainder.

theorem Mereology.IsClassicalMereology.existsUnique_remainder {α : Type u_1} [PartialOrder α] [IsClassicalMereology α] {x y : α} (h : x < y) : ∃! z : α, ¬Overlap z x ∧ IsLUB {x, z} y

A proper part of y has exactly one remainder in y, the unique separation of [Kri98] and [Cha17].

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

Every pair has a least upper bound, the sum of the pair.

@[reducible]

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

The binary sum a ⊔ b of a classical mereology is the sum of the pair {a, b}.

Equations

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

instance Mereology.instHasRemaindersOfIsClassicalMereology {α : Type u_1} [SemilatticeSup α] [IsClassicalMereology α] : HasRemainders α

instance Mereology.instIsClassicalMereologySubtypeSetNonempty {ι : Type u_3} [Nontrivial ι] : IsClassicalMereology { s : Set ι // s.Nonempty }

The nonempty subsets of a set with two elements or more form a classical mereology whose sums are unions ([Cha17]).

Extensive measures

[Kri89] and [Kri98] define an extensive measure by additivity over non-overlapping elements and positivity, and derive from the remainder principle that a proper part measures less than the whole. [CK16] call a measure extensive on a set when it has that property there. Either way, the measure phrases such a measure builds are quantized.

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

The measure phrase "n units of R" denotes the R-elements of measure n, as [Kri89] analyses five ounces of gold.

Equations

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

theorem Mereology.qmod_qua {α : Type u_1} {M : Type u_3} [PartialOrder α] [Preorder M] {R : α → Prop} {μ : α → M} (hμ : StrictMonoOn μ {x : α | R x}) (n : M) : QUA (QMOD R μ n)

A measure phrase is quantized if its measure is strictly monotone on the predicate it restricts.

theorem Mereology.atomCount_strictMonoOn {α : Type u_1} [SemilatticeSup α] [Fintype α] {P : α → Prop} (hP : ∀ ⦃a : α⦄, P a → Atom a) : StrictMonoOn (atomCount α) {x : α | AlgClosure P x}

On a finite carrier the atom count is strictly monotone on the closure of a predicate that holds only of atoms.

theorem Mereology.qua_algClosure_atomCount {α : Type u_1} [SemilatticeSup α] [Fintype α] {P : α → Prop} (hP : ∀ ⦃a : α⦄, P a → Atom a) (n : ℕ) : QUA (QMOD (AlgClosure P) (atomCount α) n)

The sums of P-atoms with n atoms form an antichain, so two cats is quantized ([CK16]).

class Mereology.IsExtensiveMeasure {α : Type u_1} {M : Type u_3} [SemilatticeSup α] [AddCommMonoid M] [PartialOrder M] (μ : α → M) : Prop

An extensive measure function ([Kri89], [Kri98]) is additive over non-overlapping elements and positive on non-null ones.

• additive (x y : α) : ¬Overlap x y → μ (x ⊔ y) = μ x + μ y
• positive (x : α) : ¬IsBot x → 0 < μ x

theorem Mereology.IsExtensiveMeasure.strictMono {α : Type u_1} {M : Type u_3} [SemilatticeSup α] [AddCommMonoid M] [PartialOrder M] [HasRemainders α] [AddLeftStrictMono M] (μ : α → M) [h : IsExtensiveMeasure μ] : StrictMono μ

Over a carrier with remainders, an extensive measure gives a proper part a smaller measure than the whole, which adds a non-null remainder to it.

instance Mereology.instIsExtensiveMeasureFinsetNatCard {β : Type u_2} [DecidableEq β] : IsExtensiveMeasure Finset.card

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], [Lan20]), and the null schema of [SF21] unions all perspectives. The overlap relation ov is a parameter (mereologically, Overlap).

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

A predicate overlaps if two distinct members 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

A predicate is disjoint if no two distinct members share a part.

Equations

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

theorem Mereology.disjointPred_iff_pairwise {α : Type u_1} (ov : α → α → Prop) {P : Set α} : DisjointPred ov P ↔ P.Pairwise fun (x1 x2 : α) => ¬ov x1 x2

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

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

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

D is a maximally disjoint subset of P if it is disjoint and cannot be extended within P without overlap.

Equations

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

theorem Mereology.isMaxDisjointIn_iff_maximal {α : Type u_1} (ov : α → α → Prop) (D P : Set α) : IsMaxDisjointIn ov D P ↔ Maximal (fun (D : Set α) => D ⊆ P ∧ DisjointPred ov D) D

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

The null individuation schema of P is the union of its maximally disjoint subsets.

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 maximally disjoint subsets overlaps.

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)

The null schema of a predicate with two distinct perspectives overlaps.

theorem Mereology.isMaxDisjointIn_self {α : Type u_1} (ov : α → α → Prop) {P : Set α} (h : DisjointPred ov P) : IsMaxDisjointIn ov P P

A disjoint predicate is its own unique perspective.

theorem Mereology.exists_isMaxDisjointIn_mem {α : Type u_1} (ov : α → α → Prop) {P : Set α} {x : α} (hx : x ∈ P) : ∃ (D : Set α), IsMaxDisjointIn ov D P ∧ x ∈ D

Every member of a predicate lies in some perspective on it, since a disjoint subset containing it extends to a maximal one.

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

The null schema is the identity, since every member of a predicate is in some perspective.

theorem Mereology.disjointPred_overlap_iff {α : Type u_1} [PartialOrder α] [OrderBot α] {P : Set α} : DisjointPred Overlap P ↔ P.PairwiseDisjoint id

On a carrier with a null individual, a predicate is disjoint iff its members are pairwise disjoint in the lattice sense.