A Topological Rewriting of Tarski's Mereogeometry

This paper presents a Coq-based formalization that extends Tarski's mereogeometry into a full topological space by proving the correspondence between mereological classes and regular open sets, thereby reducing Tarski's axiomatic system and enhancing its expressiveness for Euclidean geometric reasoning.

The Gist

Imagine you are trying to build a map of the world, but you aren't allowed to use dots (points) or lines. You can only use shapes and blobs. This is the challenge faced by computer scientists who want machines to understand space, like a robot navigating a room or a GPS understanding a city.

For a long time, the tools used to do this were a bit like a child's drawing: they could say "this blob is inside that blob," but they struggled with the messy details of real-world geometry, like smooth curves, boundaries, or the fact that two things can be close without touching.

This paper, "A Topological Rewriting of Tarski's Mereogeometry," by Patrick Barlatier and Richard Dapoigny, proposes a new, much more sophisticated way to build these maps. They take an old, dusty blueprint (Tarski's geometry) and rebuild it using modern, high-tech tools (a programming language called Coq) to make it mathematically perfect.

Here is the breakdown of their idea using simple analogies:

1. The Problem: The "Blob" vs. The "Point"

Traditional ways of describing space often rely on Mereology (the study of parts and wholes). Think of it like a game of Lego.

• The Old Way: You have a big Lego structure. You can say, "This brick is part of that wall." But if you try to describe a smooth curve or a precise boundary, the Lego blocks get in the way. The math gets "shaky," and the computer can't prove things are true with 100% certainty.
• The Goal: The authors want to create a system where "blobs" (regions) act exactly like the smooth, perfect shapes we see in Euclidean geometry (like circles and spheres), but without ever needing to define a single "point."

2. The Solution: The "Magic Clay" (Regular Open Sets)

The authors use a concept called Regular Open Sets. Imagine you have a bucket of magic clay.

• If you squish the clay into a shape, it holds that shape perfectly.
• If you poke a hole in the middle, the clay doesn't just leave a jagged edge; it smooths itself out.
• In their system, every "thing" (a region) is a piece of this magic clay that has been smoothed out. There are no jagged edges or missing bits.

They prove that their system of "Lego blobs" is actually mathematically identical to this "smooth clay." This is a huge deal because it means they can use the strict rules of geometry to reason about their blobs.

3. Re-inventing the "Point"

In normal geometry, a point is a dot with no size. In this paper, the authors say: "Points are too abstract. Let's build them out of the blobs instead."

• The Analogy: Imagine a Russian Nesting Doll.
  • A "Point" isn't a single dot. It is a set of concentric balls (like the nesting dolls) getting smaller and smaller, all centered on the same spot.
  • If you have a ball inside a ball inside a ball, all sharing the same center, that whole stack is a point.
  • This allows them to define a "point" using only the "blobs" (balls) they already have. It's like defining a "person" not by their name, but by the specific family they belong to.

4. The "House" and the "Fence" (Topology)

Once they have their smooth blobs and their "nesting doll" points, they build a Topology (a mathematical map of space).

• The Interior: The inside of a room.
• The Boundary: The walls and the fence.
• The Exterior: The outside world.

The authors prove that their system handles these boundaries perfectly. They show that if you have two different points (two different stacks of nesting dolls), you can always draw a "fence" (a boundary) around them so they don't touch. In math-speak, this is called the Hausdorff property (or T2), which basically means "everything is distinct and separated."

5. Why Use a Robot Lawyer? (The Coq Proof)

The most impressive part of this paper is how they did it. They didn't just write it on a chalkboard; they fed it into Coq, a computer program that acts like a super-strict robot lawyer.

• The robot lawyer checks every single step of their logic.
• If there is even one tiny gap in the argument, the robot says, "No, that doesn't prove anything."
• Because the robot accepted their proof, we know for a fact that their new system is 100% logically sound. There are no hidden errors.

6. Why Should You Care?

This isn't just abstract math; it has real-world superpowers:

• Better Robots: Self-driving cars and drones need to understand space perfectly to avoid crashing. This system gives them a "perfect map" of the world.
• Smart AI: The authors suggest this could help train Large Language Models (like the one you are talking to now) to understand space better. Right now, AI is good at words but bad at geometry. This provides a "skeleton" of logic that AI can learn from.
• Architecture & GIS: It helps architects and city planners verify that their designs are physically possible and logically consistent.

The Big Picture

Think of this paper as renovating an old house.

• The old house (traditional spatial logic) was built with shaky wood (imprecise logic) and had rooms that didn't quite fit together.
• The authors took the blueprints (Tarski's old ideas), reinforced the foundation with steel beams (Type Theory and Coq), and added a new wing that connects the "part" (blobs) to the "whole" (smooth geometry).
• The result is a fortress of logic that is strong enough to hold up the most complex spatial reasoning tasks, from guiding a robot through a maze to helping AI understand the physical world.

Technical Summary

Here is a detailed technical summary of the paper "A Topological Rewriting of Tarski's Mereogeometry" by Barlatier and Dapoigny.

1. Problem Statement

The paper addresses significant limitations in existing Qualitative Spatial Reasoning (QSR) models, particularly those based on Goodman-style mereology and pseudo-topological frameworks (e.g., RCC8, contact algebras). The authors identify four primary challenges:

• Lack of True Geometry: Existing models often lack a fully developed Euclidean geometric foundation, relying instead on shallow representations of part-whole relations.
• Boundary Ambiguity: There is no formal specification of topological boundaries (i.e., whether a boundary is a spatial object or an abstract entity).
• Decidability Issues: The decidability of many resulting logical systems remains unresolved, hindering tractable reasoning.
• Expressiveness: Direct mappings of part-of relations into first-order logic often result in insufficient reasoning mechanisms and poor expressiveness.

The authors aim to bridge the gap between mereology, topology, and geometry by creating a unified, formally verified theory that supports advanced geometric reasoning without relying on primitive points.

2. Methodology

The research leverages the Coq theorem prover and its underlying dependent type theory to construct a formal system. The methodology proceeds in three main stages:

A. Foundation: The $\lambda$-MM Library

The work builds upon the existing open-source $\lambda$-MM library, which implements Leśniewski's Mereology and Ontology within a syntactic, type-theoretic framework.

• Nominalist Approach: Instead of set-theoretic membership, the system uses a syntactic relation ($\eta$) where names refer to individuals or aggregates.
• Inductive Types: "Names" are objects of an inductive type $N$, ensuring existence and identity are determined syntactically rather than semantically.
• Boolean Mereology: The library models mereological classes as a quasi-Boolean algebra (without a bottom element), where the "part-of" relation ($pt$) serves as the ordering principle.

B. Topological Extension (Mereology as Topology)

The authors extend $\lambda$-MM to define a topological space where mereological classes correspond to regular open sets.

• Operators: They introduce meet (intersection) and join (union) operators to the Boolean model.
• Interior Operator: Defined such that the interior of a plural name (a class) is the individual name representing that class.
• Kuratowski Axioms: The system is proven to satisfy Kuratowski's interior axioms (preservation of total space, intensiveness, idempotence, and preservation of binary intersections), establishing $\langle N, T_{MM} \rangle$ as a valid topology.
• Regularity: By defining the closure as the complement of the interior of the complement, they prove that mereological classes correspond to regular open sets (sets equal to the interior of their closure).

C. Integration of Tarski's Geometry

The authors integrate Tarski's Geometry of Solids (based on balls/spheres) into this topological framework.

• Point-Free Construction: Points are not primitives but are defined as filters of concentric balls (second-order objects).
• Saturated Interior Points: To construct a robust topology of regions, they redefine Tarski's "interior point" as a saturated interior point (a point whose associated concentric balls are entirely contained within the region).
• Subspace Topology: They define a subspace topology ($T_{MG}$) where the basis consists of sums of balls, and open sets are regions (m-classes of balls).

3. Key Contributions

1. Formal Equivalence of Mereology and Regular Open Sets:
   The paper proves that the Boolean mereological model implemented in $\lambda$-MM is isomorphic to a structure of regular open sets. This allows mereological operations (part-of, sum, product) to faithfully represent topological relations (inclusion, union, intersection).

2. Topological Rewriting of Tarski's Axioms:
   The authors successfully reconstruct Tarski's axiomatic system for solids using purely topological and mereological primitives within Coq.

   • Postulate 2 & 3: Proved that the class of interior points of a region forms a regular open set (a mereological class).
   • Postulate 4: Proved that the inclusion of interior point sets implies the part-of relation between regions.

3. Hausdorff (T2) Property and Convexity:

   • The constructed geometric space ($G_{space}$) is proven to satisfy the Hausdorff (T2) property, ensuring distinct points have disjoint neighborhoods.
   • The authors introduce a definition for convex regions within this framework, ensuring that the line segment between any two interior points lies entirely within the region.

4. Unified Type-Theoretic Framework:
   The work provides a single, constructive framework that unifies:

   • Mereology: Part-whole reasoning.
   • Topology: Open sets, boundaries, and closure.
   • Geometry: Euclidean concepts (betweenness, concentricity, convexity) derived without primitive points.

4. Results

• Verification: All definitions and theorems (including the isomorphism to regular open sets, Kuratowski axioms, and Tarski's postulates) have been formally verified in Coq.
• Reduction of Axioms: The system reduces Tarski's axiomatic system by deriving key properties from the underlying mereological and topological definitions.
• Boundary Definition: The paper provides a rigorous definition of the boundary as a set of points (concentric spheres) that belong neither to the region nor its complement, resolving the "boundary problem" common in QSR.
• Homeomorphism Conjecture: The authors conjecture a homeomorphism between their constructed structure $\langle R, T_{GM} \rangle$ and standard Euclidean space $\langle \mathbb{R}^3, T_{\mathbb{R}^3} \rangle$, suggesting topological equivalence.

5. Significance and Applications

• High-Assurance Systems: The use of Coq ensures certified proofs and ontological robustness, making the system suitable for safety-critical applications such as autonomous navigation (collision avoidance, route planning), architectural validation, and Geographic Information Systems (GIS).
• Neuro-Symbolic AI: The authors propose that this formally structured library can serve as a high-quality training resource for Large Language Models (LLMs). By providing symbolic scaffolds for spatial reasoning, it aims to bridge the gap between generative AI and formal logical reasoning, potentially improving the spatial capabilities of AI systems.
• Theoretical Advancement: It offers a "point-free" alternative to classical set-theoretic geometries, demonstrating that complex geometric properties can be derived from mereological and topological primitives alone, enhancing the expressiveness of qualitative spatial theories.

In summary, the paper presents a rigorous, machine-verified reconstruction of Tarski's geometry that overcomes the expressiveness and decidability limitations of traditional QSR models by grounding them in a type-theoretic mereotopology of regular open sets.