Decidability of the satisfiability problem for Boolean set theory with the unordered Cartesian product operator

TL;DR

This paper proves the decidability of the satisfiability problem for a simplified variant of Boolean set theory with an unordered Cartesian product operator, advancing understanding of its computational properties.

Contribution

It introduces a decidability result for a simplified version of MLSC with unordered Cartesian product, suggesting potential extension to the full theory.

Findings

Decidability of the simplified MLSC variant established

The unordered Cartesian product operator does not hinder decidability

Results indicate possible extension to full MLSC

Abstract

The satisfiability problem for multilevel syllogistic extended with the Cartesian product operator (MLSC) is a long-standing open problem in computable set theory. For long, it was not excluded that such a problem were undecidable, due to its remarkable resemblance with the well-celebrated Hilbert's tenth problem, as it was deemed reasonable that union of disjoint sets and Cartesian product might somehow play the roles of integer addition and multiplication. To dispense with nonessential technical difficulties, we report here about a positive solution to the satisfiability problem for a slight simplified variant of MLSC, yet fully representative of the combinatorial complications due to the presence of the Cartesian product, in which membership is not present and the Cartesian product operator is replaced with its unordered variant. We are very confident that such decidability result can be generalized to full MLSC, though at the cost of considerable technicalities.