Decidability of General Extensional Mereology

摘要

The signature of the formal language of mereology contains only one binary predicate P which stands for the relation “being a part of”. Traditionally, P must be a partial ordering, that is, ({forall{x}Pxx, forall{x}forall{y}((Pxyland Pyx)to x=y)}) and ({forall{x}forall{y}forall{z}((Pxyland Pyz)to Pxz))}) are three basic mereological axioms. The best-known mereological theory is “general extensional mereology”, which is axiomatized by the three basic axioms plus the following axiom and axiom schema: (Strong Supplementation) ({forall{x}forall{y}(neg Pyxto exists z(Pzyland neg Ozx))}), where Oxy means ({exists z(Pzxland Pzy)}), and (Fusion) ({exists xalpha to exists zforall y(Oyzleftrightarrow exists x(alpha land Oyx))}), for any formula α where z and y do not occur free. In this paper, I will show that general extensional mereology is decidable, and will also point out that the decidability of the first-order approximation of the theory of complete Boolean algebras can be shown in the same way.