Decidability of general extensional mereology (Q2377058)

General extensional mereology (GEM) is defined in the paper as a first-order theory the language of which contains only one binary predicate symbol \(P\) interpreted as the ``is a part of'' relation. Another relation, overlapping, is defined by \(Oxy =_{\mathrm{df}} \exists z(Pzx \wedge Pzy)\). GEM has, besides the axioms of reflexivity, antisymmetry and transitivity for \(P\), an axiom of strong supplementation: \(\forall xy(\neg Pyx \to \exists z(Pzy \wedge \neg Ozx))\), and an axiom scheme of fusion: for any formula \(\alpha\) with \(z\) and \(y\) not free, \(\exists x\alpha \to \exists z \forall y(Oyz \leftrightarrow \exists x(\alpha \wedge Oyx))\). This theory is stronger than the mereological theories dealt with by the author in the earlier papers [Log. Log. Philos. 18, No. 1, 45--63 (2009; Zbl 1186.03018); ibid. 20, No. 3, 251--265 (2011; Zbl 1244.03054)]. The author proves that GEM is decidable and notices that a certain first-order approximation to the theory of complete Boolean algebras can be shown to be decidable using the same method.