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

Patrick Barlatier (1) , Richard Dapoigny (1)

1 LISTIC - Laboratoire d'Informatique, Systèmes, Traitement de l'Information et de la Connaissance

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.

Mots clés: mereology; monadic second-order logic; geometry of solids; calculus of inductive constructions; theorem prover; type theory; mereology monadic second-order logic geometry of solids calculus of inductive constructions theorem prover type theory; mereology

Domaines: Intelligence artificielle [cs.AI]; Mathématiques [math]

Patrick Barlatier, Richard Dapoigny. A Monadic Second-Order Version of Tarski’s Geometry of Solids. Logic and Logical Philosophy, 2023, 33 (1), pp.55-99. ⟨10.12775/LLP.2023.019⟩. ⟨hal-04470647⟩