In the context of Computable Set Theory, we consider the satisfiability problem for various subcases of the fragment BST⊗ (Boolean Set Theory with the unordered Cartesian product ⊗ ), whose long-standing decision problem has received very recently a positive solution in the NEXPTIME complexity class. BST⊗ is the quantifier-free set theory involving the Boolean set operators of union ( ∪), intersection (∩), and set diference ( ∖), as well as the unordered Cartesian product operator (⊗ ), and the set equality (=) and inclusion (⊆ ) predicates, where the unordered Cartesian product ⊗ of two sets and is defined as the collection of all possible unordered pairs formed by selecting one element from and one element from . It is an open problem whether the satisfiability problem for BST⊗ is NP-complete. Here, we delve into the specific case in which the number of distinct leading variables in literals of the form = ⊗ is O(log ), where represents the size of the BST⊗ formula that one wants to test for satisfiability, and prove its NP-completeness. We will also mention various additional NP-completeness and polynomial results concerning the decision problem for other subtheories of BST⊗ .
The field of Computable Set Theory has emerged from extensive research on the decision problem in set theory over the past few decades. This research, as documented in [5], originally aimed at mechanizing mathematics through a proof verifier based on set-theoretic formalism [21, 9, 19, 27]. However, it gradually evolved to focus on foundational aspects, specifically identifying the boundary between decidable and undecidable problems in set theory.
In 1980, the precursor fragment of set theory investigated for decidability was Multi-Level Syllogistic (MLS), as described in [16]. Since then, several progresses have been made, by extending MLS and demonstrating the decidability of their satisfiability problems. In some cases, the NP-completeness of these extensions has also been proven. For a more detailed and comprehensive account, the reader can refer to the monographs [5, 8, 27, 20, 12].
The decision problem for the extension MLS× of MLS with the Cartesian product × has been challenging and has resisted attempts to find a solution, whether positive or negative. Initially, it was even uncertain whether the satisfiability problem for MLS× was decidable, especially for ifnite models. There was speculation about a potential reduction of Hilbert’s Tenth problem (H10) to the satisfiability problem for MLS× . Hilbert’s Tenth problem [17] seeks a uniform procedure to determine if a given Diophantine polynomial equation with integral coeficients has a solution in integers. In 1970, it was proven that no algorithmic procedure exists for H10, known as the DPRM theorem [24, 15, 18].
It was hypothesized that the union of disjoint sets and the Cartesian product could mirror integer addition and multiplication in H10, respectively, based on the properties of set cardinalities: | ∪ | = || + || for disjoint sets and , and | × | = || · | | for sets and . This observation forms the basis of the proof for the undecidability of the satisfiability problem for MLS× when extended with the cardinality comparison predicate | · | ⩽ | · | (see [1] and [7]). In this case, || ⩽ || holds if and only if the cardinality of does not exceed that of .
Eforts to solve the satisfiability problem for MLS× have significantly influenced the advancement of computable set theory. These attempts have led to the introduction of the technique known as “formative processes," which has played a crucial role in the most intricate solutions to decision problems. The formative processes technique is extensively covered in [12], providing a relatively accessible introduction. Notably, this technique has been applied to solve the decision problems for the extensions MLSSP (with power set and singleton operators) [10] and MLSSPF (with finiteness predicate) [11].
Recently, an algorithmic solution to the satisfiability problem (s.p., for short) for the set theory fragment BST⊗ has been presented in [14]. This fragment is closely related to MLS× and is obtained by dropping the membership predicate ∈ from it and also by replacing the ordered Cartesian product operator × with its unordered variant ⊗ . In BST⊗ , ⊗ represents the set of unordered pairs {, } where ∈ and ∈ . Notably, these modifications do not afect the aforementioned connection with H10. The focus on BST⊗ instead of MLS× just allows for a more streamlined analysis, removing unnecessary complexities from the study.
The finite s.p. for the extension of MLS with cardinality comparison is reducible to purely existential Presburger arithmetic, a known NP-complete problem [26, 2, 25]. In contrast, when cardinality comparison is added to either BST× or BST⊗ , the finite s.p. for these extensions becomes undecidable. This is evident from the reduction of H10 to these problems, similar to the results in [1] and [7] for MLS⊗ and MLS× . These findings demonstrate that the decision problem for BST⊗ is situated at the brink of decidability.
To be more specific, the fragment of set theory BST⊗ is the quantifier-free propositional closure of atoms of the following types:
= ∪ , = ∩ , = ∖ , ⊆ , = ⊗ , where , , stand for (existentially quantified) set variables. Its ordinary and (hereditarily) ifnite s.p. have been proved to be decidable in [ 14] (see also [13] for a preliminary version), where NEXPTIME decision procedures have been provided.1
In this paper, we analyze a family of subtheories of BST⊗ , denoted BST⊗ log , where > 0, and prove that their s.p. is NP-complete.
As shown in [14], by means of a suitable normalization process, the s.p. for BST⊗ -formulae 1The ordinary and the (hereditarily) finite s.p. will be defined precisely in the next section. can be easily reduced to the corresponding s.p. for conjunctions of literals of the following forms: = ∪ , = ∖ , ̸= , = ⊗ . (1) Calling ⊗ -variable the leading variable in any ⊗ -literal of the form = ⊗ , the fragment BST⊗ log consists of normalized BST⊗ -conjunctions Φ that have at most log |Φ | distinct ⊗ variables. Here, is any positive real parameter and |Φ | represents the size of Φ , defined as the number of conjuncts in Φ . It is important to note that there is no restriction on the number of ⊗ -conjuncts in any Φ belonging to BST⊗ log .
The paper is organized as follows. In Section 2, we present the semantics of BST⊗ using partition assignments and provide a comprehensive overview of the relevant terminology and concepts. Next, in Section 3, we revisit key notions introduced in [14], such as ⊗ -graph, accessibility, fulfillment by a ⊗ -graph, and ⊗ -graphs induced by partitions. Additionally, we state two results from the same paper that are particularly relevant to our study. Subsequently, in Section 4, we introduce the novel concept of projection of a partition assignment and state various useful basic results related to them. We then proceed to prove the main result of the paper, namely the NP-completeness of the s.p. for the fragments BST⊗ log (for > 0). Finally, we conclude the paper with a summary of our findings and outline potential directions for future research.
A set assignment is a map from a collection of set variables, denoted as dom( ) (the variable-domain of ), to the von Neumann cumulative hierarchy := ⋃︀ ∈On of wellfounded sets. The universe is constructed in stages using transfinite recursion over the class On of all ordinals, where := ⋃︀< pow( ), for every ∈ On, with pow(· ) denoting the powerset operator.2 The rank of a well-founded set ∈ is the least ordinal such that ⊆ . The collection of the sets with finite rank, namely those that belong to for some ifnite ordinal , is the set of the hereditarily finite sets (HF).
The operators in BST⊗ are interpreted based on their usual semantics. For a set assignment and , , ∈ dom( ), we have
( ⋆ ) := ⋆ , where ⋆ ∈ {∪, ∩, ∖, ⊗} and where in particular ⊗ , for any sets and , is the set of all the unordered pairs {, } such that ∈ and ∈ : in symbols, ⊗ := {{, } | ∈ , ∈ }.
A set assignment is extended to interpret the BST⊗ -atoms over the variables in dom( ) by putting: ( = ⋆ ) = true ( = ) = true ( ⊆ ) = true →−← →−←
Def Def Def = ( ⋆ ), = , ⊆ , →−← for all , , ∈ dom( ) and ⋆ ∈ {∪, ∩, ∖, ⊗} , and recursively for the propositional connectives. 2Thus, 0 = ⋃︀< 0pow( ) = ∅, since 0 is the smallest ordinal.
Given a set assignment and a collection of variables ′ ⊆ = dom( ), we put ′ = { | ∈ ′}. The set-domain of is the set ⋃︀ = ⋃︀∈ . A set assignment is finite (resp., hereditarily finite) if so is its set-domain.
A BST⊗ -formula Φ is satisfied by a set assignment if Φ = true, in which case we write |= Φ and say that is a model for Φ . If Φ has a model, then Φ is satisfiable; otherwise, it is unsatisfiable. If |= Φ and is finite (resp., hereditarily finite), then Φ is finitely satisfiable (resp., hereditarily finitely satisfiable).
The satisfiability problem for BST⊗ refers to the task of determining whether a given BST⊗ -formula can be satisfied by some set assignment.
We observe that the empty set ∅ can be characterized by means of the BST⊗ -literal ∅ = ∅ ∖ ∅, where ∅ can be regarded as a reserved variable, and that each literal = ∪ is equisatisfiable with the conjunction
= ∖ ∧ = ∖ ∧ ∅ = ∖ , where is a newly introduced variable. Hence, we can drop from the list (1) the literals of the form = ∪ , and restricting ourselves hereafter, without loss of generality, to the s.p. for conjunctions of literals of the following three types:
= ∖ , ̸= , = ⊗ .
In [14], it was demonstrated that both the ordinary and the finite (resp., hereditarily finite) satisfiability problems for BST⊗ can be efectively solved, indicating the existence of algorithmic tests that can provide answers for all instances of these problems. These results were established within the framework of partition assignments. (We recall that a partition is a set of pairwise disjoint nonempty sets, called the blocks of the partition.) Definition 1 (Partition assignments). Let Φ be any BST⊗ -conjunction, and let Vars(Φ) denote the set of all the variables occurring in Φ . A partition Σ is said to satisfy Φ via some map I : Vars(Φ) → pow(Σ) (called a partition assignment), and we write Σ /I |= Φ , if the set assignment I induced by I satisfies Φ , where I := ⋃︀I() for ∈ Vars(Φ) . A partition Σ is said to satisfy Φ , and we write Σ |= Φ , if it satisfies Φ via some partition assignment.
We close the section by introducing the unary variant of the unordered Cartesian product, similar to the unary versions of the binary set operators ∪ and ∩, which are defined as follows: ⋃︀ := { | ∈ , for some ∈ } and ⋂︀ := { | ∈ , for all ∈ }.
Specifically, for any sets and (which may or may not be distinct), we put ⊗ {, } := ⊗ , where we recall that ⊗ = {︀ {, } | ∈ , ∈ ︀} .
Following [14], we review the definitions of ⊗ -graphs, accessible ⊗ -graph, the notion of fulfillment by an accessible ⊗ -graph, and two relevant results connected to them. Definition 2 (⊗ -graphs). A ⊗ -graph is a directed bipartite graph whose set of vertices comprises two disjoint parts: a set of places , such that ∩ ( ⊗ ) = ∅, and a set of {P4,P5} {P2} ⊗ -nodes , where ⊆ ⊗ . The edges issuing from each place are exactly all pairs ⟨, ⟩ such that ∈ ∈ : these are the membership edges. The remaining edges of , called distribution edges, go from ⊗ -nodes to places. When there is an edge ⟨, ⟩ from a ⊗ -node to a place , we say that is a target of . Every ⊗ -node must have at least one target. The map over defined by
() := { ∈ | is a target of }, for ∈ , is the target map of , hence we have : → pow+(), where pow+() := pow() ∖ {∅}. Plainly, a ⊗ -graph is fully characterized by the set of its places and its target map , since the sets of the ⊗ -nodes of is expressible as dom( ). The size of a ⊗ -graph is the cardinality of its set of places.
Figure 1 presents an example of a ⊗ -graph, where the round shaped vertices (1, 2, 3, 4, and 5) are the places and the box shaped vertices are the nodes. Recalling that nodes are pairs of places, in the example the node {2} stands for the (unordered) pair {2, 2}. Dashed edges are the membership edges of our ⊗ -graph: these connect each place of the ⊗ -graph to the nodes that contain it. Finally, the remaining edges are the distribution edges of our ⊗ -graph, and connect nodes to places.
Definition 3 (Accessible ⊗ -graphs). A place of a ⊗ -graph = (, , ) is a source place if it has no incoming edges. The remaining places, namely those with incoming edges, are called ⊗ -places. We denote by ⊗ the set of the ⊗ -places of . A place of is accessible (from the source places of ) if either it is a source place or, recursively, it is the target of some node of whose places are all accessible from the source places of . Finally, a ⊗ -graph is accessible when all its places are accessible.3 Definition 4 (Fulfillment by an accessible ⊗ -graph). An accessible ⊗ -graph = (, , ) fulfills a given BST⊗ -conjunction Φ provided that there exists a map F : Vars(Φ) → pow() (called a -fulfilling map for Φ ) such that the following conditions are satisfied: (a) F() = F() ∖ F(), for every conjunct = ∖ in Φ ; (b) F() ̸= F(), for every conjunct ̸= in Φ ; and (c) for every conjunct = ⊗ in Φ , (c1) F() ⊗ F() ⊆ dom( ); (c2) F() = ⋃︀ [F() ⊗ F()]; and (c3) ⋃︀ [︀ ∖ (F() ⊗ F())]︀ ∩ F() = ∅.
Let Φ be a satisfiable BST⊗ -conjunction and let Σ be a partition that satisfies Φ via a map I : → pow(Σ) , where := Vars(Φ) . Also, let ⊗ be the collection of the ⊗ -variables of Φ .
We illustrate the construction of Σ, the ⊗ -graph induced by Σ and Φ , where for simplicity the dependence on Φ in the notation Σ is implicitly understood.4
Let = ⊗ , for = 1, . . . , , be the ⊗ -atoms of Φ , so that ⊗ = {1, . . . , }. We put Σ ⊗ := ⋃︀ I() = ⋃︀I[⊗ ] and Π ⊗ := ⋃︀ (︀ I() ⊗ I()︀) . Hence ⋃︀Σ ⊗ = ⋃︀⊗ [Π ⊗ ] 1⩽⩽ 1⩽⩽ holds.
Let Σ be any set of the same cardinality as Σ and such that Σ ∩ ︀( Σ ⊗ Σ︀) = ∅, and let ↦→ (∙ ) be any bijection from Σ onto Σ . Places in Σ are intended to represent the blocks in Σ , via the bijection (∙ ).
Let Σ ⊆ Σ ⊗ Σ be such that Σ(∙ ) = Π ⊗ , where the bijection (∙ ) has been naturally extended to any set ∈ Σ⊗ Σ, by putting (∙ ) := {(∙ ) | ∈ }, and to any set A ⊆ Σ⊗ Σ, by putting A(∙ ) := {(∙ ) | ∈ A}. The members of Σ are the ⊗ -nodes of the ⊗ -graph Σ we are after. Hence, the vertex set of Σ is the union Σ ∪ Σ. The disjoint sets Σ and Σ will form the parts of the bipartite graph Σ.
Concerning the edges of Σ, for all places ∈ Σ and ⊗ -nodes ∈ Σ such that ∈ , there is a membership edge ⟨, ⟩ in Σ. In addition, for all ⊗ -nodes and places such that (∙ ) ∩ ⊗ (∙ ) ̸= ∅, there is a distribution edge ⟨, ⟩ in Σ. Only places such that (∙ ) ∈ Σ ⊗ have incoming edges. We call them ⊗ -places and denote their collection by Σ,⊗ . Hence, Σ() := { ∈ Σ,⊗ | (∙ ) ∩ ⊗ (∙ ) ̸= ∅}, for ∈ Σ is the target map Σ of Σ.
Next, we define a map FΣ : Vars(Φ) assignment I, by putting
→ pow(Σ), which is supposed to abstract the partition
FΣ() := { ∈ Σ | (∙ ) ∈ I()}, The following two lemmas hold, both proved in [14]: for ∈ Vars(Φ) .
(2) 3Thus, a ⊗ -graph with no source places is trivially not accessible. 4It is also possible to define a variant of the ⊗ -graph solely induced by Σ. This alternative approach was undertaken in [14].
P2 {P2} P1 {P1} Lemma 1. The ⊗ -graph Σ induced by the partition Σ (and by the BST⊗ -conjunction Φ ) is accessible and fulfills Φ via the map FΣ defined in (2).
Lemma 2. A BST⊗ -conjunction fulfilled by an accessible ⊗ -graph is satisfiable.
The two preceding lemmas yield at once the following result: Theorem 1. A BST⊗ -conjunction with distinct variables is satisfiable if and only if it is fulfilled by an accessible ⊗ -graph.
Next, we present an example of a satisfiable BST⊗ -conjunction and the ⊗ -graph fulfilling it.
Φ := = ⊗ ∧ = ∖ ∧ = ∖ ∧ ̸= . (3) We claim that the ⊗ -graph = ( , , ) in Figure 2 is accessible and fulfills Φ . The sets of places and nodes of are = {1, 2} and
= {︀ {1}, {2}, {1, 2}}︀ , respectively, and the target map : → pow+( ) of is given by
({1}) = ({2}) = ({1, 2}) = {1}.
By observing that all places of are source places, the accessibility of follows immediately. Next, we show that the ⊗ -graph fulfills Φ via the map F : {, , } → pow( ), where F() = {1, 2},
F() = {1},
F() = ∅.
We just have to check that the conditions (a), (b), and (c) in Definition 4 are satisfied for Φ . , F, and
In relation to condition (a) with respect to the conjuncts = ∖ and = ∖ , we have, respectively: In relation to condition (b) with respect to the conjunct ̸= , we have:
F() ∖ F() = ∅ ∖ ∅ = ∅ = F(),
and F() ∖ F() = {1} ∖ {1, 2} = ∅ = F().
F() = {1} ≠ ∅ = F().
Finally, as regards condition (c) with respect to the conjunct = ⊗ , we have: (c1) (c2) (c3)
F() ⊗ F() = {{1}, {2}, {1, 2}} = dom( ); ⋃︀ [F() ⊗ F()] = ⋃︀ [︀{ {1}, {2}, {1, 2}}︀] = ⋃︀{︀ {1}} = {1} = F(); since ⋃︀ [ ∖ (F() ⊗ F())] = ⋃︀ [∅] = ∅, we readily have
⋃︀ [ ∖ (F() ⊗ F())] ∩ F() = ∅.
In view of Lemma 2 recalled above, the above considerations allow us to deduce that the formula Φ is satisfiable. In fact, Φ has the model such that = HF, = HF ⊗ HF, and = ∅, where we recall that HF denotes the set of the hereditarily finite sets. In addition, it is easy to check that the formula Φ is not finitely satisfiable. This fact becomes clear once one notes that the formula (∃)(∃)Φ is equivalent to the conjunction ⊗ ⊆ ∧ ̸= ∅.
▷
Preliminarily, we adapt to partition assignments the concept of a set distinguishing a collection of variables with respect to a set assignment, introduced in [4] (see also [23]). We also state some properties associated with it, whose proofs are omitted due to space limits.
Given a partition Σ , a map I : → pow(Σ)
over a set of variables , and a ⊆ Σ , the projection of I to Σ ′ is the map IΣ′ : → pow(Σ ′) defined by 4.1. Distinguishing sets of variables Definition 5. subpartition Σ ′ Σ ′ ⋉I ′, if IΣ′ () := I() ∩ Σ ′, for all ∈ .
We say that the subpartition Σ ′ distinguishes a subset ′ ⊆ (relative to I), and write ′ ∈ Σ ′ for which the following biimplication holds:
I() ̸= I() =⇒
IΣ′ () ̸= IΣ′ (), for all , ∈ ′, namely if for every pair of variables , ∈ ′ such that I() ̸= I() there exists a block ′ ∈ I() ⇐⇒ ′ ∈/ I().
(4) A block ′ satisfying (4) is said to distinguish and (relative to I).
The property Σ ′ ⋉I ′ propagates upward with respect to its first argument and downward (namely it is hereditary) with respect to its second argument, as stated in the following lemma. Lemma 3. Given Σ ′ ⊆ Σ and ′ ⊆ , we have (a) (∀ Σ ′′ | Σ ′ ⊆ Σ ′′ ⊆ Σ)(Σ
′ ⋉I ′ =⇒ Σ ′′ ⋉I ′), and (b) (∀ ′′ ⊆ ′)(Σ ′ ⋉I ′ =⇒ Σ ′ ⋉I ′′).
Proof. As for (a), it is enough to observe that, if Σ ′ ⊆ Σ ′′ ⊆ Σ and , ∈ , then IΣ′ () ̸= IΣ′ () =⇒ =⇒
I() ∩ Σ ′ ̸= I() ∩ Σ ′
I() ∩ Σ ′′ ̸= I() ∩ Σ ′′ =⇒
IΣ′′ () ̸= IΣ′′ ().
Property (b) is immediate.
The next lemma asserts that, for any finite partition Σ and any finite set of variables , every subpartition Σ ′ of Σ that distinguishes a subset ′ of (relative to a given partition assignment) can be extended with at most one block for each of the variables in ∖ ′ to a subpartition of Σ that distinguishes the whole .
Lemma 4. Let Σ be a finite partition and a finite set of variables, and let I : → pow(Σ) be a partition assignment over . Let Σ ′ ⊆ Σ and ′ ⊆ be such that Σ ′ ⋉I ′. Then, relative to I, is distinguished by a subpartition Σ ′′ ⊆ Σ extending Σ ′ and whose cardinality exceeds that of Σ ′ by at most | ∖ ′|, namely such that |Σ ′′| ⩽ |Σ ′| + | ∖ ′|.
Proof. Let 1, . . . , be the distinct variables in ∖ ′, with := | ∖ ′|, and let Σ ′0 := Σ ′. Recursively, we define Σ ′ ⊆ Σ , for = 1, . . . , , by setting ⎧ ⎪Σ ′− 1 ⎨ Σ ′ := Σ ′− 1 ∪ { } ⎪ ⎩ if Σ ′− 1 ⋉I ′ ∪ {1, . . . , }, otherwise, where is any5 block in Σ such that Σ ′− 1 ∪ { } ⋉I ′ ∪ {1, . . . , }.
Note that the above recursive definition contains an implicit claim, namely that if Σ ′− 1 ⋉/I ′ ∪ {1, . . . , } then there exists ∈ Σ such that Σ ′− 1 ∪ { } ⋉I ′ ∪ {1, . . . , }. We show that such a claim indeed holds for all ∈ {1, . . . , }, thereby proving that the definition of the Σ ′’s is well-given. To this purpose, it is enough to observe that, for ∈ {1, . . . , }, if Σ ′− 1 is defined and Σ ′− 1 ⋉/I ′ ∪ {1, . . . , }, then it can be proved that there exists some block ∈ Σ such that Σ ′− 1 ∪ { } ⋉I ′ ∪ {1, . . . , }.
Letting Σ ′′ := Σ ′, we plainly have that is distinguished by Σ ′′. Indeed, by the very definition of Σ ′, if Σ ′ = Σ ′− 1 then Σ ′− 1 ⋉I ′ ∪ {1, . . . , }, whereas if Σ ′ ̸= Σ ′− 1 then Σ ′ ⋉I ′ ∪ {1, . . . , }, and in any case Σ ′ ⋉I holds, since = ′ ∪ {1, . . . , }. In addition, we have
|Σ ′| ⩽ |Σ ′| + = |Σ ′| + | ∖ ′|, proving the lemma. 4.2. The NP-completeness proof Let Φ be a satisfiable BST⊗ -conjunction and let Σ be a partition that satisfies Φ via a map I : → pow(Σ) , where := Vars(Φ) . Also, let ⊗ be the collection of the ⊗ -variables of Φ .
We will prove that if |⊗ | ⩽ log |Φ | for some > 0, then the conjunction Φ can be fulfilled by an accessible ⊗ -graph of size O(|Φ |max(, 1)). This will imply that in nondeterministic polynomial time one can construct an accessible ⊗ -graph and a -fulfilling map for Φ , thereby establishing the nondeterministic polynomiality of the s.p. for each of the subfragments BST⊗ log of BST⊗ . 5A don’t-care nondeterminism is present in the recursive definition of the Σ′’s, as no specific instructions are given regarding the selection of the block ∈ Σ such that Σ′− 1 ∪ { } ⋉I ′ ∪ {1, . . . , }. However, any valid choice will sufice. In addition, by ordering Σ, such nondeterminism could be easily eliminated.
Let as follows:
Let, as before, Σ ⊗ := ⋃︀I[⊗ ] be the subpartition consisting of all blocks in Σ that belong to some I(), where ∈ ⊗ . We define the following equivalence relation ∼ ⊗ over Σ ⊗ : ∼ ⊗ →−←
Def
(∀ ∈ ⊗ )(︀ ∈ I() ⇐⇒ ∈ I())︀ .
∈ Σ ⊗ , and let ⊗ , := { ∈ ⊗ | ∈ I()}. The equivalence class [ ]∼ ⊗ can be expressed Within each equivalence class of ∼ ⊗ their collection by Σ ∼ ⊗
. Thus, we have: [ ]∼ ⊗ := ⋂︀{︀ I() | ∈ ⊗ ,
︀} ∖ ⋃︀{︀ I() | ∈ ⊗ ∖ ⊗ , ︀} , the number of equivalence classes of ∼ ⊗ is bounded by 2|⊗ | − showing that there is an injective map [ ]∼ ⊗ ↦→ ⊗ , , where ⊗ , ∈ pow+(⊗ ), and therefore , we choose any representative block, and we denote Lemma 5. The subpartition Σ ∼ ⊗ distinguishes the variables in ⊗ (in the sense of Definition 5). Proof. Let I() ̸= I(), for some , ∈ ⊗ . Then there exists a block ∈ Σ such that |Σ ∼ ⊗ | < 2|⊗ |. ∈ I() ⇐⇒ /∈ I(), (5) (6) (7) so that ∈ Σ ⊗ . Letting ∈ Σ ∼ ⊗
be the ∼ ⊗ -representative of in Σ ⊗ , we plainly have ∈ I() ⇐⇒ ∈ I() and ∈ I() ⇐⇒ ∈ I(), Lemma 3(a), so does Σ ∼ ⊗
. and therefore, by (6), ∈ I() ⇐⇒
/∈ I(). Hence, distinguishes and and, by the whole set of the variables occurring in Φ and such that
By Lemma 4 and the inequality (5), there exists an extension Σ I ⊆ Σ of Σ ∼ ⊗ that distinguishes |Σ I | ⩽ ⃒⃒ Σ ∼ ⊗ ⃒⃒ + | ∖ ⊗ | < 2|⊗ | + | | ⩽ 2|⊗ | + 3 · | Φ |.
Thus, ⊆ satisfies Φ via the mapping I, we have I = I ⊗ I, namely ⋃︀I() = ⋃︀I() ⊗ Given ∈ Σ ⊗ , there is a ⊗ -literal = ⊗ in Φ , such that ∈ I(). Recalling that Σ ⋃︀I() ⊗ ⋃︀I(), and so there exist ∈ I() and ∈ I() such that intersects the ⋃︀I().
P⊗ , := {︀ ∈ Σ ⊗ Σ | (⊗ ) ∩ ⋃︀[ ]∼ ⊗ ̸= ∅}︀ product ⊗ . Hence, the set is nonempty for all ∈ Σ ⊗ .
For every ∈ Σ I ∩ Σ ⊗ , we select from P⊗ , an unordered pair such that ⊗ contains , and call the doubleton the precursor of . Then, we put some member of minimal rank in ⋃︀⊗ [P⊗ , ]∩⋃︀[ ]∼ ⊗ From (7), we have
Σ II := Σ I ∪ (︀ ⋃︀{ | ∈ Σ I ∩ Σ ⊗ } ∖ Σ ⊗ )︀ . | Σ II | ⩽ ⃒⃒ Σ I ⃒⃒ + ⃒⃒ ⋃︀{ | ∈ Σ I ∩ Σ ⊗ } ∖ Σ ⊗ ⃒⃒ ⩽ |Σ I | + 2 · ⃒⃒ Σ I ∩ Σ ⊗ ⃒⃒ ⩽ 3 · | Σ I | ⩽ 3 · 2|⊗ | + 3 · | Φ |)︁ .
︁( be any bijection from onto Σ .
Thus, taking into account our hypothesis |⊗ | ⩽ log |Φ |, where > |Σ II | ⩽ 3 · (2 log |Φ| + |Φ |) = 3 · (|Φ | + |Φ |) ⩽ 12 · | Φ | 0, we have max(, 1).
Let be any set of the same cardinality as Σ and such that ∩ ︀( ⊗ )︀ = ∅, and let ↦→ (∙ ) when
We define next an accessible ⊗ -graph II = (︀ II , II , II )︀ of size |Σ II | and then prove that it fulfills Φ . Let
II := {︀ ∈ | (∙ ) ∈ Σ II }︀ .
Only places ∈ II such that (∙ ) ∈ Σ ⊗ —and hence such that (∙ ) ∈ Σ I ∩ Σ ⊗ —are targets of some ⊗ -node in II ⊆ II ⊗ II . In order to characterize the distribution edges of II , we extend the equivalence relation ∼ ⊗ to an equivalence relation ∼ ⊗⋆ over the whole partition Σ by letting ∼ ⊗⋆ := ∼ ⊗ ∪ ︀{ { } | ∈ Σ ∖ Σ ⊗ ︀} .
To simplify the exposition, for all places , and unordered pairs of places and , in what follows we will write ∼ ⊗ , ∼ ⊗⋆ ,
∼ ⊗⋆ (∙ ) ∼ ⊗ (∙ ), (∙ ) ∼ ⊗⋆ (∙ ), (∙ ) ∼ ⊗⋆ (∙ ) hold, respectively. Also, if ∼(∙ ⊗ ) is the representative block in the ∼ ⊗ -equivalence class [(∙ )]∼ ⊗ , we will refer to the place ∼ ⊗ as the ∼ ⊗ -representative of . Finally, if the unordered pair of blocks (∙ ) is the precursor of a block (∙ ), we also say that the ⊗ -node is the precursor of the place .
For all ⊗ -nodes := {1, 2} and := {1, 2} of Σ, we put
Def ∼ ⊗⋆ →−← (∃ ∈ {1, 2})(1 ∼ ⊗⋆ ∧ 2 ∼ ⊗⋆ 3− ).
Similarly, for all distribution edges ⟨, ⟩ and ⟨, ⟩ of Σ, we put
Def ⟨, ⟩ ∼ ⊗⋆ ⟨, ⟩ →−← ( ∼ ⊗⋆ ∧ ∼ ⊗⋆ ).
For all ∈ II ⊗ II and ∈ II , ⟨, ⟩ is a distribution edge of II if and only if Σ contains a distribution edge ⟨, ⟩ such that ⟨, ⟩ ∼ ⊗⋆ ⟨, ⟩. The graph II contains no other distribution edges.
The set II of the ⊗ -nodes of II consists of all ∈ II ⊗ II for which ⟨, ⟩ is a distribution edge of II , for some ∈ II .
A ⊗ -node of II is a precursor node of a ⊗ -place of II if and only if there exists a distribution edge ⟨, ⟩ of Σ such that ⟨, ⟩ ∼ ⊗⋆ ⟨, ⟩ and is the precursor of .
For each ⊗ -node {1, 2} of II , the membership edges ⟨︀ 1, {1, 2}︀⟩ and ⟨︀ 2, {1, 2}︀⟩ are in II , and these are the only membership edges of II . Thus, Lemma 6. The ⊗ -graph II has size at most 12 · | Φ |max(, 1).
Next, we show that the ⊗ -graph II is accessible.
Proof. For a contradiction, let us assume that II is not accessible, and let be a non-accessible ⊗ -place of II (hence (∙ ) ∈ Σ ⊗ ) such that ⋃︀[(∙ )]∼ ⊗ contains a member of smallest rank among the non-accessible ⊗ -places of II . Also, let {1, 2} be a precursor ⊗ -node of (in II ). Then, there are 1, 2, ∈ Σ such that – (1∙ ) ∼ ⊗⋆ (1∙ ), (2∙ ) ∼ ⊗⋆ (2∙ ), and (∙ ) ∼ ⊗⋆ (∙ ); – ⟨︀ {1, 2}, ⟩︀ is a distribution edge of Σ; and – (∙ ) contains some member of smallest rank in ⋃︀[(∙ )]∼ ⊗ . tion Φ .
Since both ⋃︀[(1∙ )] ∼ ⊗ and ⋃︀[(2∙ )]
∼ ⊗ contain elements of smaller rank than that of any element contradiction, proving that II is accessible. in ⋃︀[(∙ )] 1 and 2 are accessible in II . Therefore, after all, the place is accessible in II , which is a ∼ ⊗
, the minimality of among all the non-accessible ⊗ -places of II yields that both We are now ready to prove our main result, namely that the ⊗ -graph II fulfills our conjunca II -fulfilling map for Φ . Hence the ⊗ -graph II fulfills the BST⊗ -conjunction Φ .
FII () := FΣ() ∩ II , for each ∈ , is Proof. Preliminarily, we observe that we have:
FII () = {︀ ∈ | (∙ ) ∈ I() ∩ Σ II }︀ , for every ∈ .
(8) Concerning the fulfilling condition (a) for FII , for every literal = ∖ in Φ we have FII () = FΣ() ∩
II = (︀ FΣ() ∖ FΣ())︀ ∩
II = (︀ FΣ() ∩
II )︀ ∖ ︀( FΣ() ∩
II )︀ = FII () ∖ FII () condition (a) for FII . (since, by the same fulfilling condition for FΣ, it holds that FΣ() = FΣ() ∖ FΣ()), proving
As regards the fulfilling condition (b) for FII , for every literal in Φ of the form ̸= , by the same fulfilling condition for
FΣ it holds that FΣ() ̸= FΣ(), and therefore I() ̸= I(). By (8), we readily obtain FII () ̸= FII (), thus establishing also condition (b) for FII . recalling that Σ II distinguishes (relative to I), we have I() ∩ Σ II ̸= I() ∩ Σ II . Hence, by
As for condition (c) of Definition 4, we need to prove that the following fulfilling conditions hold, for every ⊗ -literal = ⊗ in Φ : (c1) FII () ⊗ FII () ⊆ dom( II ), (c2) FII () = ⋃︀ II [FII () ⊗ FII ()], and (c3) ⋃︀ II [︀ II ∖ (FII () ⊗ FII ())]︀ ∩ FII () = ∅, where II and II are the target map and the set of the ⊗ -nodes of II , respectively. Thus, let = ⊗ be any ⊗ -literal in Φ .
Concerning condition (c1), let ∈ FII () and ∈ FII (). Hence, it holds that , ∈ II , ∈ FΣ(), and ∈ FΣ(). Since, by Lemma 1, the ⊗ -graph Σ induced by the partition Σ and by Φ fulfills the
BST⊗ -conjunction Φ via the map FΣ, from conditions (c1) and (c2) for FΣ, it follows that ∅ ̸= Σ({, }) ⊆
FΣ(). Let ∈ Σ({, }), so that ∈ FΣ() and , and let ∼ ⊗ ∈ Σ be the ∼ ⊗ -representative of . Then, ⟨︀ {, }, ∼ ⊗ ︀⟩ is a distribution edge in II , proving that {, } ∈ dom( II ), and in turn establishing condition
Next, concerning the fulfilling condition (c 2) for FΣ, let ∈ FII (), so that ∈ FΣ() ∩ II . Hence, by the same fulfilling condition for ∈ Σ({, }). Letting ∼ ⊗ and ∼ ⊗
FΣ, there exist ∈ FΣ() and ∈ FΣ() such that be the ∼ ⊗ -representatives of the equivalence classes and []∼ ⊗ , respectively, we have ∼ ⊗ ∈ FII (), ∼ ⊗ ∈ FII (), and {∼ ⊗ , ∼ ⊗ } ∼ ⊗ {, }. ∈ II (︀ {∼ ⊗ , ∼ ⊗ } ⊆ ︀) ⋃︀ II [︀ FII () ⊗ FII ()]︀ , and therefore we have FII () ⊆ ⋃︀ II [FII () ⊗ FII ()].
As for the reverse inclusion, let ∈ FII () and ∈ FII (), and let ∈ II ({, }). Then there exist , , and such that ∈ Σ({, }), ∼ ⊗⋆ , ∼ ⊗⋆ , and ∼ ⊗⋆ . We need to show that ∈ FII (). Since ∈ II , it is enough to prove that ∈ FΣ(). From ∼ ⊗⋆ and ∈ FΣ(), we have ∈ FΣ(). Likewise, we have ∈ FΣ(). Thus, {, } ∈ FΣ() ⊗ FΣ() and therefore, by the fulfilling condition (c 2) for FΣ, we have ∈ FΣ(). Since ∼ ⊗⋆ , the latter implies that ∈ FΣ(), which is precisely what we wanted to prove. Thus, we have ⋃︀ II [FII () ⊗ FII ()] ⊆ FII () that, together with the inclusion proved earlier, implies FII () = ⋃︀ II [FII () ⊗ FII ()], proving that the fulfilling condition (c 2) holds for FII .
Finally, to prove that also the fulfilling condition (c 3) holds for FII , it is enough to show that, taken any ∈ FII () and {, } ∈ dom( II ) ∖ (︀ FII () ⊗ FII ())︀ , (9) we have ∈/ II (︀ {, })︀ .
If, for contradiction, we have ∈ II (︀ {, })︀ under the hypotheses (9), then there exist places , , ∈ Σ such that
∼ ⊗⋆ , ∼ ⊗⋆ , ∼ ⊗⋆ , and ∈ Σ({, }), so that (∙ ) ∩ ((∙ ) ⊗ (∙ )) ̸= ∅. Since ∈ FII () = FΣ() ∩ II and ∼ ⊗⋆ , it follows that ∈ FΣ(). Hence, (∙ ) ∈ I(). Letting {, } ∈ (∙ ), where ∈ (∙ ) and ∈ (∙ ), in view of ⋃︀I() = ⋃︀I() ⊗ ⋃︀I() (since Σ /I |= = ⊗ ), we have {, } ∈ ⋃︀I() ⊗ ⋃︀I(). Without loss of generality, let us assume that ∈ ⋃︀I() and ∈ ⋃︀I(). Then we have (∙ ) ∈ I() and (∙ ) ∈ I(), and so (∙ ) ∈ I() and (∙ ) ∈ I(), which yield ∈ FΣ() and ∈ FΣ(). From {, } ∈ dom( II ) we have , ∈ II , and so ∈ FII () and ∈ FII (), from which it follows that {, } ∈ FII () ⊗ FII (), which is a contradiction. Thus, even the last fulfilling condition (c 3) holds for FII .
This completes the proof that FII is indeed a II -fulfilling map for Φ .
Letting := max(, 1), from Lemmas 6, 7, and 8, it follows that our satisfiable BST⊗ log conjunction Φ is fulfilled by an accessible ⊗ -graph II of size at most 12 · | Φ | via a suitable II -fulfilling map FII . These, namely II and FII , can be constructed in nondeterministic O︀( |Φ |3 )︀ time, and in deterministic O(︀ |Φ |3 )︀ time, it can be verified that II fulfills Φ via FII indeed. Hence, in view of Lemma 2, the s.p. for each of the subfragments BST⊗ log of BST⊗ (with > 0) is in NP. The NP-hardness is inherited from that of the s.p. for the theory BST proved in [3], where BST is the subtheory of BST⊗ obtained by forbidding all the literals of the form = ⊗ . Hence, the NP-completeness of each fragment BST⊗ log follows: Theorem 2. For every > 0, the s.p. for the theory BST⊗ log is NP-complete.
Through an analysis of the subfragments BST⊗ log of BST⊗ , in this paper we have established the NP-completeness of their satisfiability problems for any > 0. This result contributes to our understanding of the computational complexity of BST⊗ , which currently falls within drawn from the list where the bounds of NP-hardness and NEXPTIME. It is expected that if the s.p. for the whole theory BST⊗ is NP-complete, the techniques developed here may be generalized so as to prove it.
Decision algorithms for enhanced versions of MLS (and therefore for BST) have become crucial in the inference mechanisms utilized by the proof-checker ÆtnaNova, also known as Ref [27]. Given the widespread use of this mechanism in practical applications of ÆtnaNova, as discussed in [22, 20] and in the sections on ‘blobbing’ of [27], it is advantageous to minimize the occasional poor performance associated with the full-strength decision algorithm whenever possible. Therefore, identifying valuable ’small’ fragments of set theory that possess eficient decision tests is of utmost importance.
In light of this, building upon the work initiated in [6, 3], we have already embarked on the investigation of the satisfiability problem for other valuable subfragments of BST⊗ . Specifically, letting BST⊗ (︀ lit1, lit2, . . . )︀ denote the subtheory of BST⊗ involving only literals lit1, lit2, . . . (∖), (∪), (∩), (̸=), (⊆⊗ ), (⊗⊆ ), (⊗ ), the one discussed extensively in the preceding section: (with ⋆ ∈ {∖, ∪, ∩}), we have already obtained the following complexity results, in addition to BST⊗ (︀ ̸=, ⊆⊗ BST⊗ (︀ ̸=, ⊗⊆ ︀) : both the ordinary and the finite s.p. have a O(2) complexity; ︀) : the ordinary s.p. is O(), while the finite s.p. is NP-complete; BST⊗ (︀ ̸=, ⊗ )︀ : both the ordinary and the finite s.p. are NP-complete; BST⊗ log : the finite s.p. is NP-complete.
Our future plans involve extending this complexity taxonomy to encompass more combinations of literals of the aforementioned types.
Informaticae, 181(1):37–69, 2021.
verification. XLVIII(9-10):1–45, 1995. [1] D. Cantone, V. Cutello, and A. Policriti. Set-theoretic reductions of Hilbert’s tenth problem.
In Proc. of 3rd Workshop “Computer Science Logic” 1989, pages 65–75, 1990. Lecture Notes in Computer Science, 440. [2] D. Cantone, V. Cutello, and J. T. Schwartz. Decision problems for Tarski’s and Presburger’s arithmetics extended with sets. In E. Börger, H. Büning, M. Richter, and W. Schönfeld, editors, Proceedings of 3rd Workshop Computer Science Logic - CSL ’90 (Heidelberg 1990), pages 95–109 Berlin, 1990. Lecture Notes in Computer Science, 533. [3] D. Cantone, A. De Domenico, P. Maugeri, and E. G. Omodeo. Complexity assessments for decidable fragments of set theory. I: A taxonomy for the Boolean case. Fundamenta [4] D. Cantone and A. Ferro. Techniques of computable set theory with applications to proof [5] D. Cantone, A. Ferro, and E.G. Omodeo. Computable Set Theory, vol. 6 International Series of Monographs on Computer Science. Clarendon Press, Oxford, UK, 1989. [6] D. Cantone, P. Maugeri, and E. G. Omodeo. Complexity assessments for decidable fragments of set theory. II: A taxonomy for ‘small’ languages involving membership. Theoretical Computer Science, 848:28–46, 2020. [7] D. Cantone, E. G. Omodeo, and M. Panettiere. Reconciling transparency, low ∆ 0-complexity, and axiomatic weakness in undecidability proofs. Journal of Logic and Computation, 33(4):738–763, 2023. [8] D. Cantone, E.G. Omodeo, and A. Policriti. Set Theory for Computing - From decision procedures to declarative programming with sets. Monographs in Computer Science. Springer-Verlag, New York, 2001. [9] D. Cantone, E.G. Omodeo, J.T. Schwartz, and P. Ursino. Notes from the logbook of a proof-checker’s project. In N. Dershowitz, editor, Verification: Theory and Practice (Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday), vol. 2772 of Lecture Notes in Computer Science, pp. 182–207, Springer-Verlag, Berlin, 2003. [10] D. Cantone, E.G. Omodeo, and P. Ursino. Formative processes with applications to the decision problem in set theory: I. Powerset and singleton operators. Information and Computation, 172(2):165–201, 2002. [11] D. Cantone and P. Ursino. Formative processes with applications to the decision problem in set theory: II. Powerset and singleton operators, finiteness predicate. Inf. Comput., 237: 215–242, 2014. [12] D. Cantone and P. Ursino. An Introduction to the Technique of Formative Processes in Set
Theory. Springer International Publishing, 2018. [13] D. Cantone and P. Ursino. Decidability of the satisfiability problem for Boolean set theory with the unordered Cartesian product operator. arXiv, https://arxiv.org/abs/2106.01224, 2022. [14] D. Cantone and P. Ursino. Decidability of the satisfiability problem for Boolean set theory with the unordered Cartesian product operator. ACM Transactions on Computational Logic, 2023. doi:10.1145/3626823 (just accepted). [15] M. Davis, H. Putnam, and J. Robinson. The decision problem for exponential Diophantine equations. Annals of Mathematics, 74(2): 425–436, 1961. [16] A. Ferro, E.G. Omodeo, and J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. I: Multilevel syllogistic and some extensions. Comm. Pure Appl. Math., 33:599– 608, 1980. [17] D. Hilbert. Mathematical Problems. Bulletin of the American Mathematical Society, 8(10), 437–479, 1902. [18] Yu. V. Matiyasevich. Enumerable sets are Diophantine (in Russian). Dokl. AN SSSR, 191(2), 278–282, 1970. Translated in: Soviet Math. Doklady, 11(2), 354–358. Correction Ibid 11 (6), 1970, vi. Reprinted on pp. 269–273 in: Mathematical logic in the 20th century, G. E. Sacks, (Ed.), Singapore University Press and World Scientific Publishing Co., Singapore and River Edge, NJ, 2003. [19] E.G. Omodeo, D. Cantone, A. Policriti, and J.T. Schwartz. A Computerized Referee. In M.
Schaerf and O. Stock, editors, Reasoning, Action and Interaction in AI Theories and Systems – Essays dedicated to Luigia Carlucci Aiello, vol. 4155 of Lecture Notes in Artificial Intelligence , pp. 117–139. Springer Berlin/Heidelberg, 2006. [20] E.G. Omodeo, A. Policriti, and A. Tomescu. On Sets and Graphs: Perspectives on Logic and Combinatorics. Springer International Publishing, 2017. [21] E.G. Omodeo and J.T. Schwartz. A ‘Theory’ mechanism for a proof-verifier based on firstorder set theory. In A. Kakas and F. Sadri, editors, Computational Logic: Logic Programming and Beyond – Essays in honour of Bob Kowalski, Part II, vol. 2048 of Lecture Notes in Artificial Intelligence, pp. 214–230. Springer-Verlag, Berlin, 2002. [22] E.G. Omodeo, A.I. Tomescu. Set graphs. III. Proof Pearl: Claw-free graphs mirrored into transitive hereditarily finite sets. J. Automat. Reasoning, 2014. 52(1):1–29. [23] F. Parlamento, A. Policriti, and K. P. S. B. Rao. Witnessing diferences without redundancies.
Proceedings of the American Mathematical Society, 125(2):587–594, 1997. [24] J. Robinson, Existential definability in arithmetic, Trans. Amer. Math. Soc. 72 (1952) 437–449. [25] B. Scarpellini. Complexity of subcases of Presburger Arithmetic. Transactions of the
American Mathematical Society, 284(I):93–119, 1984. [26] J.T. Schwartz. Instantiation and decision procedures for certain classes of quantified set-theoretic formulae. ICASE Report, 78-10, 1978. [27] J.T. Schwartz, D. Cantone, and E.G. Omodeo. Computational logic and set theory: Applying formalized logic to analysis. Springer-Verlag, 2011. Foreword by M. Davis.