Decidability of general extensional mereology

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.

Recommendations

Cites work

Cited in

(13)

This page was built for publication: Decidability of general extensional mereology

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2377058)