On the Decidability of Axiomatized Mereotopological Theories
Hsing-chien Tsai · Notre Dame Journal of Formal Logic · 2015
The signature of the formal language of mereotopology contains two predicates P and C, which stand for “being a part of” and “contact,” respectively. This paper will deal with the decidability issue of the mereotopological theories which can be formed by the axioms found in the literature. Three main results to be given are as follows: (1) all axiomatized mereotopological theories are separable; (2) all mereotopological theories up to ACEMT, SACEMT, or SACEMT′ are finitely inseparable; (3) all axiomatized mereotopological theories except SAX, SAX′, or SB¯X′, where X is strictly stronger than CEMT, are undecidable. Then it can also be easily seen that all axiomatized mereotopological theories proved to be undecidable here are neither essentially undecidable nor strongly undecidable but are hereditarily undecidable. Result (3) will be shown by constructing strongly undecidable mereotopological structures based on two-dimensional Euclidean space, and it will be pointed out that the same construction cannot be carried through if the language is not rich enough.