The Satisfiability Problem for Boolean Set Theory with a Rational Choice Correspondence

We investigate the satisfiability problem for an elementary fragment of set theory denoted BSTC, which includes a choice operator along with Boolean set operators, singleton, membership, equality, inclusion, and propositional connectives. The intended interpretation of the choice operator is as a rationalizable choice within the framework of Rational choice theory (a model of social and economic behavior), namely a contractive map defined on nonempty subsets of a universe 𝑈 that can be derived from a binary relation on 𝑈 by selecting the maximal elements of each set. We establish a small model property for BSTC under the interpretation of the choice operator as a rationalizable choice. This property enables us to develop an algorithmic solution to the satisfiability problem for BSTC, which allows us to prove that the latter falls under the complexity classes NP-hard and NEXPTIME. By investigating the implications and characteristics of rational decision-making within this fragment of set theory, our research contributes to a better understanding of the interplay between rational choice theory and set theory.