Mereotopology

Mereotopology adds to parthood a relation of connection, which is reflexive, symmetric, and monotone along parthood, so that parthood and overlap entail it. Casati and Varzi's ground mereotopology, in the form Grimm gives it, uses connection to single out the self-connected individuals, which come in one piece, and the clusters, sums of entities transitively connected through others of their kind, such as a pile of sand or a swarm of locusts. Grimm lets aggregate nouns denote clusters, under external connection for sand and proximate connection for ants. Transitive connection is reachability in the graph of connection between the entities of a predicate, so a cluster is the sum of finitely many of them inside one connected component, and the clusters of a component are cumulative.

Main definitions

• IsConnection C: the axioms of a connection relation.
• SelfConnected C x: self-connection.
• connectionGraph C P: connection between P-entities as a graph, whose reachability is transitive connection.
• IsClusterIn C P c, IsCluster C P, IsMaxCluster C P: clusters inside a connected component, clusters, and maximal clusters.

Main results

• IsConnection.of_le, IsConnection.of_overlap: parthood and overlap entail connection.
• isCluster_iff: a cluster is the sum of a nonempty finite set of P-entities any two of which are transitively connected, Grimm's definition.
• cum_isClusterIn: the clusters of a connected component are cumulative.
• disjointPred_isMaxCluster: maximal clusters do not overlap.

Implementation notes

Connection is reflexive on non-null individuals only, as Overlap relates non-null parts: were a null individual connected to itself, monotonicity would connect everything. On a carrier without a null individual, such as a classical mereology, the axioms are Casati and Varzi's. Monotonicity is stated in the second argument, which by symmetry is the axiom that whatever is connected to a part is connected to the whole. Self-connection keeps Grimm's overlap formulation. Strong self-connection, its maximal form, and the strong and external connection relations defined from it need an interior operator and are not formalized. The chain that connects two members of a cluster may run through P-entities outside the cluster, since Grimm's definition quantifies over the set the chain runs through.

References

• [CV99], [Gri12]

Connection and self-connection

structure Mereology.IsConnection {α : Type u_1} [PartialOrder α] (C : α → α → Prop) : Prop

A connection relation ([Gri12] T1–T3) is reflexive on non-null individuals, symmetric, and monotone along parthood.

• refl ⦃x : α⦄ : ¬IsBot x → C x x
• symm ⦃x y : α⦄ : C x y → C y x
• mono (z : α) : Monotone (C z)

theorem Mereology.IsConnection.of_le {α : Type u_1} [PartialOrder α] {C : α → α → Prop} {x y : α} (hC : IsConnection C) (hx : ¬IsBot x) (h : x ≤ y) : C x y

Parthood entails connection.

theorem Mereology.IsConnection.of_overlap {α : Type u_1} [PartialOrder α] {C : α → α → Prop} {x y : α} (hC : IsConnection C) (h : Overlap x y) : C x y

Overlap entails connection ([Gri12] (8)).

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

An individual is self-connected ([Gri12] D24) if any two individuals that between them overlap exactly what it overlaps are connected.

Equations

• Mereology.SelfConnected C x = ∀ (y z : α), (∀ (w : α), Mereology.Overlap w x ↔ Mereology.Overlap w y ∨ Mereology.Overlap w z) → C y z

Clusters

def Mereology.connectionGraph {α : Type u_1} (C : α → α → Prop) (P : α → Prop) : SimpleGraph α

In the connection graph of P, two distinct P-entities are adjacent when they are connected. Its reachability is transitive connection ([Gri12] D32), a chain of P-entities each connected to the next.

Equations

• Mereology.connectionGraph C P = SimpleGraph.fromRel fun (a b : α) => P a ∧ P b ∧ C a b

theorem Mereology.connectionGraph_reachable {α : Type u_1} {C : α → α → Prop} {P : α → Prop} {a b : α} (ha : P a) (hb : P b) (h : C a b) : (connectionGraph C P).Reachable a b

Two connected P-entities are transitively connected.

def Mereology.IsClusterIn {α : Type u_1} [PartialOrder α] (C : α → α → Prop) (P : α → Prop) (c : (connectionGraph C P).ConnectedComponent) (x : α) : Prop

A cluster of P-entities inside the connected component c is the sum of a nonempty finite set of P-entities of c.

Equations

• Mereology.IsClusterIn C P c x = ∃ (Z : Finset α), Z.Nonempty ∧ (∀ z ∈ Z, P z ∧ (Mereology.connectionGraph C P).connectedComponentMk z = c) ∧ IsLUB (↑Z) x

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

A cluster of P-entities ([Gri12] D33) is a cluster inside some connected component.

Equations

• Mereology.IsCluster C P x = ∃ (c : (Mereology.connectionGraph C P).ConnectedComponent), Mereology.IsClusterIn C P c x

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

A maximal cluster contains every cluster that overlaps it.

Equations

• Mereology.IsMaxCluster C P x = (Mereology.IsCluster C P x ∧ ∀ (y : α), Mereology.IsCluster C P y → Mereology.Overlap y x → y ≤ x)

theorem Mereology.isCluster_iff {α : Type u_1} [PartialOrder α] {C : α → α → Prop} {P : α → Prop} {x : α} : IsCluster C P x ↔ ∃ (Z : Finset α), Z.Nonempty ∧ (∀ z ∈ Z, P z) ∧ (∀ z ∈ Z, ∀ z' ∈ Z, (connectionGraph C P).Reachable z z') ∧ IsLUB (↑Z) x

A cluster is the sum of a nonempty finite set of P-entities any two of which are transitively connected.

theorem Mereology.disjointPred_isMaxCluster {α : Type u_1} [PartialOrder α] {C : α → α → Prop} {P : α → Prop} : DisjointPred Overlap {x : α | IsMaxCluster C P x}

Maximal clusters do not overlap, since each would contain the other.

theorem Mereology.cum_isClusterIn {α : Type u_1} [SemilatticeSup α] (C : α → α → Prop) (P : α → Prop) (c : (connectionGraph C P).ConnectedComponent) : CUM (IsClusterIn C P c)

The clusters of a connected component are cumulative.