Spatial Logic

Origin. Multiple traditions: topology-based (McKinsey-Tarski, 1940s), mereotopology (Whitehead, Clarke), region-based (Randell et al., 1992). Logics for spatial reasoning. Modal interpretations on topological spaces. Region Connection Calculus (RCC) for qualitative spatial relations. Applications in GIS, robotics, image analysis.

Models. Reasoning about space and location. Points, regions, boundaries, connections. Modal operators: interior, closure. Qualitative relations: connected, overlaps, contains. Topological semantics for modal logic. Spatial databases and geographic information.

Formalism.

Topological semantics (S4): Interpret modal logic on topological space (X, τ).

⟦□φ⟧ = Int(⟦φ⟧) (interior)
⟦◇φ⟧ = Cl(⟦φ⟧) (closure)

S4 is complete for this semantics.

Region Connection Calculus (RCC-8): Eight relations between regions: DC (disconnected), EC (externally connected), PO (partial overlap), EQ (equal), TPP (tangential proper part), NTPP (non-tangential proper part), TPPi (inverse), NTPPi (inverse)

Composition tables enable constraint reasoning.

Mereotopology: Combines mereology (part-whole) with topology (connection).

P(x,y): x is part of y
C(x,y): x connects with y
O(x,y): x overlaps y

Modal spatial logic: □φ: everywhere in interior ◇φ: somewhere in closure Near(φ): in closure but not interior

Spatial extension of temporal: 4D spacetime: combine LTL with spatial operators.

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	White square / Box	Interior operator: everywhere inside
◇	U+25C7	White diamond	Closure operator: somewhere in the closure
Int	—	Interior	Topological interior
Cl	—	Closure	Topological closure
⟦	U+27E6	Mathematical left white square bracket	Opens the extension of a formula
⟧	U+27E7	Mathematical right white square bracket	Closes it; ⟦φ⟧ is a subset of the space
X	—	Space	The underlying point set
τ	U+03C4	Greek small tau	The topology on X
C	—	Connection	x connects with y: touch or overlap
P	—	Part	x is part of y
O	—	Overlap	x and y share a part
DC, EC	—	Disconnected, externally connected	The two RCC-8 relations with no shared interior
PO, EQ	—	Partial overlap, equal	Overlapping regions; identical regions
TPP, NTPP	—	Tangential, non-tangential proper part	Proper parthood with and without boundary contact
Near	—	Boundary operator	In the closure but not the interior

Metatheory. McKinsey and Tarski (1944) proved S4 sound and complete for the topological reading of □ as interior, and complete already for any single dense-in-itself metric space, so the real line, Euclidean space of any dimension and Cantor space each determine exactly S4 and no more. Adding the universal modality gives S4u, still decidable. On the region side, Renz and Nebel (1999) showed RCC-8 constraint satisfaction NP-complete, and Renz (1999) identified maximal tractable subsets on which path consistency decides satisfiability in polynomial time. Full first-order mereotopology is undecidable: Grzegorczyk (1951) proved this for connection-based theories, and Kontchakov, Pratt-Hartmann, Wolter and Zakharyaschev showed that adding connectedness constraints over the plane already breaks decidability. Spatio-temporal combinations behave like products of modal logics, with the usual jump in complexity.

Applies to. Geographic information systems. Robot navigation and planning. Image analysis and recognition. Architecture and CAD. Natural language spatial expressions. Qualitative physics. Environmental modeling.

Limitations. The topological completeness theorem is itself the inexpressibility result: since every dense-in-itself metric space validates exactly S4, no formula of the modal language distinguishes the line from the plane from Cantor space, and dimension, connectedness, convexity and every metric property are invisible. RCC-8 has no points, so boundaries are not objects and cannot be quantified over, and the calculus expresses no distance, direction, size or shape — only the eight jointly exhaustive and pairwise disjoint connection patterns. Path consistency is sound but incomplete over the full relation set, so the polynomial algorithms decide only the tractable subsets. Every strengthening that recovers what is missing — connectedness predicates, full mereotopology, quantification over regions — crosses into undecidability.