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, ?xPxx, ?x?y((Pxy ∧ Pyx) → x = y) and ?x?y?z((Pxy ∧ Pyz) → 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) ?x?y(?Pyx → ?z(Pzy ∧ ?Ozx)), where Oxy means ?z(Pzx ∧ Pzy), and (Fusion) ?xα → ?z?y(Oyz ? ?x(α ∧ 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.