CODI: A multidimensional theory of mereotopology with closure operations

1. Introduction

Geometric data models power most of the spatial information systems used for navigation, mapping (e.g., geographic information systems (GIS)), and design (e.g., computer-aided design or manufacturing systems (CAD/CAM)) and form the foundation for the spatial information that is essential to transportation and logistics, property records, land use and urban planning, architectural, mechanical and product design, and emergency response planning and disaster relief. Geometric data models represent objects’ spatial location and extent using geometric conceptualizations of space – typically Euclidean or spherical geometry – either directly or as base entities in algebraic topological structures (see, e.g., work by Blumenthal and Menger (1970) and by Egenhofer et al. (1989)) such as simplicial or other cell complexes, or tessellations such as triangulated irregular networks (TIN). Each object is represented by a point location, a collection of points, or by more complex geometric features, such as polylines, polygons, or polyhedra, all of which are based on points (e.g., the points that define the individual segments of a polyline, which in turn define polygons). All points must have precise coordinates in the underlying reference system. Yet a lot of other, especially textual, information such as from historical records or from social media is of primarily qualitative rather than geometric-quantitative nature and lacks geometric precision. Such qualitative spatial information cannot easily be stored using geometric data models without often arbitrary and unwarranted geometric approximations of the described objects and places. Such geometric approximations also lead to artifacts such as accidental overlap, for example, two lakes may overlap or a road along a lake’s share overlapping the lake because of their representations as polygons and polylines and a purely geometric definition of overlaps. Moreover, the precision that comes with geometric representations, for example the ability to measure the length or size of an intersection, is misguiding for geometrically approximated or vague entities. More important is often the nature of the spatial relationship between the entities (e.g., does the road border the town or does it go into it?, is it entirely within the town or are parts outside?) that qualitative relations can capture without the detour via geometric approximation of the entities.

Mereotopological models of space can fill this gap, but are often incompatible with the existing geometric data models, thus motivating the presented work. While mereotopology has been extensively studied throughout Philosophical Logic, Computer Science, Cognitive Science, and Geographic Information Science (see, for example, the excellent overview by Casati and Varzi (1999) or the review by Hahmann and Grüninger (2012)), most existing mereotopological theories are unidimensional in the sense that they only permit entities of a single dimension in any particular model and thus cannot accommodate zero-dimensional (e.g., points), one-dimensional (e.g., lines or curves), two-dimensional (e.g., polygons and surfaces), and three-dimensional spatial entities (e.g., solids) in a single a model. Multidimensional mereotopologies overcome this restriction by explicitly permitting entities of different dimensions to co-exist in a model (Galton, 2004).

This paper provides a comprehensive and streamlined overview of the multidimensional mereotopology CODI whose development has been inspired by Galton’s and Gotts’ earlier work (Galton, 1996; Gotts, 1996). CODI formalizes the primitive notions of spatial containment and relative spatial dimension (the ontology’s name stands for COntainment and DImension) in first-order logic and defines a set of six intuitive mereotopological relations: containment and its refinement parthood together with contact and its refinements partial overlap, incidence, and superficial contact, which apply to entities of all dimensions but which operate largely independently of the precise dimensions of the involved spatial entities (Hahmann and Grüninger, 2011b). This paper extends CODI by introducing and axiomatizing mereological closure operations of product/intersection, difference (i.e., relative complementation), and sums that apply to any pair of spatial entities regardless of their dimension. The earlier theories (Galton, 1996; Gotts, 1996) limited these operations to entities of equal dimension. As a result, some meaningful intersection and differences, for example between a linear feature (e.g., a road or river) and a 2D region, as shown in Fig. 1(c), are not captured, thereby limiting the use of the operations more than necessary. However, if we insist that these operations are defined for all pairs of spatial regions, one can easily end up with mixed-dimensional entities, such as an entity consisting of a line segment and an isolated point (e.g., the intersection in Fig. 1(a)) or of a 2D region with a line segment removed (e.g., the difference x − y in Fig. 1(c)). To better understand to what extent CODI aligns with unidimensional mereotopologies and geometric conceptualizations of space, this paper analyzes CODI ’s extended axiomatization with a focus on the following questions:

OPEN IN VIEWER

Fig. 1.

Models of CODI that illustrate intersections and differences involving regions of varying dimensions. Other mereotopologies only entail the existence of an entity for the intersection and difference in (b). In (a), r and s share two regions: the linear feature l and the point p. But both together cannot be the intersection, because such an entity would not be a dimensionally uniform region. Instead, r · s = l . Then the intersection · is not associative because r · ( s · p ) = r · p = p ≠ ∅ = l · p = ( r · s ) · p . In (b) intersection and the differences x − y and y − x are defined as expected between two regions of the same dimension. In (c) the intersection x · y is a proper part of y but not a proper part of x, though a lower-dimensional region contained in x. Hence, only the difference y − x results in a new region, while x − y loses the lower-dimensional artifact and results in x. In (d) x − y = x and y − x = y since the intersection x · y is of a lower dimension than both x and y.

It is shown that the proposed mereological operations are well-defined in the resulting theory CODI ↕ , with the double arrow denoting upward (i.e. under sums) and downward (i.e. under intersections and differences) closure. It is shown that this theory exhibits the expected behavior between entities of the same dimension and satisfies the most important mereological principles from unidimensional mereotopology. The operations further adhere to most of the desired mathematical properties, though some require weakening (e.g., left- and right-alternative laws instead of associativity of the intersection operation), while only few must be forfeited. It is further proved that atomic models of CODI ↓ – the theory closed only under intersections and differences – can always be decomposed (i.e., partitioned) into a set of minimal (i.e., indivisible) parts, which simplifies the implementation of the theory on top of geometric data models wherein entities are represented as collections of minimal entities (e.g., line segments or atomic cells). This decomposition extends to CODI ↕ because it is a logical extension of CODI ↓ . As a final result, the models of CODI ↕ are characterized as sets of Boolean algebras, wherein the set of all entities of identical dimension together form a Boolean algebra.

Mereological relations relate parts to wholes (e.g., subregions to a larger region), while topological relations describe whether and how things are connected to one another. Mereotopological relations (Varzi, 1996) arise from the combination of both kinds of relations, enabling the definition of relations such as overlap (i.e., connected via a shared part) and external connection (i.e., touching in only a boundary).1

Mereotopology originally emerged from interest in region-based theories (Clarke, 1981; Biacino and Gerla, 1991; Whitehead, 1929) – so-called pointless topologies – as more perceptually accurate alternative to point set topology and geometry, wherein points are first-class entities. In that philosophical tradition, mereotopologies have been married to strict region-based conceptualizations of space wherein extended spatial entities – typically called regions – are the only first-class entities of the domain and points and other lower-dimensional entities are not entities in the domain. We refer to these mereotopologies as unidimensional mereotopologies (Hahmann and Grüninger, 2012). Examples of first-order logic axiomatizations of unidimensional mereotopology include the Region Connection Calculus (RCC; Cohn et al., 1997; Randell et al., 1992) and the mereotopology RT (Asher and Vieu, 1995; Hahmann et al., 2009). Unidimensional mereotopologies can be constructed using either a single topological primitive of contact, a single mereological primitive of parthood, or a combination of a topological and a mereological primitive relation (Cohn and Varzi, 2003). These unidimensional mereotopologies must resort to higher-order constructs, i.e., constructs such as ideals or filters that are not expressible in first-order logic, as only ways to define lower-dimensional entities. But as clearly demonstrated by work originating from the spatial database and geographic information science communities (Clementini and Di Felice, 1995; Clementini et al., 1993; Egenhofer, 1991; Egenhofer and Herring, 1991; McKenney et al., 2005), mereotopological relations also apply to entities of different dimensions. Thus, it is possible to decouple mereotopological relations from a strictly region-based, unidimensional conceptualization of space.

A few first-order logical axiomatizations of mereotopology, (e.g., Baumann et al., 2016; Galton, 1996; Gotts, 1996; Smith, 1996; Smith and Varzi, 1997) have gone this route by allowing entities of different spatial dimensions to co-exist. We refer to those theories as multdimensional mereotopologies. Many of them, however, limit the kind of permissible lower-dimensional entities. For example, Smith (1996) and Smith and Varzi (1997) follow Brentano’s ideas of space (Brentano, 1988) wherein boundaries (and parts thereof) are the only kind of permissible lower-dimensional objects. Smith and Varzi (1997) achieve this, for example, by including a primitive predicate B ( x , y ) denoting ‘x is the boundary of y’ in their axiomatization.

To our knowledge, Galton (1996) was the first to acknowledge the need for an explicit concept of “dimensionality” in a multidimensional mereotopology, an approach the development of the CODI family of theories also follows. While Galton used a boundary predicate B ( x , y ) similar to Smith and Varzi (1997), he then defined lower-dimensional entities more generally as the entities that are of the same dimension as the boundary of higher-dimensional entities rather than only the boundaries themselves. Thus, lower-dimensional entities do not have to be boundaries of higher-dimensional entities. Since then, at least three first-order axiomatizations of multidimensional mereotopologies have been developed: Gotts’ INCH Calculus (Gotts, 1996), GFO’s ontology for space (Baumann et al., 2016), and CODI (Hahmann and Grüninger, 2011b). The INCH calculus is based on the single primitive relation INCH ( x , y ) denoting that x includes (i.e., spatially contains) an equi-dimensional chunk of y; this relation then allows defining notions of equidimensionality and lower-dimensionality. Unlike the INCH calculus, CODI introduces a primitive relation ⩽ dim as an explicit relation for comparing the dimensions of two entities. But CODI and the INCH calculus are similar in that they define their mereotopological relations without explicitly distinguishing the dimensions of the involved entities. For example, CODI ’s containment relation applies regardless of the specific dimension of the contained entity. GFO Space takes a different approach by defining four sorts of spatial entities, namely zero-dimensional, one-dimensional, two-dimensional, and three-dimensional entities using a primitive relation of spatial boundary sb ( x , y ) and then defining separate mereotopological relations based on the dimension of the involved entity. For example, GFO Space dimensionally distinguishes four containment relations: spatial part, 2-dimensional hyper part, 1-dimensional hyper part, and 0-dimensional hyper part.

This work on extending CODI with closure operations is largely motivated by the observation that Galton’s work, Gotts’ INCH calculus, and GFO Space all unnecessarily restrict the mereological closure operations of intersection, difference, and sum to only pairs of entities with identical dimension. The restriction of the sum operation is justifiable to avoid entities of mixed dimensionality because the sum of two entities of different dimensions will always be of mixed dimension except for the special case where one entity is contained in the other. But the intersection or difference between two entities of different dimensions can be, and often is, of uniform dimension. For example, the intersection of the areal and linear features in Fig. 1(c) is itself a linear feature, but this intersection is permissible neither in the INCH calculus nor in Galton’s theory. This paper explores how to fill this gap by presenting and investigating an extension to CODI with axioms that define intersections, differences, and sums for all pairs of entities regardless of their relative dimension. We achieve totality by modifying the operations such that they drop all entities in the intersection (or difference or sum) that are not of the same dimension as the highest-dimensional entity in the intersection (or difference or sum). For example, a 2D region that intersects a linear feature in a line segment and a point would drop the point and just yield the intersecting line segment.

In addition to the discussed prior work on axiomatic formalizations of mereotopology, two other types of approaches for defining mereotopological relations between spatial entities have been studied in the literature: (1) qualitative calculi of lattices of relations and associated composition operations, such as the RCC-5 and RCC-8 (Cohn et al., 1997; Randell et al., 1992); and (2) matrices of the nine point-set intersections of the interior, boundary, and exterior of two entities (Egenhofer, 1991; Egenhofer and Herring, 1991).

Qualitative calculi of mereotopology, such as the RCC-5 or RCC-8, are a set of base relations equipped with a composition table that supports constraint-based reasoning over sets of relations between regions (Cohn and Renz, 2008). While the RCC relations are derived from an accompanying logical axiomatization, the axiomatization’s purpose is only to ensure that the base relations are jointly exhaustive and pairwise disjoint (JEPD). The axiomization – including the closure operations defined therein – is not used (and cannot be used) for constraint-based reasoning with the qualitative calculi. Whereas the original RCC is restricted to a set of regions of equal dimension (e.g., a set of 2D regions or a set of 3D regions), a more recent extension to multidimensional space has been proposed by Clementini and Cohn (2014), with corrections proposed by Izadi et al. (2019). However, this calculus – called RCC*-9 – does not include predicates that allow expressing of what dimension two related entities are: neither absolutely (using classes of regions) nor relatively by comparing the dimension of two regions. Even earlier, Kurata (2010) proposed the 9⁺-intersection calculus as a multidimensional calculus of mereotopological relations that dimensionally refines the 9-intersection approach, which is discussed in more detail shortly, to derive more fine-grained relations. However, no closure operations are included in this calculus either. The main reason is that the kind of constraint-based reasoning used with any qualitative calculi restricts the involved relations to binary ones. Thus, these qualitative calculi are unable to express or perform reasoning using closure operations such as sums, differences, or intersections to pairs of entities because these binary operations (which are, mathematically, functions) are, once translated to relations, ternary relations. Thus, closure operations do not fit into the kind of lattice of relations that is the basis of any qualitative calculus and are outside the scope of constraint-based reasoning.

In addition to this limitation of the signature of qualitative calculi, it is also not yet clear how useful composition-based reasoning can be for multidimensional mereotopological relations because in a higher-dimensional space many combinations of a relation between x and y and another relation between y and z seems to only minimally restrict what relation can hold between x and z – as supported by the sheer number of relations in dimensionally refined versions of the 9-intersection method discussed below. This requires further study of the composition tables for the multidimensional calculi, which have not yet been published for either the RCC*-9 or the 9⁺-intersection calculus. In ongoing work, we are also conducting a more thorough formal comparison and integration between the RCC*-9 and the theory presented in this paper.

Matrices of point-set intersections, such as used by the 9-intersection method (Egenhofer, 1991; Egenhofer and Herring, 1991; Kurata, 2008), define mereotopological relations based on combinations of the point set intersections of the interior, boundary, and exterior of two regions. Extensions that take the dimensions of the participating entities into account, lead to a combinatorial increase in the number of distinct mereotopological relations, for example the dimension-extended and calculus-based methods by Clementini and Di Felice (1995) result in 52 and 81 unique relations, respectively, and the approach by McKenney et al. (2005) creates around 300 relations – and these relations do not even consider any 3D entities. While the total number of relations is not easily gathered for the 9⁺-intersection calculus, it likely yields a similarly large number of relations. This is caused by introducing separate relations for each combination of the dimensions of the involved entities. For example, separate point-point, point-line, point-region, line-line, line-region, and region-region relations are defined.

But more importantly and in line with the original intent of the 9-intersection approach – which was to provide a more user-friendly, qualitative language to query geometric data sources – these approaches do not provide any axioms relating the relations, thus very much limiting the spatial reasoning that can be performed. Specifically, mereological closure operations are not within the scope of these approaches. Only the few approaches that additionally provide a qualitative calculi (e.g., Kurata, 2010) support reasoning but still not over expressions that involve any of the mereological closure operations. Such approaches, for example, cannot reason about how the difference − y between two regions is related to a third region given how the third region is related to x and y.

This section reviews the multidimensional mereotopology CODI , which was first proposed by Hahmann and Grüninger (2011b) and fully developed by Hahmann (2013), and proves additional theorems that help characterize the defined relations. These theorems will also simplify many of the proofs in the extension of CODI by closure operations presented in the subsequent section. Any model of CODI has a universe of discourse that consists of a finite or infinite set of spatial (and possibly spatio-temporal) regions of various dimensions. All these regions are embedded in a common n-dimensional space, typically in R n , and thus form an n-dimensional spatial scene. We will specifically study the finite models, that is, the scenes with only a finite number of interacting spatial regions (points, curves, areas or volumes).

In any model, every spatial region is simple or complex. Simple regions represent regular closed sets2

Examples of permissible regions are points and finite sets of points; 1D entities such as curve and line segments, infinite curves and lines, as well as complex linear features (e.g., finite sets of segments connected, if at all, only in their endpoints); 2D areal regions including polygons, cell complexes, and other bounded regions (e.g., a part of the surface of a sphere) as well as unbounded regions (e.g., planes, semi-planes, or the entire surface of a sphere); or 3D voluminal regions. Regions with lower-dimensional artefacts, for example, an areal region with a protruding or missing line segment or a missing boundary is not permitted as entity in the domain, but could be described as a “scene” (i.e., a model of CODI ) consisting of two or more entities that happen to intersect. The theory can be limited to a specific number of dimensions if so desired (Hahmann, 2013; Hahmann and Grüninger, 2011a).

Note that CODI is designed as a theory of abstract spatial entities, i.e., arbitrary space regions, rather than physical/material endurants. For abstract spatial entities, arbitrary intersections, complements, and sums are justifiable as they produce other abstract spatial entities. The same is not necessarily true for physical objects. Because of this scope, all entities in the domain of discourse are assumed to be space regions. However, a second variant of the theory that explicitly distinguishes space regions – denoted by S ( x ) – from other objects, in particular physical endurants, has been developed to allow the theory to be used in conjunction with DOLCE taxonomy of physical endurants. In that version,4

CODI ’s formalization is based on two primitive relations: (1) a mereological predicate of spatial containment, denoted as Cont ( x , y ) and interpreted point-set topologically as “x is a subset of y” (i.e., x is entirely contained within y), and (2) a predicate ⩽ dim  – typically written in infix notation as x ⩽ dim y  – that compares the dimension of two spatial regions and is interpreted as “if all of y’s components can be embedded (as regular closed sets) in spaces of dimension m, then all of x’s component can be embedded in spaces of dimension m or lower”.5

3.1. The theory of relative dimensionality

The predicate ⩽ dim is a reflexive, totally ordered, and transitive relation (D’-A1–3), with < dim , > dim , ⩾ dim , and = dim defined as expected (D’-D1–4). For mathematical simplicity, the theory introduces a zero (or null) region, indicated by the unary predicate ZEX . The zero region – if one exists at all6

⁶

CODI ↓ will entail that the zero region exists (Z-T1) to ensure totality of the difference operation.

– is unique (D’-A5) and is assigned a dimension lower than all other regions (D’-A5).7

⁷

The set of axioms used here are denoted by D’ to distinguish them from an earlier more generalized axiomatization (Hahmann and Grüninger, 2011b) that allowed for entities with incomparable dimensions.

(D’-A1)

x ⩽ dim x ( ⩽ dim reflexive)

(D’-A2)

x ⩽ dim y ∨ y ⩽ dim x ( ⩽ dim is a total/linear order)

(D’-A3)

x ⩽ dim y ∧ y ⩽ dim z → x ⩽ dim z ( ⩽ dim transitive)

(D’-A4)

ZEX ( x ) ∧ ZEX ( y ) → x = y (unique zero region)

(D’-A5)

ZEX ( x ) ∧ ¬ ZEX ( y ) → x ⩽ dim y ∧ y ≰ dim x (zero region has lowest dimension)

(D’-D1)

x < dim y ↔ x ⩽ dim y ∧ y ≰ dim x (lesser dimension)

(D’-D2)

x = dim y ↔ x ⩽ dim y ∧ y ⩽ dim x (equal dimension)

(D’-D3)

x > dim y ↔ y < dim x (greater dimension)

(D’-D4)

x ⩾ dim y ↔ y ⩽ dim x (greater or equal dimension)

Additional notions of maximal and minimal dimension (apart from the zero region) MaxDim and MinDim and of covering dimension (i.e, next greater dimension) ≺ dim (D-D5–7) are defined as follows.

(D-D5)

MaxDim ( x ) ↔ ∀ y [ y ⩽ dim x ] (maximal-dimensional entities)

(D-D6)

MinDim ( x ) ↔ ¬ ZEX ( x ) ∧ ∀ y [ ¬ ZEX ( y ) → y ⩾ dim x ] (minimal-dimensional non-zero entities)

(D-D7)

x ≺ dim y ↔ x < dim y ∧ ∀ z [ z ⩽ dim x ∨ y ⩽ dim z ] (next-lower dimension)

For most purposes, it is convenient and customary to assume that the set of dimensions form a bounded (i.e. with a lowest and a highest dimension, postulated by D’-A6 and D’-A7) and discrete set (i.e. the dimensions are not dense in the sense that there is a unique next-lower and next-higher dimension for each region; captured as D’-A8 and D’-A9).

(D’-A6)

∃ x [ MinDim ( x ) ] (a region of lowest dimension exists)

(D’-A7)

∃ x [ MaxDim ( x ) ] (a region of highest dimension exists)

(D’-A8)

¬ MaxDim ( x ) → ∃ y [ x ≺ dim y ] (discrete set of dimensions: for every region that is not of highest dimension a region of next-higher dimension exists)

(D’-A9)

¬ ZEX ( x ) ∧ ¬ MinDim ( x ) → ∃ y [ y ≺ dim x ] (discrete set of dimensions: for every non-zero region that is not of lowest dimension a region of next-lower dimension exists)

We define the ontology module8

⁸

All modules presented here are provided in Common Logic format in COLORE: http://colore.oor.net in the folders multidim_mereotopology_XXX. DI linear - bounded - discrete ′ , for example, is axiomatized in http://colore.oor.net/multidim_mereotopology_dim/dim_prime_linear_bounded_discrete.clif.

DI linear - bounded - discrete ′ = {D’-D1–D4, D-D5–D7, D’-A1–A9} The following theorems D-T1–D-T3 verify that the defined relation = dim is indeed an equivalence relation, i.e., that = dim is reflexive, symmetric, and transitive. D-T4, D-T5 verify that dimensional equivalence preserve transitivity of < dim , while D-T6 expresses in simpler form that any two regions are dimensionally comparable, i.e., they either have the same dimension or one of them has a lower dimension than the other.9

⁹

Proofs for all theorems – sentences with labels of the form XX-Tx – throughout Sections 3 to 5 and for the supplementation principles EP-E1, EP-E2, EP-E3, PO-E1 and PO-E2 in Section 4 are provided in the Appendix.

Together with the definitions, this ensures that the dimension relations form the relation lattice shown in Fig. 2.

OPEN IN VIEWER

Fig. 2.

Lattice of the dimensional relations in DI linear ′ - bounded - discrete and maintained in CODI .

(D-T1)

x = dim x ( = dim reflexive)

(D-T2)

x = dim y → y = dim x ( = dim symmetric)

(D-T3)

x = dim y ∧ y = dim z → x = dim z ( = dim transitive)

(D-T4)

x = dim y ∧ z < dim x → z < dim y ( = dim renders < dim transitive)

(D-T5)

x = dim y ∧ x < dim z → y < dim z ( = dim renders < dim transitive)

(D-T6)

x < dim y ∨ y < dim x ∨ x = dim y (of two entities, one is either of lesser, equal, or greater dimension than the other)

3.3. The combined theory CODI

A single axiom relates the primitive notions: if x is contained in y, then y must have at least the dimension of x (CD-A1).

(CD-A1)

Cont ( x , y ) → x ⩽ dim y (a contained entity is of the same or a lesser dimension)

Parthood and proper parthood are defined as unidimensional variants of containment (EP-D, EPP-D) with parthood being – just like containment – reflexive (EP-T1), antisymmetric (EP-T2), transitive (EP-T3), and extensional (EP-T9).

(EP-D)

P ( x , y ) ↔ Cont ( x , y ) ∧ x = dim y (equidimensional parthood)

(EP-T1)

¬ ZEX ( x ) → P ( x , x ) (P reflexive)

(EP-T2)

P ( x , y ) ∧ P ( y , x ) → x = y (P antisymmetric)

(EP-T3)

P ( x , y ) ∧ P ( y , z ) → P ( x , z ) (P transitive)

(EP-T9)

∀ z [ P ( z , x ) ↔ P ( z , y ) ] ↔ x = y (P extensional)

(EPP-D)

PP ( x , y ) ↔ P ( x , y ) ∧ x ≠ y (equidimensional proper parthood)

Min and Max denote minimal (i.e., indivisible, not containing any proper parts) and maximal (i.e., not a proper part of another region) entities within a dimension (ME-D1,D2). To prove decomposability later on, we need to restrict the theory to models that are atomic, wherein each region must contain some minimal part (ME-E1).

(ME-D1)

Max ( x ) ↔ ¬ ZEX ( x ) ∧ ∀ y [ ¬ PP ( x , y ) ] (maximal in a dimension)

(ME-D2)

Min ( x ) ↔ ¬ ZEX ( x ) ∧ ∀ y [ ¬ PP ( y , x ) ] (minimal in a dimension)

(ME-E1)

¬ ZEX ( x ) → ∃ y [ P ( y , x ) ∧ Min ( y ) ] (nonzero regions have a minimal part)

Three specialized symmetric contact relations become definable: partial overlap PO when two regions of equal dimension share a region of the same dimension (e.g., the 2D regions in Fig. 1(b) share a 2D part; PO-D);12

¹²

Our use of PO differs from the use in most unidimensional mereotopologies, e.g., by the RCC (Cohn et al., 1997) or others discussed by Casati and Varzi (1999), where PO disallows full containment, a notion expressible here as PO ( x , y ) ∧ ¬ Cont ( x , y ) ∧ ¬ Cont ( y , x ) . In that sense, our relation PO is closer to RCC’s O relation.

incidence SC when a region shares a part with a higher-dimensional region (e.g., in Fig. 1(c) the curve shares a segment with the 2D region, and in Fig. 1(a) the 1D region l is contained in the 2D region r; Inc-D); and superficial contact SC when two regions share a lower-dimensional region (e.g., the 2D regions r and s share 1D region l and point p in Fig. 1(a); SC-D). Together, the three relations are an exhaustive and mutually exclusive set of subrelations of contact (Hahmann and Grüninger, 2011b). Refer to Hahmann (2013, Ch. 6) for a detailed discussion of the contact relations.

(PO-D)

PO ( x , y ) ↔ ∃ z [ P ( z , x ) ∧ P ( z , y ) ] (partial overlap)

(Inc-D)

Inc ( x , y ) ↔ ∃ z [ ( Cont ( z , x ) ∧ P ( z , y ) ∧ z < dim x ) ∨ ( P ( z , x ) ∧ Cont ( z , y ) ∧ z < dim y ) ] (incidence)

(SC-D)

SC ( x , y ) ↔ ∃ z [ Cont ( z , x ) ∧ Cont ( z , y ) ] ∧ ∀ z [ Cont ( z , x ) ∧ Cont ( z , y ) → z < dim x ∧ z < dim y ] (superficial contact)

We define13

¹³

http://colore.oor.net/multidim_mereotopology_codi/codi.clif

CODI = DI linear - bounded - discrete ′ ∪ CO basic ∪ {CD-A1, EP-D, EPP-D, PO-D, Inc-D, SC-D, ME-D1,D2} and14

¹⁴

http://colore.oor.net/multidim_mereotopology_codi/codi_atomic.clif

CODI at = CODI ∪ {ME-E1} as its atomic version. (PO-T1)

¬ ZEX ( x ) → PO ( x , x ) ( PO reflexive)

(PO-T2)

PO ( x , y ) → PO ( y , x ) ( PO symmetric)

(PO-T3)

PO ( x , y ) → x = dim y ( PO requires equidimensionality)

(Inc-T1)

¬ Inc ( x , x ) ( Inc irreflexive)

(Inc-T2)

Inc ( x , y ) → Inc ( y , x ) ( Inc symmetric)

(Inc-T3)

x = dim y → ¬ Inc ( x , y ) (equidimensionality prevents Inc )

(Inc-T4)

Inc ( x , y ) → x < dim y ∨ y < dim x ( Inc requires comparability of entities)

(SC-T1)

SC ( x , y ) ↔ C ( x , y ) ∧ ¬ ∃ z [ Cont ( z , x ) ∧ P ( z , y ) ] ∧ ¬ ∃ z [ P ( z , x ) ∧ Cont ( z , y ) ] ( SC expressed in terms of Cont , C, and P)

(SC-T2)

¬ SC ( x , x ) ( SC irreflexive)

(SC-T3)

SC ( x , y ) → SC ( y , x ) ( SC symmetric)

(SC-T4)

SC ( x , y ) → ∃ z [ z < dim x ∧ z < dim y ∧ Cont ( z , x ) ∧ Cont ( z , y ) ] ( SC requires a shared entity of a lower dimension)

(SC-T5)

SC ( x , y ) ∧ Cont ( z , x ) ∧ Cont ( z , y ) → z < dim x ∧ z < dim y (anything shared by two regions in superficial contact must be of a lower-dimension)

3.3.1. Lattice of contact relations

The three defined relations PO , Inc , and SC form a set jointly exhaustive, pairwise disjoint (JEPD) specializations of contact C in CODI shown in Fig. 3. This is proved via the following theorems, where CD-T1 to T4 show that the three relations are exhaustive subrelations of C and CD-T5 to CD-T10 show that they are pairwise disjoint.

OPEN IN VIEWER

Fig. 3.

Lattice of the contact relations in CODI .

(CD-T1)

PO ( x , y ) → C ( x , y ) ( PO specializes C)

(CD-T2)

SC ( x , y ) → C ( x , y ) ( SC specializes C)

(CD-T3)

Inc ( x , y ) → C ( x , y ) ( Inc specializes C)

(CD-T4)

C ( x , y ) → PO ( x , y ) ∨ SC ( x , y ) ∨ Inc ( x , y ) ( PO , SC , and Inc are exhaustive w.r.t. C)

(CD-T5)

PO ( x , y ) → ¬ SC ( x , y )

(CD-T6)

PO ( x , y ) → ¬ Inc ( x , y )

(CD-T7)

SC ( x , y ) → ¬ PO ( x , y )

(CD-T8)

SC ( x , y ) → ¬ Inc ( x , y )

(CD-T9)

Inc ( x , y ) → ¬ PO ( x , y )

(CD-T10)

Inc ( x , y ) → ¬ SC ( x , y )

OPEN IN VIEWER

Fig. 4.

Lattice of nine base relations in CODI based on containment and contact.

To construct a complete lattice of the various contact and containment relations, we introduce four more definitions purely for brevity and convenience:

(DC-P)

DC ( x , y ) ↔ ¬ C ( x , y ) (disconnection)

(PPO-D)

PPO ( x , y ) ↔ PO ( x , y ) ∧ ¬ P ( x , y ) ∧ ¬ P ( y , x ) (Proper partial overlap)

(PInc-D)

PInc ( x , y ) ↔ Inc ( x , y ) ∧ ¬ Cont ( x , y ) ∧ ¬ Cont ( y , x ) (Proper incidence)

( Cont < -D)

Cont < ( x , y ) ↔ Cont ( x , y ) ∧ x < dim y (Lower-dimensional containment)

By proving two more specializations (C-T6, Cont < -T1), we have constructed the lattice of spatial relations for CODI JEPD ∪ {DC-P, PPO-D, PInc-D, Cont < -D} shown in Fig. 4. It consists of the nine jointly exhaustive, pairwise disjoint (JEPD) base relations PPO , PP , =, PP − 1 , Cont < , Cont < − 1 , PInc , SC , and DC .

(C-T6)

Cont ( x , y ) → C ( x , y )

( Cont < -T1)

Cont < ( x , y ) → Inc ( x , y )

This section presents our axiomatizations for the closure operations of intersection and relative complement (difference) as extension to CODI and CODI at . We verify that the operations are well-defined functions, i.e. for each pair of elements x, y, only one element qualifies as potential intersection and only one as potential difference, and show that the axioms suffice to guarantee that CODI ↓ at , the extension of CODI at , satisfies the decomposability property, which requires all entities to be decomposable into a set of non-overlapping and jointly covering minimal entities. The proposed axioms for the operations are informed by Gotts’ previous work (Gotts, 1996) and Casati and Varzi’s detailed study of mereological and topological closure operations in unidimensional mereotopologies (Casati and Varzi, 1999) but go beyond those used in prior multidimensional mereotopologies by not restricting the operations to only pairs of entities of equal dimension.

If we want to ensure that the entities resulting from the operations are again of uniform dimension (i.e., each component of such a region is of the same dimension), the closure operations must be necessarily lossy in that they lose pieces of the intersection or difference that are of lower dimensions than other pieces. As the result, the operations violate a number of properties typically associated with product and difference operations in set theory, such as associativity of intersections: a · ( b · c ) = ( a · b ) · c .

4.1. Intersections

We already have distinguished contact relations depending on the relative dimensionality of the shared region. But this only considers the shared region of greatest dimension. Consider for example Fig. 1(a): the two 2D regions r and s share l as a common piece of boundary (a 1D region) but also the point p (a 0D region), which is unrelated to l. Likewise, a 1D curve could properly intersect a 2D region in a curve segment, while also meeting the 2D region at a separate point. The problem with these cases is that the full intersection could consist of scattered pieces of varying dimensions. To yield a valid region we must ensure that the pieces are of uniform dimension. This is achieved by dropping extra lower-dimensional pieces from the intersection, thus defining the intersection x · y as the maximal intersection of highest dimension among all entities shared by the regions x and y (Int-A1–Int-A4). This intersection could still consist of scattered parts (e.g, the intersection between x and y in Fig. 1(c)) as long as they are of equal dimension. All other, lower-dimensional entities are lost unless they are contained in the intersection of highest dimension, in which case they are still contained in the intersection by transitivity of containment.

We can now verify that the intersection operation · is well-defined in CODI ∪ {Int-A1–Int-A4} , that is, for every pair of elements x, y, one and only one element meets all requirements from Int-A1–Int-A4 to serve as x · y .15

¹⁵

By the nature of · being a function, for every model M and every of elements x, y in its domain Dom ( M ) , some entity z ∈ Dom ( M ) exists such that z = x · y . Thus, we only need to prove that no other entity in Dom ( M ) satisfies the axioms Int-A1–Int-A4 as well. The same applies to the proofs for Theorems 2 and 3.

Theorem 1.

The operation · is well-defined in CODI ∪ {Int-A1–Int-A4} , that is, any two models M and M ′ of CODI ∪ {Int-A1–Int-A4} with equivalent extensions for all non-logical symbols apart from · must have equivalent extensions · M = · M ′ .

In other words, if two models M and M ′ of CODI ∪ {Int-A1–Int-A4} were equivalent (i.e. with equivalent domains and predicate extensions) except for their interpretations · M and · M ′ , then for arbitrary x , y ∈ Dom ( M ) (and thus, because of the equivalence, x , y ∈ Dom ( M ′ ) ), if z = x · M y and z ′ = x · M ′ y , then z = z ′ .

Proof.

Let M and M ′ be arbitrary models with x, y being arbitrary elements in their domains Dom ( M ) = Dom ( M ′ ) . Then we need to prove that any two z , z ′ ∈ Dom ( M ) that satisfy all conditions for z = x · M y and z ′ = x · M ′ y are indeed equivalent.

Since · is a function, some entity z ∈ Dom ( M ) exists such that z = x · M y .

It remains to prove the uniqueness.

Two cases are considered: (1) when ⟨ x , y ⟩ ∉ C M ;16

¹⁶

The bold symbols, such as C M or ZEX M are used to refer to the predicates’ extensions in a model M . But for any of the dimensional comparison predicates, we use a bold infix notation, such as x ⩽ dim y , instead of the longer statement ⟨ x , y ⟩ ∈ ( ⩽ dim ) M to denote that x is related to y in a model M .

(2) when ⟨ x , y ⟩ ∈ C M .

Case (1): z = x · M y where z ∈ ZEX M satisfies all conditions: Int-A1 is trivial, while Int-A2, Int-A3, and Int-A4 are vacuously true because x · M y ∈ ZEX M and ⟨ z , x ⟩ ∉ Cont M and ⟨ z , x ⟩ ∉ P M by C-A4 and EP-D. Moreover, by D’-A4, there is a unique z with z ∈ ZEX M in the model. So if z ′ ∈ ZEX M ′ , we must have z = z ′ because the two extensions of ZEX are identical. If z ′ ∉ ZEX M ′ , then ⟨ x , y ⟩ ∈ C M ′ as shown in the proof of Int-T6 (the converse direction of Int-A1). Then we also have ⟨ x , y ⟩ ∈ C M . But by Int-A1 this contradicts that ⟨ x , y ⟩ ∉ C M .

Case (2): Assume ⟨ x , y ⟩ ∈ C M . Then by C-D, there must exist some z ∈ Dom ( M ) such that ⟨ z , x ⟩ , ⟨ z , y ⟩ ∈ Cont M . Let Z ( { x , y } ) be the set of all z ∈ Dom ( M ) that satisfy this condition, i.e. Z ( { x , y } ) = { z ∗ ∈ Dom ( M ) ∣ ⟨ z ∗ , x ⟩ , ⟨ z ∗ , y ⟩ ∈ Cont M } . Any z , z ′ ∈ Z satisfies Int-A1 (vacuously) and Int-A2 when substituted for x · M y and x · M ′ y . Further, because the entities in Z form a bounded discrete linear pre-order by D’-A6 to D’-A9 with some maximal dimension, a non-empty subset Z ( { x , y } ) max-dim of the elements of greatest dimension within Z exists, defined as Z ( { x , y } ) max-dim = { z ∗ ∈ Z ∣ ∀ z ⋆ [ z ⋆ ∈ Z → z ⋆ ⩽ dim z ∗ ] } . Any element from Z ( { x , y } ) max-dim that is chosen as the intersection x · M y or x · M ′ y then satisfies Int-A3. Int-A4 further postulates that at least one region, denoted as x · y , in Z max-dim contains all regions in Z max-dim (i.e. that are both contained in x and y and of the same dimension as x · y ) as parts. Likewise, z ′ contains all regions in Z max-dim .

Because the extensions P M and P M ′ are equivalent, we have ⟨ z , z ′ ⟩ ∈ P M and ⟨ z ′ , z ⟩ ∈ P M . Thus, z = z ′ by EP-T2. □

Typical properties of intersection/product operations are: commutativity ( x · y = y · x ), idempotence ( x · x = x ), existence of an identity 1 ( 1 · x = x · 1 = x ), existence of a zero element 0 ( 0 · x = x · 0 = 0 ), and associativity ( ( x · y ) · z = x · ( y · z ) ).

Commutativity and idempotence are easily proved (Int-T5,T10), and the zero region serves as null element (Int-T13), while an identity element would require postulating that a universal region that contains every nonzero region exists: ∃ x ∀ y [ ¬ ZEX ( y ) → Cont ( y , x ) ] . The theorems Int-T6–T9 further verify the correct dimensionality of the intersection for the four exhaustive cases of ¬ C  – the only case that leads to an empty intersection – and the three pairwise disjoint, jointly exhaustive kinds of connection partial overlap PO , incidence Inc , and superficial contact SC .

(Int-T5)

x · y = y · x (intersection commutative)17

¹⁷

Note that Int-T6 simplifies the proof of Int-T5, thus we proof Int-T6 first.

(Int-T6)

ZEX ( x · y ) ↔ ¬ C ( x , y ) (zero intersection only for disconnected entities)

(Int-T7)

PO ( x , y ) → x = dim x · y ∧ y = dim x · y (for partial overlap x · y is of the same dimension as both intersecting entities)

(Int-T8)

[ Inc ( x , y ) ∧ x < dim y ] → [ x · y = dim x ∧ x · y < dim y ] (for incidence x · y has the same dimension as one of the intersecting entities and a lower dimension than the other)

(Int-T9)

SC ( x , y ) → x · y < dim x ∧ x · y < dim y (for superficial contact x · y is of a lower dimension than both x and y)

(Int-T10)

x · x = x (· is idempotent)

(Int-T13)

ZEX ( x ) → ZEX ( x · y ) (existence of a null element for ·)

Associativity, that is, the identity ( x · y ) · z = x · ( y · z ) , is the only property of the set-theoretic intersection operation that is no longer guaranteed in our multidimensional mereotopology in cases where one of the intersections x · y or y · z is nonuniform as exemplified in Fig. 1(a). Our intersection operation satisfies only weaker forms of associativity, known as the left- and right-alternative laws (Int-T11,T12), because of the way it is defined to drop lower-dimensional pieces from the intersection.

(Int-T11)

( x · x ) · y = x · ( x · y ) (· left-alternative)

(Int-T12)

y · ( x · x ) = ( y · x ) · x (· right-alternative)

4.2. Differences

Models of unidimensional mereotopologies are usually closed under complementation in the sense that some universal region U exists that contains all other nonzero regions, and every region y has a complement y ′ = U − y . But even without a universal entity, it is reasonable to require that relative complements exist: any region y that is a proper part of a region x has a nonzero relative complement x − y . Inspired by set theory, we refer to − as the difference operation.

To ensure that in a multidimensional mereotopology the difference x − y has a uniform dimension, we again only take the pieces of largest dimension into account, similar to how the intersection operation drops lower-dimensional pieces in the intersection. Thus, whenever the difference is not empty, it has the same dimension as the minuend x (Dif-A1). For two regions of equal dimension, the difference matches the definitions from unidimensional mereotopology (Galton, 1996; Gotts, 1996), as exemplified by the difference between the 2D regions in Fig. 1(b). Likewise, the difference between two 1D regions, e.g. between y and x · y in Fig. 1(c), is a 1D region. This idea extends to differences whose subtrahend is of a greater dimension than the minuend (Dif-A3), as exemplified by the difference y − x between the line segment y and the 2D region x in Fig. 1(c), which is a line segment that is a proper part of y. But when the minuend is of a greater dimension than the subtrahend, the difference must be the minuend itself (Dif-A2), ignoring missing lower-dimensional artifacts (e.g., x − y = x in Fig. 1(c)). This works in general because the intersection never has a greater dimension than either of the intersecting regions. Dif-T7 verifies that the difference between x and y is indeed equivalent to the difference between x and the intersection of x and y. Dif-A4 captures the exact conditions when the difference may be empty: either the minuend is zero or the minuend is contained in the subtrahend. From reflexivity of Cont for nonzero regions, it follows that x − x is always the zero region.

We define the theory18

¹⁸

http://colore.oor.net/multidim_mereotopology_codi/codi_down.clif

CODI ↓ = CODI ∪ {Int-A1–Int-A4, Dif-A1–Dif-A4} and its atomic variant as19

¹⁹

http://colore.oor.net/multidim_mereotopology_codi/codi_down_atomic.clif

CODI ↓ at = CODI ↓ ∪ { ME -E1 } Because − is a function, differences must exist even for any combination of two entities, including the difference x − x , which must be the zero region. Thus CODI ↓ and CODI ↓ at both entail that some zero region must exist (Z-T1).

We next prove theorems about the behavior of the difference operation that are prerequisites to prove that it is a well-defined function and satisfies the desired supplementation principles from unidimensional mereotopology. The first three theorems Dif-T1–T3 confirm the relationship of x − y to x and y. More precisely, they show that the difference x − y correctly deals with all the parts of x and y: (1) x − y is a part of x (unless it is empty) (Dif-T1); (2) if y is a proper part of x, then the complementary difference x − y is also a proper part of x (Dif-T2); and (3) nothing can be a part of both y and x − y (Dif-T3).

(Dif-T1)

¬ ZEX ( x − y ) → P ( x − y , x ) (a nonempty difference x − y is part of x)

(Dif-T2)

PP ( y , x ) → PP ( x − y , x ) (for a proper part y of x, x − y is also a proper part of x)

(Dif-T3)

¬ PO ( x − y , y ) (y and x − y do not partially overlap)

The next theorems consider the interaction between the intersection and difference operations. Dif-T4 confirms that the intersection x · y and the difference x − y never overlap, while Dif-T5 shows that the difference can be described in terms of parthood alone.20

²⁰

Recall that PO denotes overlap in a part rather than proper overlap and thus includes full containment. Thus PO is the most general overlap relation between unidimensional entities similar to O as used by Casati and Varzi (1999), Cohn et al. (1997), and Randell et al. (1992).

Dif-T6,T7 capture further interaction between the intersection and difference operations that are maintained from intersections and differences in set theory, ensuring that x − y = x − ( x · y ) = x · ( x − y ) holds as expected. Dif-T6 specifically confirms the remainder principle known from mereology (Simons, 1987).

(Dif-T4)

¬ PO ( x − y , x · y ) ( x · y and x − y do not partially overlap)

(Dif-T5)

P ( z , x − y ) ↔ P ( z , x ) ∧ ¬ PO ( z , x · y ) (parts of the difference x − y )

(Dif-T6)

x − y = x − ( x · y ) ( x − y and x − ( x · y ) are identical)

(Dif-T7)

x − y = x · ( x − y ) ( x − y and its intersection with x are identical)

The last three theorems Dif-T8–T10 verify that the difference operations works correctly in borderline case: (1) for a part y of x, y is the difference between x and x − y (Dif-T8); (2) for identical regions x and y, both differences x − y and y − x are empty (Dif-T9); and (3) regions in superficial contact, which only share a lower-dimensional region, the difference x − y equals x and, likewise, y − x = y .

(Dif-T8)

P ( y , x ) → y = x − ( x − y ) (− involutary)

(Dif-T9)

x = y ↔ ZEX ( x − y ) ∧ ZEX ( y − x ) (− anticommutative)

(Dif-T10)

SC ( x , y ) → x − y = x (difference between entities in superficial contact)

In set theory, the intersection and difference operations are interdefinable through the equivalence x · y = x − ( x − y ) . Because of CODI ↓ ’s lossy operations that ensures all regions have uniform dimensions, the same equivalence is not guaranteed as demonstrated by x and y in Fig. 1(c): x · y yields a segment of y, while x − y = x because y has a lower dimension than x. Then x − ( x − y ) = x − x , yielding the zero region rather than the lower-dimensional intersection of x and y. Thus, intersections and differences must be axiomatized separately in CODI though many of the relationships between the operations from set theory are still preserved.

4.3. Supplementation and extensionality principles

Important criteria for evaluating unidimensional mereological and mereotopological theories are supplementation principles (Casati and Varzi, 1999; Simons, 1987). Its weakest form requires each part of a region to be complemented by some other non-overlapping part of the same region (EP-E1). The stronger variant requires every region that is not a part of x to have a proper part that does not overlap x (EP-E2) and thus is also not a part of x. Both are provable in CODI ↓ . While EP-E1 and EP-E2 only consider the supplementation by equi-dimensional entities, EP-E2 can be further generalized to multidimensional cases: every region y not contained in x has a part z such that the intersection z · x is of a lower dimension than z (EP-E3), meaning that z does not share a part with x. EP-E3 is also provable in CODI ↓ . In fact, all of three principles are consequences of the remainder principle (Dif-T6), which strengthens strong supplementation further.

These supplementation principles are a crucial step towards our ultimate goal of establishing decomposability for regions in models of CODI ↓ at such that every region is identified by a finite sum of minimal parts. Towards this goal, strong supplementation already entails that the partial overlap relation PO is extensional (PO-E2) in CODI ↓ , which ensures that every entity is uniquely identified by its overlapping regions. This also means that monotonicity of the PO relation implies parthood.

(PO-E1)

¬ ZEX ( x ) ∧ ∀ z [ PO ( z , x ) → PO ( z , y ) ] → P ( x , y ) (monotonicity of PO implies parthood)

(PO-E2)

∀ z [ PO ( z , x ) ↔ PO ( z , y ) ] → x = y ( PO extensional)

Dif-T5 together with extensionality of parthood (EP-E9) now help prove that the difference x − y , like the intersection operation ·, is indeed well-defined for every pair of elements x, y in a model of CODI ↓ .

Theorem 2.

The operation − is well-defined in CODI ↓ , that is, for any two models M and M ′ of CODI ↓ with identical extensions of all predicates and of ·, if z , z ′ ∈ Dom ( M ) = Dom ( M ′ ) with z = x − M y and z ′ = x − M ′ y , then z = z ′ .

Proof.

Let M and M ′ be two models of CODI ↓ with identical extensions of all predicates and of ·. Let x and y be two arbitrary entities in Dom ( M ) = Dom ( M ′ ) .

Since − is a function, some entity z ∈ Dom ( M ) exists such that z = x − M y . It remains to prove the uniqueness. Suppose that z = x − M y and z ′ = x − M ′ y .

If x > dim y , then by Dif-A2, z = x − M y = x and also z ′ = x − M ′ y = x , thus z = z ′ .

If x ∈ ZEX M , then by Dif-A4, z = x − M y ∈ ZEX M and z ′ = x − M ′ y ∈ ZEX M . Then z = x = z ′ by D’-A4.

Now assume x ∉ ZEX M . If z = x − M y ∈ ZEX M , then ⟨ x , y ⟩ ∈ Cont M by Dif-A4 and further ⟨ x , y ⟩ ∈ Cont M ′ by the theorems assumption and then z ′ = x − M ′ y ∈ ZEX M again by Dif-A4. Analogously, if z ′ = x − M ′ y ∈ ZEX M then z = x − M y ∈ ZEX M . In either case z = z ′ by D’-A4.

Now assume that x , z , z ′ ∉ ZEX M and x ≯ dim y , that is, x ⩽ dim y .

Then ⟨ z , x ⟩ ∈ P M by Dif-T1 and hence z = dim x by EP-D. Analogously z ′ = dim x .

We can use Dif-T5 to determine the set of parts v ∈ Dom ( M ) of both differences z = x − M y and z ′ = x − M ′ y . Note that the set of parts of x, i.e. the v ∈ Dom ( M ) with ⟨ v , x ⟩ ∈ P M = P M ′ , is unique by EP-T9.

If ⟨ v , x ⟩ ∉ P M , then ⟨ v , z ⟩ ∉ P M and ⟨ v , z ′ ⟩ ∉ P M ′ , both by Dif-T5.

If ⟨ v , x ⟩ ∈ P M , then by Dif-T5, ⟨ v , z ⟩ ∈ P M iff ⟨ v , x · M y ⟩ ∉ PO M . Likewise, ⟨ v , z ′ ⟩ ∈ P M ′ iff ⟨ v , x · M ′ y ⟩ ∉ PO M ′ .

Since P M = P M ′ , PO M = PO M ′ and · M = · M ′ by the theorem’s assumption, we have ⟨ v , z ⟩ ∈ P M iff ⟨ v , z ′ ⟩ ∈ P M . Hence z = z ′ by EP-T9. □

OPEN IN VIEWER

Fig. 5.

A model of CODI ↓ at (top) decomposed by intersections and differences into its atomic entities: points p1–p7 (right), linear features l3, which is not further decomposed, and l7–l19 (center), and areas a4–a8 (left), shown in the bottom figures. Non-atomic entities are sums of atomic ones, e.g., a 3 = a 5 ∪ a 7 ∪ a 8 and l 5 (the boundary of a2) equals to l 9 ∪ l 10 ∪ l 14 ∪ l 13 . Because of the existence of complements, additional non-atomic entities are entailed to exist: a 3 · a 1 = a 5 ∪ a 7 and l 5 − l 9 = l 10 ∪ l 14 ∪ l 13 .

4.4. Decomposability of atomic models of CODI ↓

Extensionality of the PO relation (PO-E2) means that any entity in a model of CODI ↓ at is fully described by the entities it overlaps. For atomic models we can go a step further by proving that each region can be decomposed into a set of minimal, covering and non-overlapping parts. This property, called decomposability (Varzi, 2007) and illustrated by Fig. 5, holds in many mereologies and unidimensional mereotopologies. We now confirm that decomposability follows in the atomic version CODI ↓ at of our multidimensional mereotopology from the extensionality of PO (PO-E2) and the strong supplementation principle (EP-E2). It can also be captured as the logical sentence PO-E3.

(PO-E3)

∀ z [ Min ( z ) → [ PO ( z , x ) ↔ PO ( z , y ) ] ] → x = y ( PO extensional for minimal entities)

The property may not hold in non-atomic models, where some entity may contain infinitely many smaller parts.

In any model of CODI ↓ at all nonzero regions contain some minimal, i.e., indivisible, proper part. Proving decomposability then amounts to showing that the models are atomistic, that is, proving that every two partially overlapping regions share some minimal part. Then, any region is the sum of its minimal parts and those minimal parts uniquely define the region. This also means that each region in contact with a given region x shares a, possibly lower dimensional, region contained in some minimal part of x. In other words, the containment of lower-dimensional regions in models of the multidimensional mereotopology CODI ↓ at does not significantly alter the models’ structure that is still defined – as in most unidimensional mereotopologies – by (equidimensional) parthood. Instead, the additional structure from containment of lower-dimensional works within the confines of the models’ parthood structure.

Theorem 3.

Let M be a model of CODI ↓ at . Then every entity x ∈ Dom ( M ) has a unique set of minimal parts that partition the entity.

Proof.

Let M be a model of CODI ↓ at with domain M = Dom ( M ) .

By ME-E1, we have M ⊨ ∀ x [ ¬ ZEX ( x ) → ∃ y [ P ( y , x ) ∧ Min ( y ) ] ] .

Recall that by PO-E2, every entity x ∈ M has a unique extension of PO that involves x: PO M ( x ) = { ⟨ x , w ⟩ ∣ ⟨ x , w ⟩ ∈ PO M } .

Choose an arbitrary x ∈ M . We need to prove that x has a unique set PO M Min ( x ) ⊆ PO M ( x ) that relates x to the minimal entities it overlaps: PO M Min ( x ) = { ⟨ x , w ⟩ ∣ ⟨ x , w ⟩ ∈ PO M and w ∈ Min M } ⊆ PO M ( x ) = { ⟨ x , w ⟩ ∣ ⟨ x , w ⟩ ∈ PO M }

Now suppose there exists another entity x ′ ∈ M with x ′ ≠ x that partially overlaps the same set of minimal entities as x, i.e., PO M Min ( x ′ ) = PO M Min ( x ) . From x ′ ≠ x , either (i) ⟨ x ′ , x ⟩ ∈ PP M or (ii) ⟨ x ′ , x ⟩ ∉ P M .

Consider the case (i) when ⟨ x ′ , x ⟩ ∈ PP M . Then by EP-E1, some z ∈ M exists such that ⟨ z , x ′ ⟩ ∈ P M and ⟨ z , x ⟩ ∉ PO M . Then z ∉ ZEX M by EP-D and C-A4. Then by ME-E1, some minimal entity w ∈ M exists such that ⟨ w , z ⟩ ∈ P M and hence ⟨ w , x ′ ⟩ ∈ P M by transitivity of P (EP-T3) and ⟨ w , x ′ ⟩ ∈ PO M by PO-D. But at the same time ⟨ w , x ⟩ ∉ P M by PO-D. Hence w ∈ PO M Min ( x ′ ) and w ∉ PO M Min ( x ) by PO-D.

Consider the case (ii) where ⟨ x ′ , x ⟩ ∉ P M . Then by EP-E2 some w ∈ M exists such that ⟨ w , x ′ ⟩ ∈ P M and ⟨ w , x ⟩ ∉ PO M . Such a w would – by ME-E1 – contain a minimal entity v ∈ M . Then ⟨ x , v ⟩ ∉ PO M Min but ⟨ x ′ , v ⟩ ∈ PO M Min , which contradicts the assumption that x ′ and x partially overlap the same minimal entities.

Notice that because every entity y ∈ PO M Min ( x ) is minimal, i.e., each y has itself as only part, we conclude by definition PO-D that PO M Min ( x ) = P M Min ( x ) . Thus, any region x is uniquely defined by its minimal parts, i.e., by the set P M Min ( x ) , in a model of CODI ↓ at . □

Because distinct minimal entities cannot overlap and entities that partially overlap must share a minimal part, the minimal parts of a region x form a spatial partition of x: they are pairwise non-overlapping and they are exhaustive, i.e., any other region in contact with x must be in contact with one of its minimal parts.

5. Extending CODI ↓ with a sum operation

The previous section has focused on downwards mereological closure operations that decompose spatial entities into their minimal parts. Similarly, we can close models of the multidimensional mereotopology upwards by introducing sums of every pair of entities. While arbitrary sums are not always meaningful as discussed to length by Casati and Varzi (1999), they are still valuable when the domain of discourse are abstract spatial regions rather than physical or other kinds of objects. For that reason, most unidimensional and multidimensional mereotopologies postulate the existence of arbitrary sums. But postulating the existence of sums of arbitrary entities may again lead to entities of nonuniform dimension. For example, the sum consisting of a region, a line, and a set of points in which the line and the points are not contained in the region is not of uniform dimension and as such cannot be an entity in a model of our multidimensional theory. But consistent with our formalization of intersections and differences, we can treat sums of entities of different dimensions as the sum of the entities contained in the entity of higher dimension (Sum-A3). The sum of two entities of different dimensions will always yield the higher-dimensional entity (Sum-A2). That means sums will only be meaningful for two equidimensional entities, just as in other multidimensional mereotopologies (Baumann et al., 2016; Galton, 1996; Gotts, 1996). Note that our axiomatization of closure under sums requires models to already be closed under intersections and differences. Sum-A4 then ensures that the sum and difference operations interact correctly.

We define the theory21

²¹

http://colore.oor.net/multidim_mereotopology_codi/codi_down_sum.clif

CODI ↓ − sum = CODI ↓ ∪ {Sum-A1–Sum-A4} and its atomic variant as22

²²

http://colore.oor.net/multidim_mereotopology_codi/codi_down_sum_atomic.clif

CODI ↓ − sum at = CODI ↓ − sum ∪ { ME -E1 }

In the extended theory CODI ↓ − sum , the theorems Sum-T1–Sum-T6 verify basic property of the sum, such as idempotence (Sum-T2) and associativity (Sum-T7), the expected behaviour when the zero entity (Sum-T3,4) or two equidimensional entities (Sum-T5) are involved, and the correct interaction with the containment and partial overlap relations (Sum-T1, Sum-T6).

(Sum-T1)

Cont ( z , x + y ) → ∃ v [ P ( v , z ) ∧ [ Cont ( v , x ) ∨ Cont ( v , y ) ] ] (every z contained in x + y has some part contained in x or in y)

(Sum-T2)

x + x = x (+ idempotent)

(Sum-T3)

ZEX ( x + y ) ↔ ZEX ( x ) ∧ ZEX ( y ) (zero sum of zero entities)

(Sum-T4)

ZEX ( y ) → x + y = x (sum with zero entity)

(Sum-T5)

x = dim y → x = dim x + y (dimension of the sum of equidimensional entities)

(Sum-T6)

x = dim y → ∀ z [ PO ( z , x ) ∨ PO ( z , y ) ↔ PO ( z , x + y ) ] ( x + y partially overlaps anything that overlaps either x or y)

(Sum-T7)

( x + y ) + z = x + ( y + z ) (+ associative)

Sum-T6 is also necessary to prove that the sum operation is, similarly to the intersection and difference operations, well-defined for any pair x and y in a model of CODI ↓ ∪ {Sum-A1–Sum-A4} .23

²³

http://colore.oor.net/multidim_mereotopology_codi/codi_down_sum.clif

Theorem 4.

The operation + is well-defined in CODI ↓ ∪ {Sum-A1–Sum-A4} , that is, for any two models M and M ′ of CODI ↓ ∪ {Sum-A1–Sum-A4} with identical extensions of all predicates, if z , z ′ ∈ Dom ( M ) = Dom ( M ′ ) with z = x + M y and z ′ = x + M ′ y , then z = z ′ .

Proof.

Let M , M ′ be two models of CODI ↓ ∪ {Sum-A1–Sum-A4} with equivalent extensions for all predicates (but not necessarily for +). Let x and y be arbitrary entities in their domains Dom ( M ) = Dom ( M ′ ) .

Case 1: Assume x and y have different dimensions, i.e., x ≠ dim y . Then the sums x + M y and x + M ′ y are uniquely defined as x (if x > dim y ) or y (if y > dim x ) by Sum-A2 and Sum-A1 and thus z = z ′ .

Case 2: Assume x = dim y . Then M ’s extension of PO for z = x + M y , i.e. the set PO M ( x + y ) defined as { v ∈ Dom ( M ) ∣ ⟨ v , x + M y ⟩ ∈ PO M } , is uniquely determined by Sum-T6 as v ∈ PO M ( x + M y ) ⇔ ⟨ v , x ⟩ ∈ PO M or ⟨ v , y ⟩ ∈ PO M Likewise, v ∈ PO M ′ ( x + M ′ y ) ⇔ ⟨ v , x ⟩ ∈ PO M ′ or ⟨ v , y ⟩ ∈ PO M ′ With PO M = PO M ′ by the theorem’s assumption, v ∈ PO M ( x + M y ) ⇔ v ∈ PO M ( x + M ′ y ) follows. Hence by extensionality of PO (PO-E2), z = x + M y = x + M ′ y = z ′ . □

We now proceed to prove that every part in the sum x + y can be split into parts u and v so that P ( u , x ) and P ( v , y ) without PO ( u , v ) (Sum-T9) and that the sum of two parts of z is also a part of z (Sum-T10). In other words, the sum x + y does not contain a part that is neither in x, nor in y, nor can be divided into two parts that are in x and y, respectively. To prove Sum-T9, we first prove Sum-T8, which establishes that the difference and sum operations cancel each other out for two entities in a parthood relation, i.e., if we subtract a part y from x and then add it again, we obtain x again. This then allows to prove the more general relationship Sum-T8’ that ties the intersection, difference and sum operations together by showing that the sum of the intersection x · y and the difference x − y is again x – regardless of the relative dimensions of x and y. In that way, Sum-T8’ captures the essence of Dif-T5 using the sum operation. Note that Sum-T8’ is a special case of Sum-T8 because a nonemtpy intersection x · y is always contained in x, and x · y is always a part of x as long as they are of equal dimension.

Sum-T8’ then proves the first of six conditions in Sum-T9 when a w is contained in the sum x + y but not fully contained in either x or y. Sum-T9’ is a more general expression of Sum-T9 using existential quantifiers. Sum-T9 helps us then with the proof of Sum-T10, which verifies that the sum of two parts of z is also a part of z and vice versa.

(Sum-T8)

P ( y , x ) → x = y + ( x − y ) (any part y of x and the difference x − y cover x)

(Sum-T8’)

x = ( x · y ) + ( x − y ) ( x · y and x − y cover x)

(Sum-T9)

Cont ( w , x + y ) → Cont ( w , x ) ∨ Cont ( w , y ) ∨

[ P ( w − x , w ) ∧ P ( w · x , w ) ∧ ¬ PO ( w · x , w − x ) ∧ Cont ( w − x , y ) ∧ Cont ( w · x , x ) ] (Any w in x + y is either in x, in y, or can be split into non-overlapping parts w · x and w − x contained in x and y)

(Sum-T9’)

Cont ( w , x + y ) ∧ ¬ Cont ( w , x ) ∧ ¬ Cont ( w , y ) → ∃ u , v [ w = u + v ∧ P ( v , w ) ∧ P ( u , w ) ∧ ¬ PO ( u , v ) ∧ Cont ( v , y ) ∧ Cont ( u , x ) ] (everything contained in x + y but contained neither in x nor in y is the sum of two non-overlapping parts contained in x and y)

(Sum-T10)

x = dim y ∧ ¬ ZEX ( x ) → ∀ z [ Cont ( x , z ) ∧ Cont ( y , z ) ↔ Cont ( x + y , z ) ] (the sum x + y is part of z iff x and y are part of z)

In a final step towards a full characterization of the models of CODI ↓ ∪ {Sum-A1–Sum-A4} , we are studying distributivity. Most importantly, for two entities y and z of equal dimensions, a third entities’ intersection distributes over their sum (Sum-T11) and its sum distributes over their intersection (Sum-T14). If y and z are not of the same dimension, this is not necessarily true. In Fig. 5, for example, consider the intersection a 8 · ( a 2 + l 8 ) . Because a 2 is of a greater dimension than l 8 , the line segment l 8 is dropped from the sum a 2 + l 8 . Then a 8 · ( a 2 + l 8 ) = a 8 · a 2 = l 9 . But the sum a 8 ( a 2 ) + a 8 ( l 8 ) is larger, namely l 8 + l 9 , because the intersections a 8 · a 2 = l 9 and a 8 · l 8 = l 8 are of the same dimensions and the piece l 8 that happens to be contained in a 8 is no longer dropped.

Finally, we prove that x’s sum of the difference with a second entity y is the union of the two entities (Sum-T20) – as is the case for set union and difference. Sum-T8 can then be considered a special case of Sum-T20. Sum-T20 is the final missing piece for the subsequent representation of the finite models of CODI ↓ ∪ {Sum-A1–Sum-A4} .24

²⁴

Additional properties about how the sum operation interacts with intersections and differences have been presented in (Hahmann, 2013) but are omitted here as they are not necessary for Theorem 5.

(Sum-T11)

y = dim z → x · ( y + z ) = ( x · y ) + ( x · z ) (· distributive over + when the operands are of equal dimension)

(Sum-T14)

y = dim z ∧ [ x < dim y · z ∨ x ⩾ dim y ] → x + ( y · z ) = ( x + y ) · ( x + z ) (+ distributive over · when the operands are of equal dimension)

(Sum-T20)

x + ( y − x ) = ( x + y ) (special case when + distributes over −)

5.1. A model-theoretic characterization of CODI ↓ ∪ {Sum-A1–Sum-A4}

We can now show that a model’s extension of the parthood relation in a model of CODI ↓ ∪ {Sum-A1–Sum-A4} is always partitioned into jointly exhaustive, pairwise disjoint substructures of parthood, each of them forming a Boolean algebra (see Fig. 6 for an illustration of the Boolean structure that arises from the 2D regions of the model shown in Fig. 5). Contact between entities within each Boolean substructure is reduced to partial overlap PO , which manifests itself as a non-zero meet within the Boolean algebra. While two entities of the same dimensions can also be in superficial contact, this relation is not manifested in the Boolean substructure but requires identifying a common contained entity in another Boolean substructure of the model. Across the Boolean substructures, entities can be related via incidence Inc or superficial contact SC . Both relations manifest themselves as a non-zero meet over the partial order defined by the Cont relation as x ⩽ y ⇔ Cont ( x , y ) ∨ ZEX ( x ) . Then, the partial order within each Boolean substructure – defined as x ⩽ y ⇔ P ( x , y ) ∨ ZEX ( x )  – is the subset of the relation ⩽ where the entities are in a parthood relation.

OPEN IN VIEWER

Fig. 6.

Hasse diagram illustrating the 16-element Boolean substructure formed by all combinations of the atomic 2D entities a 4 , a 5 , a 6 and a 7 from Fig. 5. With the fifth and last atomic entity a 8 , the full Boolean substructure would have 2 5 = 32 entities for this particular dimension. But to avoid cluttering the illustration, sums involving the atomic entity a 8 are only included where it corresponds to “genuine” sums that involve the named objects a 1 , a 2 , or a 3 from the original configuration at the top of Fig. 5. The ordering relations involving a 8 are shown using dashed lines.

More formally, the relation = dim is an equivalence relation and thus partitions the domain of any model M of CODI ↓ ∪ {Sum-A1–Sum-A4} into sets of entities of equal dimension. The parthood relation P defines a partial order within the set for each dimension and each set defines a mereological field, that is, with the zero entity added as least element (i.e., lower bound), the entities of each dimension form a Boolean algebra.

Theorem 5.

Let M be a model 25

²⁵

We have used the model finders Paradox and Mace4 to construct a model consisting of exactly 2 elements. They can be found at http://colore.oor.net/multidim_mereotopology_codi/output/codi_down_sum.par.out and http://colore.oor.net/multidim_mereotopology_codi/output/codi_down_sum.m4.out, respectively.

of CODI ↓ ∪ {Sum-A1–Sum-A4} with a finite domain Dom ( M ) of size | Dom ( M ) | ⩾ 2 .

For each d ∈ Dom ( M ) with d ∉ ZEX M , let B d = { x ∈ Dom ( M ) ∣ ⟨ d , x ⟩ ∈ ( = dim ) M } ∪ ZEX M . be its set of equidimensional entities with ze ∈ Dom ( M ) as the unique entity in ZEX M that is included in every B d . 26

²⁶

Note that ZEX M is always a singleton set by D’-A4 and Z-T1.

Then define for each set B d a structure M d = ⟨ B d , × , + M , ′ , ze , max ⟩ 27

²⁷

Throughout the proof, we use +, ·, and − to refer to + M , · M , and − M , respectively.

where

x × y = x · y if ⟨ x , y ⟩ ∈ PO M , ze otherwise ;

max ∈ B d ∩ Max M ; and

x ′ = max − x

Then

Each structure M d is a substructure of M closed under −, +, and × and with a unique maximal element max;

Each structure M d is a Boolean algebra;

Any d ∈ Dom ( M ) ∖ { ze } is in a set B d ⊆ Dom ( M ) for exactly one structure M d .

Proof.

We need to show that ( a × b ) , ( a − b ) , ( a + b ) ∈ B a for any a , b ∈ B a . We also need to show that a unique max ∈ B a ∩ Max M exists.

Assume a, b to be arbitrary entities in B a . Then a = dim b by definition.

Closure under intersection ×: If ⟨ a , b ⟩ ∈ PO M , then a × b = a · b and a · b = dim a , b by Int-T7. Hence ( a × b ) ∈ B a by the definition of B a . Otherwise, a × b = ze with ze ∈ B a by definition.

Closure under difference −: By Dif-A1, we have a − b = dim a and thus ( a − b ) ∈ B s unless ( a − b ) ∈ ZEX M in which case a − b = ze ∈ B a .

Closure under sum +: Since a = dim b , a + b = dim a follows by Sum-T5 and thus ( a + b ) ∈ B a .

A unique max ∈ B a ∩ Max M exists: By the definition of B a it is finite and contains at least one entity a such that a ∉ ZEX M and thus Max M is non-empty.

Now suppose two distinct entities a 1 , a 2 ∈ B a ∩ Max M exist. Then by definition of B a , a 1 = dim a 2 and, by Sum-A3 ⟨ a 1 , a 1 + a 2 ⟩ , ⟨ a 2 , a 1 + a 2 ⟩ ∈ Cont M and thus ⟨ a 1 , a 1 + a 2 ⟩ , ⟨ a 2 , a 1 + a 2 ⟩ ∈ P M . Unless a 1 = a 2 = a 1 + a 2 , we either have ⟨ a 1 , a 1 + a 2 ⟩ ∈ PP M or ⟨ a 2 , a 1 + a 2 ⟩ ∈ PP M , which would contradict our assumption that both a 1 and a 2 are in Max M (see ME-D1).

Any distributive bounded lattice equipped with an operation of unique complementation is a Boolean lattice (algebra).

First we show that each structure ⟨ B d , × , + M , ′ , ze , max ⟩ is a bounded distributive lattice if we define for all x , y ∈ B a , x ⩽ y ⇔ ⟨ x , y ⟩ ∈ P M ∨ x ∈ ZEX M . Let a, b, c be arbitrary entities in B a . Then a = dim b = dim c and thereby:

+ defines a supremum, i.e., join operation: a ⩽ a + b because ⟨ a , a + b ⟩ ∈ P M by Sum-T5, Sum-A3, and C-A1 except when a = ze , but ze ⩽ a by definition. Hence a + b is an upper bound for a (and, analogously, for b).

Now suppose that a + b is not the least upper bound, i.e. some d ∈ B a exists such that a , b ⩽ d but d ≱ a + b . We will prove that every e ∈ Dom ( M ) that overlaps a + b (i.e. ⟨ e , a + b ⟩ ∈ PO M ) also overlaps d (i.e. ⟨ e , d ⟩ ∈ PO M ). Assume ⟨ e , a + b ⟩ ∈ PO M for some e ∈ B a . Then by PO-D and EP-D, e , b = dim a + b and further, by Sum-T6 ⟨ e , a ⟩ ∈ PO M or ⟨ e , a ⟩ ∈ PO M . In either case, by a , b ⩽ d and the definition of ⩽ in the lattice, ⟨ e , d ⟩ ∈ P M . Hence ⟨ e , d ⟩ ∈ PO M as desired. Hence by PO-E1, ⟨ a + b , d ⟩ ∈ P M and hence a + b is the least upper bound of a and b.

× defines an infimum, i.e., meet operation: a × b ⩽ a because if ⟨ a × b , a ⟩ ∈ PO M , then by PO-D there exists a c ∈ Dom ( M ) such that ⟨ c , a ⟩ , ⟨ c , b ⟩ ∈ P M . Then c = dim a , b by EP-D and thus c ∈ B a . Further, c ⩽ a and c ⩽ b by definition. If ⟨ a × b , a ⟩ ∉ PO M , then a × b = z e by definition and hence a × b ⩽ a , b .

ze is a minimum: ze ⩽ a by definition of ⩽.

max is a maximum: Suppose max is not a maximum, i.e., there exists an m ∈ B a such that m ≰ max . Then ⟨ m , max ⟩ ∉ P M . If m ∈ ZEX M then m ⩽ max by definition. Otherwise by EP-E2, there exists a d ∈ B a such that ⟨ d , m ⟩ ∈ P M but ⟨ d , max ⟩ ∉ PO M . But since m + max must exist (because + is a function) and m = dim max (because m , max ∈ B a ), then m + max = dim max by Sum-T5 and ⟨ max , m + max ⟩ ∈ P M by Sum-T6 and PO-E1. Because ⟨ d , max ⟩ ∉ PO M but ⟨ d , m + max ⟩ ∈ PO M (by Sum-T6), max ≠ m + max , hence ⟨ max , m + max ⟩ ∈ PP M by EPP-D and, further, max ∉ Max M by ME-D1 in contradiction to our definition of max.

× is distributive over +: a × ( b + c ) = ( a × b ) + ( a × c ) because · is distributive over + by Sum-T11 for any a , b , c ∈ B a . Note that if a × b = ze then ⟨ a , b ⟩ ∉ PO M by definition. Then by Sum-T6, ⟨ a , b + c ⟩ ∈ PO M iff ⟨ a , c ⟩ ∈ PO M . Analogously if a × c = ze .

+ is distributive over ×: a + ( b × c ) = ( a + b ) × ( a + c ) holds by Sum-T14 together with M max being closed under × and +.

The only case of special concern is where b × c = ze . Then by the definition of ×, either b · c = ze or ⟨ b , c ⟩ ∉ PO M . In the former case, ⟨ b , c ⟩ ∉ C M by Int-T6 and ⟨ b , c ⟩ ∉ PO M by CD-T1. In either case, ⟨ b , c ⟩ ∉ PO M .

Note that every entity d ∈ B a with ⟨ d , a ⟩ ∈ PO M satisfies both ⟨ d , a + b ⟩ ∈ PO M and ⟨ d , a + c ⟩ ∈ PO M by Sum-T6. Reversely, if some d ∈ B a exists with ⟨ d , a + b ⟩ ∈ PO M and ⟨ d , a + c ⟩ ∈ PO M , then ⟨ d , a ⟩ ∈ PO M because otherwise by Sum-T6 ⟨ d , b ⟩ ∈ PO M and ⟨ d , c ⟩ ∈ PO M , which by PO-D contradicts our observation that ⟨ b , c ⟩ ∉ PO M .

Thus by PO-E2, a + ( b × c ) = ( a + b ) × ( a + c ) when b × c = ze .

It remains to show that the operation ′ defined as x ′ = max − x is a unique complementation operation in any structure ⟨ B a , × , + M , ′ , ze , max ⟩ . We have:

x + x ′ = max because x + ( max − x ) = x + max by Sum-T20 and further x + max = max because max is the maximum in B a , and

x · x ′ = ze because ⟨ x , max − x ⟩ ∉ PO M by Dif-T3.

Since max is unique in every set B a , max − x is uniquely defined by Theorem 2. Hence x ′ = max − x is a unique complementation operation.

Hence every structure ⟨ B a , × , + M , ′ , ze , max ⟩ is a uniquely complemented distributive lattice and thus by definition a Boolean lattice (algebra).

By its definition, it is clear that every a ∈ Dom ( M ) is in B a . Now suppose there exists a d ∈ Dom ( M ) ∖ { z e } such that d ∈ B a and d ∈ B b for distinct a and b. Then we have d = dim a = dim b and as such B a = B b by the nature of the equivalence relation = dim used to define B a and B b .

Thus the sets B d partition the domain Dom ( M ) of a model of CODI ↓ ∪ {Sum-A1–Sum-A4} , with each structure M d = ⟨ B d , × , + M , − , ze , max ⟩ defining a Boolean algebra that is a substructure of M . □

Note that our characterization is restricted to models with finite domains because we cannot guarantee the existence of sums of infinitely many entities (at least not without employing infinite axiom schemas or second-order logic). However, the theorem extends to infinite models of CODI ↓ ∪ {Sum-A1–Sum-A4} in which a maximal entity exists in each dimension.