A Monadic Second-Order Version of Tarski’s Geometry of Solids

In this paper, we are concerned with the development of a general set theory using the single axiom version of Leśniewski’s mereology. The specification of mereology, and further of Tarski’s geometry of solids will rely on the Calculus of Inductive Constructions (CIC). In the first part, we provide a specification of Leśniewski’s mereology as a model for an atomless Boolean algebra using Clay’s ideas. In the second part, we interpret Leśniewski’s mereology in monadic second-order logic using names and develop a full version of mereology referred to as CIC-based Monadic Mereology (λ-MM) allowing an expressive theory while involving only two axioms. In the third part, we propose a modeling of Tarski’s solid geometry relying on λ-MM. It is intended to serve as a basis for spatial reasoning. All parts have been proved using a translation in type theory.