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.