We recently undertook an investigation aimed at identifying small fragments of set theory (which in most cases are sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satis ability decision tests, potentially useful for automated proof veri cation. Leaving out of consideration the membership relator 2 for the time being, in this note we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators [; \; n, the Boolean relators ; 6 ; =; 6=, and the predicates ` = ?' and `Disj( ; )', meaning `the argument set is empty' and `the arguments are disjoint sets', along with their opposites ` 6= ?' and `:Disj( ; )'.
The decision problem for fragments of set theory, namely the problem of establishing algorithmically for any formula ' in a given fragment whether or not ' is valid in the von Neumann universe of sets, has been thoroughly investigated over the last four decades within the eld of Computable Set Theory. Research has mainly focused on the equivalent satis ability problem, namely the problem of establishing in an e ective manner, for any formula in a given fragment, whether an assignment of sets to its free variables exists that makes the formula true.
The initial goal (back in 1979) envisaged an automated proof veri er based on set theory, within which it would become possible to carry out an extensive formalization of classical mathematics. The inferential kernel of such a proof assistant should have embodied decision procedures intended to capture the `obvious' (deduction steps). Very soon, and long before the proof veri er came into ? We gratefully acknowledge support from \Universita degli Studi di Catania, Piano della Ricerca 2016/2018 Linea di intervento 2" and from the INdAM-GNCS 2019 research project \Logic Programming for early detection of pancreatic cancer". existence, the initial goal sparked a foundational quest aimed at drawing the precise frontier between the decidable and the undecidable in set theory (and also in other important mathematical theories). This inspired much of the subsequent work. Several extensions of the progenitor fragments MLS and MLSS of set theory were proved to have a solvable satis ability problem, which led to a substantial body of results, partly comprised in the monographs [3,5,16,15,8].
We recall that MLS (an acronym for Multi-Level Syllogistic, see [10]) copes
with propositional combinations of literals of the form
x = y [ z;
x = y \ z;
x = y n z;
x 2 y;
(
This is why we recently undertook an investigation aimed at identifying useful `small' fragments of set theory (which in most cases are subfragments of MLS) endowed with polynomial-time decision tests.
In this note we report on results focused, for the time being, on fragments that exclude the membership relator 2.5 We provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides set variables intended to range over the von Neumann universe of all sets (see below), the Boolean operators [; \; n and relators ; 6 ; =; 6=, and the predicates (both a rmed and negated) ` = ?' and `Disj( ; )', expressing respectively that a speci ed set is empty and that two speci ed sets are disjoint.
The paper is organized as follows: Sect. 1 introduces the syntax and semantics of a language in which several hundreds of decidable fragments will be framed in this note; a subsection of it de nes `expressibility', a notion which 4 Note that, thanks to the following equivalences, 6= and 2= are available in MLS and 2 is eliminable from MLSS: x 6= y $ 9 w ( x 2 w ^ y 2= w ) ; y 2= w $ 9 v ( y 2 v ^ w \ v = v n v ) ; x 2 w $ fxg \ w = fxg :
Also note that by adding Cartesian square literals x = y y and cardinality literals jxj = jyj, jxj 6= jyj to MLS, one makes the satis ability problem undecidable [2]. 5 Some preliminary results involving the membership relator 2 will also be reviewed in Appendix B. eases the systematic assessment of the complexities of the satis ability decision tests. A complexity-based classi cation of the fragments under consideration is highlighted in Sect. 2. The paper terminates with a conclusion and some hints for future research, and with two appendices containing, respectively, the proofs of three lemmas on expressibility matters, and a brief overview of the complexity taxonomy for a small fragment involving the membership relator. 1
This section introduces an interpreted language regarding sets, whose acronym BST stands for `Boolean set theory'. The constructs of BST are borrowed from the algebraic theory of Boolean rings (see [12]), but its variables are meant to range over a universe of nested (as opposed to ` at') sets. We dub BST a `theory' simply to emphasize that it has a decidable satis ability problem. Below we will browse a wide range of subproblems of the satis ability problem referring to the whole of BST, and will assess the algorithmic complexity of those subproblems.
We postpone to future reports the treatment of 2, the membership relation. Adding 2 to BST does not disrupt its decidability and truly calls for nested sets. 1.1
The fragments of set theory investigated within the project we are reporting about are parts, syntactically delimited, of a speci c quanti er-free language
BST := BST([; \; n; =?; 6=?; Disj; :Disj; ; 6 ; =; 6=): This is the collection of all conjunctions of literals of the types s = ?; s t; s 6= ?; s 6 t;
Disj(s; t); s = t; :Disj(s; t); s 6= t; where s and t stand for terms assembled from a denumerably in nite supply of set variables x; y; z; : : : by means of the Boolean set operators: union [, intersection \, and set di erence n.
More generally, we shall denote by BST(op1; : : : ; pred1; : : :) the subtheory of BST involving only the set operators op1; : : : (drawn from the set f[; \; ng) and the predicate symbols pred1; : : : (drawn from f=?; 6=?; Disj; :Disj; ; 6 ; =; 6=g). 1.2
For any BST-conjunction ', we shall denote by Vars(') the collection of set variables occurring in '; Vars( ) is de ned likewise, for any BST-term .
A set assignment M is any function sending a collection of set variables V (called the domain of M and denoted dom(M )) into the von Neumann universe V of well-founded sets. We recall that the von Neumann universe (see [13, pp.95{ 102]), aka von Neumann cumulative hierarchy, is built up in stages as the union V := [ 2On V of the levels V := [ < P(V ), with ranging over the class On of all ordinal numbers, where P( ) is the powerset operator.
Natural designation rules attach recursively a value to every term of BST such that Vars( ) dom(M ), for any set assignment M ; here is how: M (s [ t) := M s [ M t;
M (s \ t) := M s \ M t; and
M (s n t) := M s n M t:
M (s = ?) := (true if M s = ; false otherwise,
M (Disj(s; t)) := (true if M s \ M t = ; false otherwise, M (s 6= ?) := :M (s = ?)
M (:Disj(s; t)) := :M (Disj(s; t)) for all literals s = ?, s 6= ?, Disj(s; t), and :Disj(s; t) of BST (and similarly for the literals of BST of the remaining types s t, s 6 t, s = t, and s 6= t), and then, recursively,
M (' ^
) := M ' ^ M when '; are BST-conjunctions, Vars(') dom(M ), and Vars( ) dom(M ).
Given a conjunction ' and a set assignment M such that Vars(') dom(M ), we say that M satis es ', and write M j= ', if M ' = true. When M satis es ', we also say that M is a model of '.
A conjunction ' is said to be satis able if it has some model, else unsatis able.
BST is a sublanguage of MLS, which has an NP-complete satis ability problem [4]; since, in their turn, the fragments of set theory which we shall examine are included in BST, their satis ability problems belong to NP. 1.3
The technique of reduction has been our main tool in the construction of the complexity taxonomy of BST-fragments, which will be presented at length in Sect. 2.
In our case, reductions have been mostly based on the standard notion of `context-free' expressibility:
T of BST, if there exists a T -conjunction (x) is expressible in a fragment (x; y) such that
We also devised a more general notion of `context-sensitive' expressibility, also characterized by its complexity. We named it O(f )-expressibility, where f : N ! N is any mapping intended to bound the complexity of the underlying rewriting procedure.
De nition 2 (O(f )-expressibility). Let T be a fragment of BST and f : N !
N a given mapping. A formula (x) is O(f )-expressible in T if there exists a
mapping
from T into T such that the following conditions are satis ed:
(a) the mapping (
It turns out that standard expressibility is a special case of O(
Lemma 1. If a formula
also O(
(x) is expressible in a fragment T of BST, then it is
Various expressibility and inexpressibility results are collected in the following lemma proved in Appendix A.
Lemma 2. (a) x = y n z is expressible in BST([; Disj; =); (b) x = y \ z and x = y [ z are expressible in BST(n; =); (c) x = y is expressible in BST( ); (d) x y is expressible both in BST([; =) and in BST(\; =); (e) x * y is expressible both in BST([; 6=) and in BST(\; 6=); (f ) x 6= ? is expressible in BST( ; 6=), and therefore in BST([; =; 6=); moreover, x 6= ? is expressible in BST(*), in BST(6=; Disj), in BST(=?; 6=), and in BST(:Disj); (g) x = ? is expressible in BST(Disj); (h) Disj(x; y) is expressible both in BST(\; =?) and in BST(n; =), and :Disj(x; y) is expressible both in BST(\; 6=?) and in BST( ; 6=?); (i) :Disj(x; y) (i.e., x \ y 6= ?) is expressible in BST( ; 6=), and therefore expressible in BST([; =; 6=); (j) x = ? is not expressible in BST([; \; =; 6=); (k) x = y n z is not expressible in BST([; \; =; 6=).
The following lemma, whose proof can be found in Appendix A, allows us to infer that the literal x = ? is O(n)-expressible in BST([; =; 6=). Lemma 3. The mapping '(y) 7! '(y; x) from BST([; =; 6=) into itself, where x is any set variable (possibly in ') and '(y; x) :=
^ z2Vars(') z [ x = z; enjoys the properties - if '(y) ^ '(y; x) is satis able, so is '(y) ^ x = ?, and - j= '(y) ^ x = ? ! '(y; x).
Hence, the literal x = ? is O(n)-expressible by '(y; x) in BST([; =; 6=). ? ? * ? ?
Of a fragment of BST, we say that it is NP-complete if it has an NP-complete satis ability problem (see [11]). Likewise, we say that it is polynomial if its satis ability problem has polynomial complexity.
The number of distinct fragments of BST is equal to 23 (28 1) = 2040, of which 1278 are NP-complete and the remaining 762 are polynomial. The complexity of any fragment of BST can be e ciently identi ed once the minimal NP-complete fragments (namely the NP-complete fragments of BST that do not strictly contain any NP-complete fragment of BST) and the maximal polynomial fragments (namely the polynomial fragments of BST that are not strictly contained in any polynomial fragment of BST) have been singled out. Indeed, any BST-fragment either is contained in some maximal polynomial BST-fragment or contains some minimal NP-complete fragment. rst block: the NP-completeness of the fragments BST(n; *), BST(n; :Disj), and BST(n; 6=?) in the rst block of Table 1 can be obtained by much the same technique used to reduce 3SAT to BST(n; 6=); second block: the NP-completeness of the fragment BST([; \; *) can be achieved by much the same technique used to reduce 3SAT to BST([; \; 6=); third block: the NP-completeness of the fragments BST([; \; Disj; :Disj), BST([; \; =?; :Disj), and BST([; \; 6=?; Disj) can be obtained by much the same technique used to reduce 3SAT to BST([; \; =?; 6=?); and fourth block: the NP-completeness of the fragment BST([; =; 6=?; Disj) can be shown by much the same reduction technique used for BST([; =; Disj; :Disj). Finally, by resorting to some of the expressibility results listed in Lemma 2, it can readily be proved that: - BST([; =; Disj; :Disj) can be reduced in linear time
to BST([; ; Disj; :Disj), by Lemma 2(c), - BST([; =; 6=?; Disj) can be reduced in linear time to BST([; =; 6=; Disj), by Lemma 2(f), to BST([; =; *; Disj), by Lemma 2(f), to BST([; ; 6=?; Disj), by Lemma 2(c), to BST([; ; 6=; Disj), by Lemma 2(c)(f), to BST([; ; *; Disj), by Lemma 2(c)(f). 2.2
Two of the maximal polynomial fragments of BST, namely
BST([; \; n; =?; Disj; ; =) and
BST([; \; =; 6=?; :Disj; )
are trivial as they contain only satis able conjunctions, thereby admitting a O(
Notice that the rst fragment comprises all the positive relators and the complete suite of Boolean operators. It is immediate to check that each of its Since
conjunctions ' is satis ed by the null set assignment M; over Vars('), where M x = ; for each x 2 Vars(').
;
Concerning the second fragment, it can easily be veri ed that each of its conjunctions is satis ed by any constant nonnull set assignment Ma over Vars( ), where a is a nonempty set and Max = a for every x 2 Vars( ).
Next, we provided O(n3) satis ability BST([; Disj; :Disj; 6=) and BST([; =; 6=), and a for the fragment BST(\; =?; =; 6=). tests for the fragments
O(n4) satis ability test - j= x * y - j= x = ? ! x [ y 6= y (cf. Lemma 2(e)) and ! Disj(x; x) (cf. Lemma 2(f),(g)), the O(n3) satis ability test for BST([; Disj; :Disj; 6=) yields a O(n3) satis ability test for BST([; =?; 6=?; Disj; :Disj; *; 6=).
- x 6= ? is expressible in BST(=?; 6=) (cf. Lemma 2(f)), - Disj(x; y) and :Disj(x; y) are expressible in BST(\; = ?; 6=
Lemma 2(h)), and - x y and x * y are expressible in BST(\; =?; 6=?) (cf. Lemma 2(d),(e)), ?) (cf. it follows that the O(n4) satis ability test for BST(\; =?; =; 6=) yields a O(n4) satis ability test for the fragment BST(\; =?; 6=?; Disj; :Disj; ; *; =; 6=).
Finally, since - x = ? is O(n)-expressible in BST([; =; 6=) (cf. Lemma 3), - x 6= ? is expressible in BST(=?; 6=) (cf. Lemma 2(f)), - x y is expressible in BST([; =), - x * y is expressible in BST([; 6=), and - :Disj(x; y) is expressible in BST(6=?; ), the O(n3) satis ability test for BST([; =; 6=) yields a O(n3) satis ability test for the fragment BST([; =?; 6=?; :Disj; ; *; =; 6=).
(A) none of the fragments listed in Table 1 is strictly contained in another fragment in the same table, and (B) for every fragment T of BST, there is a fragment in Table 1 that either contains T or is contained in T .
Properties (A) and (B) imply that the 18 NP-complete fragments in Table 1 are indeed minimally NP-complete and, symmetrically, the 5 polynomial fragments in Table 1 are maximally polynomial. While there is a limited interest in further investigating the non-minimal NPcomplete fragments of BST, this is not the case for the non-maximal polynomial fragments, as the latter can admit decision tests more e cient than any of the maximal polynomial fragments extending them.
We brie y report here some preliminary results obtained so far in this direction (see Table 2). In particular, we devised: - a linear-time decision test for the fragment BST([; Disj; 6=), which readily generalizes, by Lemma 2(e),(f),(g), to a linear-time satis ability test for the extended fragment BST([; =?; 6=?; Disj; *; 6=); - a cubic algorithm for the fragment BST(\; = ?; 6=), which yields, by Lemma 2(f),(h), a cubic satis ability test for the extended fragment BST(\; =?; 6=?; Disj; 6=).
For space reasons, we limit ourselves to present only a linear-time satis ability test for the fragment BST([; Disj; 6=).
For convenience, we shall represent terms of the form x1 [ [ xh as [fx1; : : : ; xhg. Thus, for a set assignment M and a nite nonempty collection of set variables L Vars('), we shall have M ([L) = [M L = Sx2L M x.
Towards a linear satis ability test for BST([; Disj; 6=), let ' be a satis able BST([; Disj; 6=)-conjunction of the form p q ^ ^ [Li 6= [Ri ^
Disj([Lj ; [Rj ); i=1 j=p+1 where the Lh's and the Rh's are nonempty collections of set variables, and let M be a set assignment over Vars(') satisfying '.
Preliminarily, we observe that, for each x 2 Sjq=p+1([Lj \ [Rj ), M x M ([Lj ) \ M ([Rj ) holds for some j 2 fp + 1; : : : ; qg. Hence, since the conjunct Disj([Lj ; [Rj ) occurs in ', we have M ([Lj ) \ M ([Rj ) = ;, which in turn yields M x = ;.
Next, for each conjunct of type [Li 6= [Ri in ', if any, we have M ([Li) 6=
M ([Ri), i.e., M ([Li) [ M ([Ri) n M ([Li) \ M ([Ri) 6= ;, and a fortiori
M ([Li) [ M ([Ri) 6= ;. Thus, there is an x 2 [Li [ [Ri such that M x 6= ;,
and therefore the preceding observaton implies ([Li [ [Ri) n Sjq=p+1([Lj \
[Rj ) 6= ;. Summarizing, we have shown that, by assuming the satis ability of
', then the following condition is ful lled:
(
Sq (C1) ([Li [ [Ri) n j=p+1([Lj \ [Rj ) 6= ;, for every i = 1; : : : ; p.
Conversely, let ' be a BST([; Disj; 6=)-conjunction of the form (
j=p+1([Lj \ [Rj ), and - M x1; : : : ; M xk are nonempty pairwise disjoint sets.
Then, it is not hard to check that M satis es '. Thus, we have proved the
following lemma, which readily yields a satis ability test for BST([; Disj; 6=).
Lemma 4. Let ' be a BST([; Disj; 6=)-conjunction of the form (
Concerning the complexity of the satis ability test implicit in Lemma 4, we observe that condition (C1) can be tested in O(j'j) time, since - the set Sjq=p+1([Lj \ [Rj ) can be computed in O Pjq=p+1(jLj j + jRj j) =
O(j'j) time; - the set ([Li [[Ri)nSjq=p+1([Lj \[Rj ) can be computed in O(jLij+jRij) time and tested for emptiness in constant time, for each i = 1m; : : : ; p, for an overall O Pip=1(jLij + jRij + 1) = O(j'j) time.
Lemma 5. The satis ability problem for BST([; Disj; 6=)-conjunctions can be solved in linear time. 3
We highlighted some preliminary results of an investigation aimed at identifying small fragments of set theory endowed with polynomial-time satis ability decision tests, potentially useful for automated proof veri cation. In this initial phase, we mainly focused on `Boolean Set Theory', namely the fragment of quanti er-free formulae of set theory involving variables, the Boolean set operators [; \; n, the Boolean relators ; 6 ; =; 6=, and the predicates ` = ?' and `Disj( ; )', along with their opposites.
Future work will concentrate on the analysis of the sub-maximal polynomial
fragments of BST, so as to obtain a ner complexity taxonomy of the collection
of all BST fragments, and also on enriching the endowment of set operators
and relators of BST. We also plan to further deepen the study of membership
fragments of the types presented in Appendix B and, ultimately, to explore the
cases in which relators correlated to membership and Boolean set predicates are
allowed simultaneously.
Proof of Lemma 1. Let (x) be any formula expressible in T , and let (x; z)
be a T -conjunction such that
! (9z) (x; z) :
(
Let M be any set assignment such that M j= ?(x; y), and set M 0z := M z [ C, for every z 2 Vars( ?), where C is any nonempty set that is disjoint from M z, for every z 2 Vars( ?) (namely, such that C \ [M (Vars( ?)) = ;). Then, for y1; : : : ; yn 2 Vars( ?), we have:
M 0(y1 [ : : : [ yn) = M 0y1 [ : : : [ M 0yn and
M 0(y1 \ : : : \ yn) = M 0y1 \ : : : \ M 0yn = (M y1 [ C) [ : : : [ (M yn [ C) = (M y1 [ : : : [ M yn) [ C = M (y1 [ : : : [ yn) [ C = (M y1 [ C) \ : : : \ (M yn [ C) = (M y1 \ : : : \ M yn) [ C = M (y1 \ : : : \ yn) [ C: (j1) if the literal y1 [ : : : [ yn = z1 [ : : : [ zm is in ?, then
M 0(y1 [ : : : [ yn) = M (y1 [ : : : [ yn) [ C (j2) if the literal y1 \ : : : \ yn = z1 \ : : : \ zm is in ?, then M 0(y1 \ : : : \ yn) = M (y1 \ : : : \ yn) [ C = M (z1 [ : : : [ zm) [ C = M 0(z1 [ : : : [ zm); = M (z1 \ : : : \ zm) [ C = M 0(z1 \ : : : \ zm); (j3) if the literal y 6= z is in
?, then we have M 0y = M y [ C;
M 0z = M z [ C; and
M y 6= M z:
Since C is disjoint from M y and M z, then M 0y 6= M 0z.
From (j1), (j2), and (j3), it follows that M 0 j= ?, so that we have also M 0 j= (9y) ?.
In addition, we have M 0x = M x [ C 6= ;. Thus, M 0 6j= (9y) ? !
x = ?, contradicting (
j= x = y n y
! (9w) (x; y; y; w): j= x = y n y ! (9w) (x;y;y;w) =) j= x = ? ! (9w) (x;y;y;w) =) j= (8y) x = ? ! (9w) (x;y;y;w) =) j= (8y) (9w) (x;y;y;w) ! x = ?
^ x = ? ! (9w) (x;y;y;w) =) j= (8y)((9w) (x;y;y;w) ! x = ?)
^ (8y) x = ? ! (9w) (x;y;y;w) =) j= (8y):(9w) (x;y;y;w) _ x = ?
^ x = ? ! (8y)(9w) (x;y;y;w) =) j= :(9w)(9y) (x;y;y;w) _ x = ?
^ x = ? ! (9w)(9y) (x;y;y;w) =) j= (9w)(9y) (x;y;y;w) ! x = ?
^ x = ? ! (9w)(9y) (x;y;y;w) =) j= x = ? ! (9w)(9y) (x;y;y;w); then
j= x = ? ! (9w)(9y) (x;y;y;w); i.e., x = ? would be expressible in BST([;\;=;6=), contradicting (j). Thus, x = y n z is not expressible in BST([;\;=;6=).
j= ' ^ ^ z [ x = z:
z2Vars(') Then ' has a model M such that Mx = ;.
We state without proof the following model-theoretic property for the fragment BST([;=;6=).
Proposition 1. Let ' be a satis able conjunction of BST([;=;6=) and x any variable such that '(y;x) := ^ z [ x = z:
z2Vars(') Plainly, j= x = ? ! Vz2Vars(') z [ x = z. Hence, a fortiori, Proof of Lemma 3. Let ' 7! '(y;x) be the mapping from BST([;=;6=) into itself where j= ('(y) ^ x = ?) ! ^ z [ x = z; z2Vars(')
B
In this appendix we present a quick overview of the complexity taxonomy for the fragment Th([; \; n; 2; 2=), which from now on we refer to as MST, acronym for membership set theory.
The number of distinct fragments of MST is 24, of which 10 are NP-complete and 14 are polynomial. Much as for BST, the complexity of any fragment of MST can be e ciently determined once the minimal NP-complete fragments and the maximal polynomial fragments have been singled out. Table 3 shows the minimal NP-complete and the maximal polynomial fragments of MST.
?
? ? ?
The maximal polynomial fragment MST([; \; n; 2=) is trivial as it contains
only satis able conjunctions, thereby admitting a O(
Indeed, every MST([; \; n; 2=)-conjunction ' is satis ed by the null set assignment M;, sending each x 2 Vars(') to ;.
We provided a O(n) satis ability test for the fragment MST([; 2). Then we managed to translate any MST([; 2; 2=)-conjunction into an equisatis able MST([; 2)-conjunction in O(n) time, which resulted in a O(n) satis ability test for MST([; 2; 2=).
We also provided a O(n2)-time satis ability test for the fragment MST(\; 2), which was extended into a satis ability test for the fragment MST(\; 2; 2=) that retains the same complexity.
Finally, the fragments MST([; \; 2) and MST(n; 2) were proved to be NPcomplete. We remark that using the axiom of regularity was necessary to prove the NP-completeness of the former fragment, while regularity was not needed to prove the NP-completeness of the latter.