A Topological Rewriting of Tarski's Mereogeometry

TL;DR

This paper formalizes Tarski's geometry within a topological framework using dependent type theory and Coq, enhancing qualitative spatial models with true Euclidean and topological structures.

Contribution

It extends lambda-MM to fully formalize Tarski's geometry, deriving a topological space from mereology and embedding Tarski's primitives, thus increasing expressiveness.

Findings

Proves that mereological classes correspond to regular open sets.

Shows Tarski's geometry forms a subspace within the constructed topology.

Reduces Tarski's axioms and extends the theory with Hausdorff property.

Abstract

Qualitative spatial models based on Goodman-style mereology and pseudo-topology often pose problems for advanced geometric reasoning, as they lack true Euclidean geometry and fully developed topological spaces. We address this issue by extending an existing formalization grounded in a dependent type theory using the Coq proof assistant, together with a Whitehead-like point-free interpretation of Tarski's geometry. More precisely, we build on a library called lambda-MM to formalize Tarski's geometry of solids by investigating an algebraic formulation of topological relations on top of the mereological framework. Since Tarski's work is rooted in Lesniewski's mereology, and given that lambda-MM currently provides only a partial implementation of Tarski's geometry, the first part of the paper completes this framework by proving that mereological classes correspond to regular open sets. This yields a topology of individual names that can be extended with Tarski's geometric primitives. Unlike classical approaches in qualitative logical theories, we adopt a solution that derives a full topological space from mereology together with a geometric subspace, thereby increasing the expressiveness of the theory. In the second part, we show that Tarski's geometry forms a subspace of this topology in which regions correspond to restricted classes. We also prove three of Tarski's original postulates, reducing his axiomatic system, and extend the theory with the T2 (Hausdorff) property and additional definitions.