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.
defined by ≾ if there is a menu ⊆ such that ∈ ().1
Classically, a choice is considered rationalizable if the observed behavior can be univocally recovered by maximizing this relation of revealed preference: that is, () = max(, ≾) for any feasible menu .2 This encoding of the concept of rationality yields a notable simplification of the observed behavior: in fact, rationalizability is equivalent to the possibility to represent a map from pow( ) into pow( ), which requires (| | · 2||) space, by a subset of × , which requires (| |2) space (here pow( ) denotes the powerset of ).
Since Samuelson’s groundbreaking paper, a significant amount of attention has been devoted
to exploring various concepts of rationality within the framework of choice theory. The
literature includes several influential contributions such as the classical works by authors like
Houthakker [
It is well-known that, under appropriate assumptions on the domain, a choice can be
considered rationalizable if and only if it satisfies the two standard consistency axioms ( ) and ( )
(refer to Sen [
In this paper, we focus on the satisfiability problem for unquantified formulae in an elementary fragment of set theory denoted as BSTC. This fragment includes essential elements such as the choice function symbol c, Boolean set operators like union ∪, intersection ∩, set diference ∖, the singleton operator { }, predicates for membership ∈, equality =, and inclusion ⊆ , as well as propositional connectives such as conjunction ∧, disjunction ∨, negation ¬, implication =⇒ , etc.
In a previous work [11], we examined cases where the interpretation of the choice operator c was subject to combinations of consistency axioms, namely ( ) and ( ), whose conjunction is equivalent to the WARP property. In this paper, we focus on a diferent scenario where the choice operator c is interpreted as a rational choice. Specifically, we establish our decidability result by demonstrating that BSTC under rationalizability exhibits a small model property. The current approach contrasts with that used in [11], which relied on reduction techniques and various lifting results.
2In this case, “levels of rationality” are associated to the properties satisfied by the relation of reveled preference,
e.g., transitivity: see [
By considering the interpretation of c as a rational choice, we aim to explore the implications and characteristics of rational decision-making within the framework of BSTC.
By depriving the BSTC-language of the choice function symbol c, we obtain the fragment 2LSS (here denoted BSTC− ) whose decidability was known since the birth of Computable Set Theory in the late 70’s. The reader can find extensive information on Computable Set Theory in the monographs [12, 13, 14, 15].
The paper is organized as follows. Section 2 is devoted to the basis of choice theory, while the syntax and semantics of the BSTC-language are presented in Section 3. Then, in Section 4, we prove that the satisfiability problem for BSTC under rationalizability is decidable and belongs to the complexity classes NP-hard and NEXPTIME. Finally, in Section 5, we draw our conclusions and hint at future developments.
Hereafter, we fix a nonempty set (the “universe"). Let pow( ) be the family of all subsets of , and pow+( ) the subfamily pow( ) ∖ {∅}. The next definition collects some basic notions in choice theory.
map : Ω → pow+( ) that is never empty-valued, namely such that ∅ ̸= () ⊆ , for every ∈ Ω.
In this paper, we denote a choice correspondence on by : Ω ⇒ , and simply refer to it as a choice. The set Ω is the choice domain of , sets in Ω are (feasible) menus, and elements of a menu are items. Further, we say that : Ω ⇒ is total if Ω = pow+( ), and partial otherwise.
Given a choice : Ω ⇒ , the choice set () of a menu collects the elements of that are deemed selectable by an economic agent. Thus, in case () contains more than one element, the selection of a single element of is deferred to a later time, usually with a diferent procedure (according to additional information or “subjective randomization", e.g., flipping a coin).
The next definition recalls the classical notion of rationalizable choices.
Definition 2. A choice : Ω ⇒ is rationalizable if there exists a binary relation ≾ over such that, for all menus ∈ Ω, () is the set
max(, ≾) := {︀ ∈ : (∀ ∈ )( ≾ =⇒ ≾ )}︀ of the strictly ≾-maximal members of .
Rationalizable choices can also be characterized in terms of asymmetric relations, namely relations that contain no pair of elements that are mutually related to each other. Lemma 1. A choice is rationalizable if and only if it is induced by an asymmetric relation. In fact, a rationalizable total choice is induced by exactly one asymmetric relation.
asymmetric part of ≾, thus: be the ≺ ⇐⇒ ≾ ∧ ̸≾ .
Notice that max(, ≾) = max(, ≺ ) for all subset ⊆ , thus ≺ rationalizes . On the counter-side plainly if is induced by an asymmetric relation then is rationalizable.
By contradiction, let us assume that a total choice : pow+( ) ⇒ is rationalized by two distinct asymmetric relations ≺ and ≺ ′ over . Thus, there exist , ∈ such that ≺ ⇐⇒ ̸≺ ′ .
∈/ max({, }, ≺ ) and ∈ max({, }, ≺ ′), which contradicts that ≺ and ≺ ′ rationalize the same choice.
For the rest of the paper, we will rely on the characterization of rationalizable choices in terms of asymmetric relations.
The rationalizability of choice is traditionally connected to the satisfaction of suitable axioms
of choice consistency. These axioms codify rules of coherent behavior of an economic agent.
Among the several axioms that are considered in the literature, the following are relevant to
our analysis (a universal quantification on all the involved menus is implicit):
axiom ( ) [standard contraction]: ⊆ =⇒ ∩ () ⊆ ()
axiom ( ) [standard expansion]: () ∩ () ⊆ ( ∪ )
axiom ( ) [symmetric expansion]: (︀ ⊆ ∧ () ∩ () ̸= ∅)︀
=⇒ () ⊆ ()
Axiom ( ) was studied by Chernof [10], whereas axioms ( ) and ( ) are due to Sen [
Upon reformulating these properties in terms of items, their semantics becomes clear. Chernof’s axiom ( ) states that any item selected from a menu is still selected from any submenu ⊆ containing it. Sen’s axiom ( ) says that any item selected from two menus and is also selected from the menu ∪ (if feasible). The expansion axiom ( ) can be equivalently written as follows: if ⊆ , , ∈ () and ∈ (), then ∈ (). In this form, ( ) says that if two items are selected from a menu , then they are simultaneously either selected or rejected in any larger menu .
Razionalizability is hereditary, as stated in the following lemma.
Lemma 2. Let Ω ⊆ pow+( ). If a choice : Ω ⇒ restrictions |Ω′ , for ∅ ̸= Ω′ ⊆ Ω.
Proof. Trivially any relation ≺ that rationalizes is such that max(, ≺ ) = () = |Ω′ (), for all ∈ Ω′, thus ≺ rationalizes |Ω′ . is rationalizable, then so is any of its
Another useful preliminary result is that a rationalizable partial choice correspondence can be lifted to a rationalizable total choice if and only if each asymmetric relation ≺ that rationalizes it is devoid of infinite ascending ≺ -sequences , namely there is no infinite sequence 0, 1, 2, . . . of items such that 0 ≺ 1 ≺ 2 ≺ · · · .
This is proved in the following lemma.
Lemma 3 (Lifting rationalizability). A (rationalizable) partial choice can be extended to a rationalizable total choice if and only if is rationalizable by an asymmetric relation devoid of infinite ascending sequences.
Proof. Let : Ω ⇒ be a partial choice correspondence, with Ω ⊆ pow+( ). Let us assume that can be extended to a rationalizable total choice ′ : pow+( ) ⇒ , and let ≺ ′ be the asymmetric relation over that rationalizes ′, namely such that ′() = max(, ≺ ′) for every ∈ pow+( ). We claim that ≺ ′ is devoid of infinite ascending sequences. Indeed, if this were not the case, letting
0 ≺ ′ 1 ≺ ′ 2 ≺ ′ · · · be an infinite ascending chain in , the related menu := {0, 1, 2, . . .} would have no ≺ ′-maximal item and therefore ′() = max(, ≺ ′) = ∅, which is impossible, as ′ is a total choice. By Lemma 2, the choice correspondence is rationalized by ≺ ′ as well.
Conversely, let us assume that our partial choice correspondence can be rationalized by an asymmetric relation ≺ over that is devoid of infinite ascending sequance. We claim that for every ∈ pow+( ) (not necessarily in Ω), the menu must have some ≺ -maximal item, namely max(, ≺ ) ̸= ∅. Indeed, if not, then for every ∈ , there would be another item ′ ∈ such that ≺ ′. Consequently, any finite ≺ -sequence in of length could be extended to a ≺ -sequence of length + 1, for every ≥ 1. Since is nonempty, this would imply the existence of infinite ascending ≺ -sequences in ⊆ , leading to a contradiction.
We specify the syntax and semantics of the Boolean set-theoretic language extended with a choice correspondence, denoted by BSTC, of which we will study the satisfiability problem, under rationalizability. 3.1. Syntax of BSTC Following [11], the language BSTC involves • two disjoint denumerable collections 0 and 1 of individual variables (denoted by small ifnal letters, such as ) and set variables (denoted by capital final letters, such as ), respectively; • the constant ∅ (empty set); • operation symbols: ∪ , ∩ , ∖ , { }, c( ) (choice map); • predicate symbols: = , ⊆
, ∈ .
Set terms of BSTC are recursively defined as follows: • set variables and the constant ∅ are set terms; • {} is a set term, for every individual variable ; • if , 1, 2 are set terms, then 1 ∪ 2, 1 ∩ 2, 1 ∖ 2, c( ) are set terms. The atomic formulae (or atoms) of BSTC have one of the following forms = , ∈ , 1 = 2, 1 ⊆ 2, where 1, 2 are set terms.
Finally, BSTC-formulae are propositional combinations of BSTC-atoms by means of the usual logical connectives ∧, ∨, ¬, =⇒ , ⇐⇒ .
We regard {1, . . . , } as a shorthand for the set term {1} ∪ . . . ∪ {}.
Choice terms are BSTC-terms of type c( ), whereas choice-free terms are BSTC-terms which do not involve the choice map c (at any level of nesting). We refer to BSTC-formulae containing only choice-free terms as BSTC− -formulae. With slight variations in syntax, BSTC− -formulae are essentially equivalent to 2LSS-formulae, which is known to have a decidable satisfiability problem (refer, for example, to [13, Exercise 10.5]).
rences (individual and set variables, set operators, propositional connectives) used to represent . 3.2. Semantics of BSTC under rationalizability A set assignment is a pair ℳ = (, ), where is any nonempty collection of objects, called the domain or universe of ℳ, and is an interpretation over the variables and the choice map of BSTC such that • ∈ , for each individual variable ∈ 0; • ∅ := ∅ and ⊆ , for each set variable ∈ 1; • c is a rationalizable total choice over .
Then, we extend over the terms by putting recursively: • (1 ⊗ 2) := 1 ⊗ 2 , where ⊗ ∈ {∪ , ∩, ∖}; • {} := { }; • (c( )) := c ( ).
The size of a set assignment is the cardinality of its domain.
Satisfiability under rationalizability ( Rtl-satisfiability, for short) of any ℳ (written ℳ |=Rtl ) is defined as follows: BSTC-formula by |=Rtl 1 ⋆ 2 |=Rtl ∈ |=Rtl 1 = 2 if if if 1 ⋆ 2 , ∈ , 1 = 2 , for all BSTC-atoms 1 ⋆ 2, ∈ , and = , where ⋆ ∈ {=, ⊆} . Finally, the logical connectives are interpreted according to their classical meaning.
For a BSTC-formula , if ℳ |=Rtl (i.e., ℳ Rtl-satisfies ), then ℳ is an Rtl-model for . A BSTC-formula is Rtl-satisfiable if it has an Rtl-model. Two BSTC-formulae and are Rtl-equivalent if they share exactly the same Rtl-models; they are Rtl-equisatisfiable if one is Rtl-satisfiable if and only if so is the other (possibly by diferent models).
The Rtl-satisfiability problem (or Rtl-decision problem) for BSTC asks for an efective procedure (or decision procedure) to establish whether any given BSTC-formula is Rtl-satisfiable or not. 3
The satisfiability problem for BSTC has been addressed also under other semantics (see [11]): specifically, the ( )-semantics, the ( )-semantics, the WARP-semantics, and the unrestricted semantics (whose satisfiability relations are denoted by |= , |= , |=WARP, and |=, respectively). These difer from the Rtl-semantics in that the interpreted choice map c is required to satisfy axiom ( ) in the first case, axiom ( ) in the second case, axioms ( ) and ( ) conjunctively (namely WARP) in the third case, and no particular consistency axiom in the latter case.
In this section, we demonstrate that the satisfiability problem for the theory BSTC under rationalizability is decidable. We will prove this result by establishing a small model property for BSTC, which allows one to test the satisfiability of any BSTC-formula by verifying if it is satisfied by some set assignment whose ‘size’ is bounded by an exponential function of the size of . Since such bounded sets assignment can be generated efectively, their number is bounded, and it can be efectively checked whether any of them actually satisfies a given BSTC-formula , the decidability of the Rtl-satisfiability problem for BSTC follows.
We recall that the decidability results presented in [11] for the four previously mentioned semantics are based instead on a reduction technique. Such technique involves enriching a given BSTC-formula that needs to be tested for satisfiability by adding appropriate clauses, resulting in an extended BSTC-formula 1. Then, by systematically replacing the choice terms in 1 with newly introduced set variables, one obtains a (choice-free) BSTC− -formula 1 that is equisatisfiable with . As a consequence, the decidability of the satisfiability problems for BSTC under the various four semantics follows from the known decidability of the satisfiability problem for BSTC− (see [13, Exercise 10.5]).
Without compromising the expressivity of BSTC, we can limit ourselves to BSTC-formulae that consist solely of equality atoms 1 = 2, where 1 and 2 are set terms constructed using only the set diference operator ‘ ∖’ and the singleton operator { }. Indeed, atoms of the form = , ∈ , and 1 ⊆ 2 can be just replaced by the equivalent atoms {} = {}, {} ⊆ , and 1 ∪ 2 = 2, respectively. Additionally, terms of the form 1 ∩ 2 can be replaced by the equivalent term 1 ∖ (1 ∖ 2). Finally, every term of the form 1 ∪ 2 can be eliminated from a given BSTC-formula by replacing it by a newly introduced set variable 1∪2 and by adding to the atoms 1∪2 ∖ 1 = 2 ∖ 1 and 1 ∖ 1∪2 = ∅ as conjuncts, since, as 3Since in this paper we are dealing we just one semantics for choice terms, we may occasionally omit the use of the shorthand Rtl when referring to expressions such as model, satisfiability, and so on. observed in [16], it holds that
|= 1∪2 = 1 ∪ 2 ⇐⇒ (1∪2 ∖ 1 = 2 ∖ 1 ∧ 1 ∖ 1∪2 = ∅).
Likewise, the set constant ∅ can be eliminated from a BSTC-formula by replacing each of its occurrences by a fresh set variable ∅ characterized by the atom ∅ = ∅ ∖ ∅.
equisatisfiable formula, rather than an equivalent formula as in the other cases considered, due to the introduction of new variables. However, this does not pose any problem for our satisfiability objectives. Note also that the size of the resulting formula is linear in the size of the initial formula.
Thus, let be an Rtl-satisfiable propositional combination of equality atoms of the form 1 = 2, where 1 and 2 are BSTC-terms, and let ℳ = (, ) be a set model for under rationalizability, namely such that ℳ |=Rtl .
denoted as ℳ, with a universe ⊆ of size (2| |). This establishes a small model property for BSTC under rationalization, leading to the decidability of the Rtl-satisfiability problem for BSTC, as previously argued.
To this purpose, we will apply the following straightforward fact.
Lemma 4. Given a BSTC-formula and two set assignments ℳ and ℳ over the variables of that Rtl-satisfy the same equality atoms in , ℳ Rtl-satisfies if and only if ℳ Rtl-satisfies .
occurring in , respectively, and let be the collection of the set terms occurring in . Plainly, | | = (| |). We intend to show that the formula admits an Rtl-model over a universe of size (2| |).
Let := { : ∈ } and let ℛ denote the Euler-Venn partition of , namely the partition
ℛ := {︀ ⋂︀ ∖ ⋃︀( ∖ ) : ∅ ≠ ⊆ }︀ ∖ {∅} of ⋃︀ , where ⋂︀ is the intersection of all the members of . Equivalently, the partition ℛ can be defined as the collection of the ⊆ -maximal nonempty subsets of ⋃︀ such that, for every term ∈ , either ⊆ or ∩ = ∅.
Without loss of generality, we may assume that = ⋃︀ , since otherwise we could replace ℳ by the set assignment ℳ′ = ( ′, ′) in our analysis, where ′ = ⋃︀ , ′ = for all ∈ V0, ′ = for all ∈ V1, and c′ = c |′ . Indeed, by Lemma 2, c′ is plainly a rationalizable total choice over ′, and so ℳ′ |=Rtl .
ℳ can be constructed, involves selecting an item from each block in ℛ . It is natural then to define the interpretation over the variables V0 ∪ V1 occurring in by setting := for each ∈ V0 and := ∩ for each ∈ V1. Notably, as {} ∈ ℛ for every ∈ V0, we then have ∈ , enabling us to define as .
Under the hypothesis that is choice-free, meaning that it does not contain any choice term, we can readily prove that the set assignment ℳ = ( , ) just defined is indeed a model for . In view of Lemma 4, it is enough to prove that, for every atom 1 = 2 in , we have
⇐⇒ 1 = 2 .
In its turn, to prove the latter biconditional it sufices to show that = ∩ holds for all set terms occurring in , as proved in the following lemma.
Lemma 5. If = ∩ holds for all set terms occurring in a BSTC-formula (not necessarily choice-free), then the biconditional holds for all set terms 1 and 2 occurring in .
Proof. Let 1 and 2 be any two terms in . The forward implication in (1) is straightforward, since if 1 = 2 holds then
1 = 1 ∩ = 2 ∩ = 2 .
As for the backward implication, let us assume, for the sake of contradiction, that 1 ∩ = 2 ∩ , but 1 ̸= 2 . Since both 1 and 2 are unions of blocks in ℛ , there must exist a block ∈ ℛ such that ∩ 1 ̸= ∅
⇐⇒ ∩ 2 = ∅.
For definiteness, let us assume that ∩ 1 ̸= ∅ and ∩ 2 = ∅. Hence, we have ⊆ 1 , and therefore:
∅ ̸= ∩ 1 ∩ = ∩ 2 ∩ = ∅, which is a contradiction. Thus, even the backward implication in (1) is true, and so the biconditional (1) holds, provided that = ∩ is true for all set terms occurring in .
Thus, we are left with establishing the truth of the condition = ∩ , for all set terms occurring in .
The case in which is choice-free can be handled quite straightforwardly by the following lemma.
Lemma 6. If is choice-free, then the condition = ∩ holds for all set terms occurring in .
Proof. We proceed by structural induction on .
to obtain:
= = ∩ = ∩ .
For the inductive step, we consider the following cases: 1. if has the form {}, where ∈ V0, by recalling that = by definition, then we have: = {} = { } = { } = {} = ; 2. if has the form 1 ∖ 2, we have: = (1 ∖ 2) = 1 ∖ 2 = (1 ∩ ) ∖ (2 ∩ )
= (1 ∖ 2 ) ∩ = (1 ∖ 2) ∩ = ∩ , where we used the inductive hypotheses = ∩ , for = 1, 2, and the identity The latter is a direct consequence of the fact that for any set :
(1 ∩ ) ∖ (2 ∩ ) = (1 ∖ 2 ) ∩ . ∈ (1 ∩ ) ∖ (2 ∩ ) ⇐⇒ ∈ 1 ∩ ∧ ∈/ 2 ∩ ⇐⇒ ∈ 1 ∧ ∈ ∧ ∈/ 2 ⇐⇒ ∈ 1 ∖ 2 ∧ ∈ ⇐⇒ ∈ (1 ∖ 2 ) ∩ .
Remark 1. We observe that Lemmas 4, 5, and 6 enable us to rediscover the decidability of the satisfiability problem for BSTC− . It is noteworthy that, in the case of BSTC− -formulae, one can significantly reduce the number of items needed to construct the universe ⊆ . As demonstrated in [17, 18], the construction of in this case only requires selecting one item from each block in a carefully chosen set of at most − 1 blocks within ℛ , where represents the number of distinct terms occurring in . This observation is at the base of the NP-completeness of the decision problem for BSTC− .
If we drop from the statement of Lemma 6 the hypothesis that the formula is choice-free, another case must be taken into account in its inductive proof: the case in which the term is of the form c(1). This would require us to prove, under the inductive hypothesis 1 = 1 ∩ , that (c(1)) = (c(1)) ∩ , namely: c (1 ∩ ) = c (1 ) ∩ . (2) Hence, special care must be taken in the definition of c in order that the identity (2) holds. The following example shows that we cannot simply define c as the restriction to pow+( ) of the choice c .
Example 1. Let = {, , , } and consider the asymmetric relation ≺ over , where ≺ and ≺ . We define the interpretation over {, } as = {, } and = {, }. Furthermore, let c be the choice function over the universe , rationalized by ≺ .
For the restricted interpretation, let = {, }. We define the interpretation over the universe as = ∩ = {} and = ∩ = {}. Assume that we define the choice function c simply as c = c |pow+(), and consider the choice term equal to c( ∪ ). Then we have: = (c( ∪ )) = c ( ∪ ) = c ({, , , }) = {, } = (c( ∪ )) = c ( ∪ ) = c ({, }) = {, }.
Comparing the results, we find that = {, }, which is not equal to the intersection of with , i.e., {}. ▷
Note that since 1 and c(1) are terms in , then 1 and (c(1)) are unions of blocks in the Euler-Venn partition ℛ . By defining Γ1 as the set of the blocks of ℛ contained in 1 , and similarly for Γc(1), namely Γ1 := { ∈ ℛ : ⊆ 1 } and Γc(1) := { ∈ ℛ : ⊆ (c(1)) }, (3) we have ⋃︀ Γ1 = 1 and ⋃︀ Γc(1) = (c(1)) = c (1 ). Therefore, we have c (⋃︀ Γ1 ) = ⋃︀ Γc(1). It would therefore be suficient that there existed a rationalizable choice over the universe such that (︀ (⋃︀ Γ) ∩ )︀ = ⋃︀ Γ′ ∩ held, for all nonempty subsets Γ, Γ′ of ℛ satisfying an identity of the form c (⋃︀ Γ) = ⋃︀ Γ′.
This is guaranteed by the following technical lemma, whose rather intricate and lengthy proof is omitted due to space limits.
Lemma 7. Let : pow+( ) ⇒ be a rationalizable total choice correspondence and Σ := {1, 2, . . . , } be an -partition of , for some ≥ 1. Then for every subset ⋆ = {1⋆, ⋆2, . . . , ⋆} of with elements such that ⋆ ∈ for = 1, 2, . . . , , there exists a rationalizable total choice ⋆ over ⋆ such that the following implication holds for all nonempty subsets Γ, Γ′ of Σ: (⋃︀ Γ) = ⋃︀ Γ′ =⇒ ⋆(︀ (⋃︀ Γ) ∩ ⋆)︀ = (⋃︀ Γ′) ∩ ⋆.
Thus, for the rest of the section, we will assume that c is any choice over such that the implication
c (⋃︀ Γ) = ⋃︀ Γ′ =⇒ c (︀ (⋃︀ Γ) ∩ )︀ = (⋃︀ Γ′) ∩ holds for all ∅ ≠ Γ, Γ′ ⊆ ℛ , whose existence is guaranteed by Lemma 7, so that can prove the identity (2) concerning terms of the form c(1).
The preceding discussion allows us to state the following strengthening of Lemma 6. Lemma 8. Assuming that c (1 ∩ ) = c (1 ) ∩ for every choice term c(1) in , then the condition = ∩ holds for all set terms in .
We claim that ℳ = ( , ) is an Rtl-model for our BSTC-formula .
In view of Lemma 4, it sufices to show that, for each atomic subformula 1 = 2 occurring in , we have ℳ |=Rtl 1 = 2 ⇐⇒ ℳ |=Rtl 1 = 2.
Since ℳ |=Rtl 1 = 2 ⇐⇒ 1 = 2 (by definition) (4) (5) ⇐⇒ ⇐⇒ for every atomic equality 1 = 2 in , from Lemma 4 and the hypothesis ℳ |=Rtl it follows that ℳ is an Rtl-model for , as claimed. In addition, we have that the universe of ℳ has size |ℛ | < 2| | ≤ 2| |, where | | is the size of .
Summing up, we have the following result: (by definition), Theorem 1 (Small model property). A BSTC-formula is Rtl-satisfiable if and only if it admits an Rtl-model over a universe of size (2| |).
The preceding theorem yields the following trivial decision procedure for the Rtl-satisfiability problem of BSTC.
procedure BSTC-Rtl-test( ); 1. let := | | and let be any universe of size 2; 2. for each set assignment ℳ = (, ) under rationalizability do 3. if ℳ |=Rtl then 4. return “ is Rtl-satisfiable by ℳ = (, )”; 5. return “ is not Rtl-satisfiable”; end procedure;
Regarding the complexity of the procedure BSTC-Rtl-test, we make the following observations. Given a set assignment ℳ = (, ) under rationalizability over a finite universe of size , and a collection V0 ∪ V1 of size of individual and set variables: 1. The interpretation takes () space. This is because the interpretation assigns values to variables from the collection, and since there are variables and each variable can be assigned a value from a universe of size , the total space required is proportional to . 2. The relation over that rationalizes c can be represented in (2) space. Here, c refers to the rational choice associated with the set assignment ℳ. The relation represents preferences among elements in the universe, and since the universe has size , storing it requires space proportional to 2.
Therefore, the total space complexity to store the interpretation and the relation over that rationalizes c is ( + 2).
Also, the time needed to check a purported set assignment ℳ = (, ) under the same aforementioned conditions is linear in its size ( + 2) (for instance, when verifying whether the rationalizing relation is indeed devoid of infinite ascending sequences, it sufices to check it for acyclicity, a task that can be accomplished in linear time with respect to its size, which is (2)).
For a given Rtl-satisfiable BSTC-formula of size , we can therefore generate a satisfying Rtl-model ℳ = (, ) with a universe of size = 2, over a collection of size () of individual and set variables, in (22 ) time and space. In addition, we can check that ℳ is indeed an Rtl-model for in deterministic (22 ) time.
Furthermore, the satisfiability problem for BSTC is NP-hard, as the satisfiability problem for propositional logic can readily be reduced to it (in linear time).
To summarize, we can state the following complexity result: Theorem 2. The satisfiability problem for BSTC-formulae under rationalizability belongs to the complexity classes NP-hard and NEXPTIME.
In this paper, we have explored the implications and characteristics of rational decision-making within the quantifier-free elementary fragment of set theory denoted as BSTC (Boolean Set Theory with a Choice operator). Our primary focus was on the satisfiability problem for BSTC-formulae. By interpreting the choice operator c as a rational choice, we have established that BSTC under rationalizability exhibits a small model property. This significant property has enabled us to demonstrate the decidability of the satisfiability problem for BSTC under rationalizability, classifying it as belonging to the complexity classes NP-hard and NEXPTIME. These findings represent an extension of previous work on the satisfiability problem in the presence of a choice operator.
For future research, it would be worthwhile to explore extensions of BSTC with a predicate
set is infinite). Additionally, further investigations can be carried out under alternative
axiomatizations of the choice operator, such as those associated with (, )-rationalizable
choices, which have been extensively studied in [
Furthermore, we intend to strengthen the small model property, if possible, along lines similar to those that allowed us to prove the NP-completeness of the theory BSTC− as hinted in Remark 1, thereby establishing the NP-completeness of BSTC under rationalizability.
By pursuing these research directions, we can deepen our understanding of the relationship between rational decision-making and set theory, paving the way for new insights and advancements in this interdisciplinary field. [8] F. Aleskerov, D. Bouyssou, M. B., Utility Maximization, Choice and Preference, Springer
Verlag, Berlin, 2007. doi:10.1007/978-3-540-34183-3. [9] C. P. Chambers, F. Echenique, E. Shmaya, General revealed preference theory, Theoretical
Economics 73 (2017) 493–511. doi:10.3982/TE1924. [10] H. Chernof, Rational selection of decision functions, Econometrica 22 (1954) 422–443.
doi:10.2307/1907435. [11] D. Cantone, A. Giarlotta, S. Watson, The satisfiability problem for Boolean set theory with a choice correspondence, in: P. Bouyer, A. Orlandini, P. San Pietro (Eds.), Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, Roma, Italy, 20-22 September 2017, volume 256, Electronic Proceedings in Theoretical Computer Science (EPTCS), 2017, pp. 61–75. doi:10.4204/EPTCS.256.5, available at http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2017.5.pdf. [12] D. Cantone, A. Ferro, E. G. Omodeo, Computable Set Theory, number 6 in International Series of Monographs on Computer Science, Oxford Science Publications, Clarendon Press, Oxford, UK, 1989. [13] D. Cantone, E. G. Omodeo, A. Policriti, Set Theory for Computing - From Decision Procedures to Declarative Programming with Sets, Monographs in Computer Science, Springer-Verlag, New York, 2001. doi:10.1007/978-1-4757-3452-2. [14] J. T. Schwartz, D. Cantone, E. G. Omodeo, Computational Logic and Set Theory: Applying Formalized Logic to Analysis, Springer-Verlag, 2011. doi:978-0-85729-808-9, foreword by M. Davis. [15] D. Cantone, P. Ursino, An Introduction to the Formative Processes Technique in Set Theory,
Springer International Publishing, 2018. [16] D. Cantone, A. De Domenico, P. Maugeri, E. G. Omodeo, Complexity assessments for decidable fragments of set theory. I: A taxonomy for the Boolean case, Fundamenta Informaticae 181 (2021) 37–69. doi:10.3233/FI-2021-2050. [17] D. Cantone, A. Ferro, Techniques of computable set theory with applications to proof verification XLVIII (1995) 1–45. [18] F. Parlamento, A. Policriti, K. P. S. B. Rao, Witnessing diferences without redundancies, Proceedings of the American Mathematical Society 125 (1997) 587–594.