A translation is proposed of conjunctions of literals of the forms x = y n z, x 6= y n z, and x 2 y, where x; y; z stand for variables ranging over the von Neumann universe of sets, into unquanti ed Boolean formulae of a rather simple conjunctive normal form. The formulae in the target language involve variables ranging over a Boolean eld of sets, along with a di erence operator and relators designating equality, nondisjointness and inclusion. Moreover, the result of each translation is a conjunction of literals of the forms x = y n z, x 6= y n z and of implications whose antecedents are isolated literals and whose consequents are either inclusions (strict or non-strict) between variables, or equalities between variables. Besides re ecting a simple and natural semantics, which ensures satis ability-preservation, the proposed translation has quadratic algorithmic time-complexity, and bridges two languages both of which are known to have an NP-complete satis ability problem.
The Flatland of sets [
An apt theoretical framework for the study of at sets is the theory of Boolean rings, a merely equational rst-order theory endowed with nitely many axioms|at times, one blends this theory with an arithmetic of cardinals. Frameworks for the study of nested sets are such all-embracing theories as ZF and NBG (the Zermelo-Fraenkel and von Neumann-Bernays-Godel theories), within which one can cast the entire corpus of mathematical disciplines.
Boolean algebra is decidable in its entirety (cf. [5, Sec. 3.7]); ZF is essentially
undecidable, nonetheless an e ort to nd decision algorithms for fragments of
it began in 1979, the purpose of this long-standing research being an e ective
implementation of specialized inference rules within a programmed system apt to
verifying the correctness of large-scale mathematical proofs [
A priori, one would expect the distance between the performances of decision algorithms for fragments of Boolean algebra, and of the seemingly much more expressive languages whose dictionaries embody nested membership, to be abysmal. Luckily, though, as we will see, this is not the case.
||||
We introduce in Sec. 1 an interpreted formal language, dubbed BST, within
which one can formulate unquanti ed Boolean constraints. Despite its syntax
being quite minimal|BST only encompasses conjunctions of primitive literals
of two forms, namely x = y n z and x 6= y n z |, the satis ability problem for
BST is NP-complete (see [
According to our semantics, the domain of discourse to which BST refers is a universe of nested sets; however, as will be seen in Sec. 2, every satis able propositional combination of BST literals (as a special case, a conjunctive BST constraint) admits a model consisting of sets which are, in a certain sense, \ at". This makes it evident that membership cannot be plainly expressed in BST. To detour this limitation, we propose in Sec. 1.2 a novel notion of expressibility, also embodying an obligation to supply an algorithmic-complexity assessment. This roundabout notion is, we believe, a valuable contribution of this paper.
In terms of the novel notion of expressibility, in Sec. 3 we will manage to
translate a conjunction of literals of the three forms x = y n z, x 6= y n z, and
x 2 y, into a propositional combination of BST literals. The proposed translation
is, of course, satis ability preserving. It leads to a conjunction some of whose
conjuncts are BST literals, while other conjuncts are rather simple disjunctions.
The algorithmic time-complexity of our translation is quadratic, which indirectly
shows that the satis ability problem remains NP-complete when the relator 2
is added to the constructs of BST: this NP-completeness result was known (see,
e.g., [
The material treated in this paper bridges, in a sense, the topics treated in
[
Boolean Set Theory (BST) is the quanti er-free theory composed by all conjunctions of literals of the following two types: x = y n z; x 6= y n z; (1) where x; y, and z are set variables assumed to range over the universe of the well-founded sets.
Semantics for the theory BST is de ned in terms of set assignments. Specifically, given a ( nite) collection V of set variables, a set assignment M over V |the variable-domain of M , denoted by dom(M )|is any map from V into the von Neumann universe V (see below).4 A set assignment M satis es a given literal x = y n z, with x; y; z 2 dom(M ), if M x = M y n M z holds, where M y n M z is the standard set di erence between M y and M z. Likewise, M satis es the literal x 6= y n z if M x 6= M y n M z holds. Finally, M satis es a BST-conjunction ' such that Vars(') dom(M ) (where Vars(') denotes the collection of the variables occurring free in ') if it satis es all of the conjuncts of ', in which case we say that M is a model of ' and write M j= '. A BST-conjunction is said to be satis able if it has some model, otherwise it is said to be unsatis able.
In [
We shall also be interested in the extension BST+ of the theory BST consisting of all propositional combinations (resulting from unrestrained use of the logical connectives ^,_, !, !,:) of atomic formulae of type x = y n z. It is not hard to check that the satis ability problem for BST+ can be reduced to the satis ability problem for BST in nondeterministic polynomial time, and therefore it is NP-complete in its turn. 1.1
The von Neumann universe We recall that the von Neumann universe V of (well-founded) sets, also dubbed von Neumann cumulative hierarchy, is built up through a trans nite sequence of 4 Notice that we are not basing our semantics of BST on at sets of urelements (as would be doable, as recalled in the Introduction). Doing so would call for minor adjustments, unjusti ed|and perhaps disturbing|in the economy of this paper. steps as the union V := S 2On V of the levels V := S < P(V ), with P( ) denoting the powerset operator and ranging over the class On of all ordinals.
Based on the level of rst appearance in the von Neumann hierarchy, one can de ne the rank of any set s, denoted rk (s). Speci cally, rk (s) is the ordinal such that s 2 V +1 n V . Hence, for every 2 On, the set V +1 n V , hereinafter denoted V#, collects all sets whose rank equals .
The following lower bound on the number of well-founded sets of any positive integer rank n, to be proved as Proposition 2 in Appendix A.1, will be useful:
Vn# > 2n 1:
Some handy properties of the rank function which we shall tacitly use are the following: for all sets s; t 2 V, we have: rk (s) = if s 2 t then rk (s) < rk (t), if s t then rk (s) 6 rk (t), (0
if s = ; supu2s(rk (u) + 1) otherwise.
We also recall that well-foundedness, as enforced by the regularity or foundation axiom of Zermelo-Fraenkel set theory, precludes the formation of in nite descending membership chains of the form and in particular of membership cycles for any sequence s0; s1; s2; : : : of sets.
2 s2 2 s1 2 s0;
Formally, existential expressibility is de ned as follows (cf. [
De nition 1 (Existential expressibility). A formula (x) is said to be existentially expressible in a theory T if there exists a T -formula ( x; z ) such that j= ( x )
! ( 9z ) ( x; z ); where x and z stand for tuples of set variables.
Existential expressibility has been generalized in [
Here we slightly generalize O(f )-expressibility so that it copes with
collections C of formulae, rather than with single formulae as its original de nition
did; another di erence lies in the fact that the generalized notion has to do with
a source theory T1 and a target theory T2, whereas [
De nition 2 (O(f )-expressibility). Let T1 and T2 be any theories and f : N ! N be a given map. A collection C of formulae is said to be O(f )-expressible from T1 into T2 if there exists a map from T1 C into T2, where no variable in z occurs in either x or y, such that the following conditions are satis ed: (a) the mapping (3) can be computed in O f (j' ^ j) -time, (b) if '( y ) ^ ' ( x; y; z ) is satis able, so is '( y ) ^ ( x ), (c) j= '( y ) ^ ( x ) ! ( 9z ) ' ( x; y; z ).
The main results in this paper are that membership atoms x 2 y are not existentially expressible in BST+, whereas any conjunction of membership atoms is O(n2)-expressible from BST into BST+. 2
Non-existential expressibility in BST+ of x 2 y In this section we show that membership atoms are not existentially expressible in BST+. Speci cally, we prove that every satis able BST+-formula admits a \ at" model M , namely a model whose union Sx2Vars( ) M x of values is made up of members all of the same positive rank. We deduce from this fact that M x 2= M y, for all x; y 2 Vars( ), namely that M 6j= x 2 y.
De nition 3. For every ordinal > 1, a set assignment M over a collection V of variables is said to be - at if all sets in the domain SfM x j x 2 V g of M have rank .
No membership atom x 2 y is satis ed by any - at set assignment: Lemma 1. Let M be a - at set assignment over a collection V of variables. Then M x 2= M y, for all x; y 2 V .
Proof. Because of the - atness of M , for every x 2 V either rk (M x) = 0 (when M x = ;) or rk (M x) = + 1 (when M x 6= ;). Hence, in any case rk (M x) 6= (since by de nition > 1), and therefore M x 2= SfM y j y 2 V g.
A satis able BST+-formula always admits a - at model, for su ciently large . This is proved in the next lemma.
Lemma 2. Every satis able formula every > jVars( )j + 1.
Proof. Let be a satis able formula of BST+, and let M be a set model for . Let +M be the conjunction of all the distinct atoms x = y n z occurring in that are satis ed by M . Likewise, let M be the conjunction of all the distinct literals x 6= y n z such that x = y n z occurs in and M 6j= x = y n z. Finally, let of BST+ admits a - at set model, for M := + M ^
M : (4) Plainly, M satis es M by construction. Additionally, by propositional reasoning, every set model for M satis es our initial formula . Thus, it is enough to show that the conjunction M admits a - at set model for every > n + 1, where n := jVars( M )j = jVars( )j.
We prove that M admits a - at set model by contracting each nonempty region RW of M of the form
RW := \fM x j x 2 W g [ [fM y j y 2 Vars( M ) n W g; for ; =6 W Vars( M ), into a distinct singleton of rank a single member of rank ).
Since the map x 7! 2x > n + 1 we have x is strictly increasing for x > 1, for every integer + 1 (hence containing jV#j = jV +1j jV j = 2jV j jV j > 2jVn+1j jVn+1j = jVn+2j jVn+1j = jVn#+1j > 2n; where the latter inequality follows from Proposition 2 (see Appendix A.1). Hence, there exists an injective map = : P(Vars( M )) ! V# from the collection of the nonempty subsets of Vars( M ) into the family V# of the (hereditarily nite) sets of rank .
Next, we de ne a set assignment M over Vars( M ) by putting
M x := f= (W ) j ; 6= W
Vars( M ) ^ RW 6= ;g: By construction, the assignment M is - at. In addition, it is not hard to check that, for every ; 6= W Vars( M ), the region RW of M de ned by
RW := \fM x j x 2 W g [ [fM y j y 2 Vars( M ) n W g is nonempty if and only if so is its corresponding region RW of M . Thus, M satis es M .
We are now ready to prove that membership atoms x 2 y are not existentially expressible in BST+.
Theorem 1. The atom x 2 y is not existentially expressible in BST+. Proof. By way of contradiction, let us assume that x 2 y is existentially expressible by a formula (x; y; z) involving only atoms of type x0 = y0 n z0. Hence, would hold.
Since x 2 y is trivially satis able, by (5) so would be (9z) (x; y; z) and therefore (x; y; z) would be satis able too. Thus, by Lemma 2, (x; y; z) would be satis ed by a - at set assignment M for some > 1, and therefore, by Lemma 1, M x 2= M y. Hence, M j= (9z) (x; y; z) ^ x 2= y, so that M 6j= (9z) (x; y; z) ! x 2 y, contradicting (5).
O(n2)-expressibility in BST+ of membership conjunctions Conforming with De nition 2, we shall prove that any membership conjunction ( x ) is O(n2)-expressible from BST into BST+ by exhibiting a map with '( y ) in BST, which can be computed in quadratic time and such that conditions (b) and (c) of De nition 2 are satis ed, where '( y ) ranges over the collection of BST-conjunctions and the variables in z are distinct from those in x and in y.
Thus, let '( y ) be any BST-conjunction and ( x ) be any conjunction of membership atoms. We let Left ( ) denote the collection of all the set variables x occurring in some membership atom x 2 y in , for some variable y.
For each variable x 2 Left ( ), we introduce a new distinct variable x (which is intended to represent the singleton fxg), and denote by x their collection. In addition, for each x 2 Vars(' ^ ) we introduce a new distinct variable xe, and denote by xe their collection (these variables will enforce that x 2 y only if xe ( ye). Then we put: ' ( x; y; x; xe ) := (x 6= ? ^ x y) ^ (thus, the list of variables z in De nition 2 results from the concatenation of the lists x and xe).
Plainly, ' is a BST+-formula5, which satis es the following proposition, implying condition (a) of Def. 2: Lemma 3.
' = jVars(' ^
)j2 .
The proof of this lemma is delayed to Sec. 3.3.
In the following subsections, we shall prove that if '( y ) ^ ' ( x; y; x; xe ) is satis able, then so is '( y ) ^ every model of '( y ) ^ ( x ) can be extended to a model of ( x ), and ' ( x; y; x; xe ), thus showing that also conditions (b) and (c) of De nition 2 are ful lled, and therefore proving that every membership conjunction is O(n2)-expressible from BST into BST+.
Translation examples Here we digress to provide a few examples illustrating how the conjunction renders the formula ' ^ . ' Example 1. The simple conjunction ' ^ gets translated into where ' := x = y n z and := z 2 y, ' := z 6= ; ^ z y ^ (:Disj(z; x) ! z
x) ^ (:Disj(z; y) (z x This shows that any relation M s 2 M t, respectively M s 2= M w, where M is a model for ' ^ ^ ' , gets translated into M s M t ^ M s~ ( M t~, resp. into Disj(s; w).
In fact, to the literal z 2 y there corresponds the conjunct z y, so that from z y ! z~ ( y~ we also get M z~ ( M y~. Furthermore M z 2= M z must hold, and in fact we can derive Disj(z; z) from (z z ! z~ ( z~) ^ (:Disj(z; z) ! z z). Then we can get M z 2 M x from ' ^ , since M x = M y n M z and M z 2= M z; we can, analogously, get M z M x from ' ^ ' : indeed, it follows from x = y n z, z y, and from the condition Disj(M z; M z) just obtained; lastly, from z x ! z~ ( x~, we get M z~ ( M x~.
In the previous example we saw that the conjunct z z, that in our translation would be the equivalent of the unsatis able z 2 z, does not appear in ' . More generally, the usage of the set variables x~ in ' allows us to detect any membership cycle x 2 2 x that might be derived from ' ^ . In the following we exemplify this property: 5 In fact, ' is a conjunction of a rather simple form.
Example 2. The conjunction ' ^
, where ' := a = b n c and
:= x 2 y ^ y 2 z ^ z 2 x; is plainly unsatis able due to the cycle x 2 y 2 z 2 x. To re ect this, comprises the literals ' x y z y ^ (x z ^ (y x ^ (z y z x ! x~ ( y~) ^ ! y~ ( z~) ^ ! z~ ( x~); therefore it is unsatis able due to the cycle x~ ( y~ ( z~ ( x~.
Our next example shows how the unsatis ability proofs for the conjunction ' ^ and ' ^ ' mimic each other, especially bearing in mind that M x 2 M y gets translated into M x M y ^ M x~ ( M y~, and M x 2= M z into Disj(M x; M z). Example 3. The conjunction ' ^ , where ' := x = y n z and := z 2 x ^ x 2 y; is unsatis able since if a model M for it existed, then we would have M x 2 M x. Indeed: from z 2 x we obtain M x 2= M z, then from x = y n z and x 2 y we obtain M x 2 M x. This will be re ected by ' ^ ' as M x~ ( M x~, which in its turn implies that also ' ^ ' is unsatis able, where ' := x 6= ; ^ x y ^ z 6= ; ^ z
x ^ (x (z (x = z z y ! z~ ( y~) ^ (z ! x~ = z~): (:Disj(x; x) (:Disj(x; z) ! x ! x x) ^ (:Disj(x; y) ! x
y) ^ z) ^ (:Disj(z; x) ! z x) ^ (:Disj(z; y) (:Disj(x; z) (x x ! x~ ( x~) ^ (x ! z ! x = z) ^ (x = z
y y) ^ (:Disj(z; z)
! z ! x = z) ^ ! x~ ( y~) ^
z) ^ ! x~ ( z~) ^ (z x
! z~ ( x~) ^ z
! z~ ( z~) ^
Above, in proving the unsatis ability of ' ^ , our rst step has been to get M x 2= M z; here, by assuming M j= ' ^ ' , we rst get Disj(M x; M z): indeed, from z x and z x ! z~ ( x~ we obtain M z~ ( M x~, then from x z ! x~ ( z~ and :Disj(x; z) ! x z we obtain Disj(M x; M z). The second step, above, has been to get M x 2 M x; here we will get M x~ ( M x~: indeed, from x y and x = y n z, and from the disjointness clause just proved, it follows that M x M x; and, nally, from x x ! x~ ( x~ we obtain M x~ ( M x~, which leads to the unsatis ability of ' ^ ' . 3.1
If ' ^
' is satis able, then so is ' ^ Assume that ' ^ ' is satis able. Hence, by Lemma 2, ' ^ ' is satis ed by some - at set assignment M such that > Vars(' ^ ' ) + 1. Since there can be no (-cycle in fM xe j x 2 Vars(' ^ )g, we can nd some ordering Vars(' ^ ) such that
M xe ( M y e ! x y; for x; y 2 Vars(' ^ ).
Following the ordering , de ne recursively, for x 2 Vars(' ^ ), where
M 0x := M x [ M +x; M +x := fM 0w j M w
M x ^ w 2 Left ( )g:
In preparation for the proof that M 0 models ' ^ , we need a few lemmas. We begin by proving that no rk (M 0x) equals , for any x 2 Vars(' ^ ): Lemma 4. For every x 2 Vars(' ^ ), rk (M 0x) 6= .
Proof. If M x 6= ;, then rk (M 0x) > rk (M x) = + 1, so rk (M 0x) 6= . On the other hand, if M x = ;, then M +x = fM 0w j M w M x ^ w 2 Left ( )g = ;, since M j= w 6= ;, for all w 2 Left ( ). Hence, M 0x = ;, so that rk (M 0x) = 0 6= .
An immediate consequence of the preceding claim is: Corollary 1. For all x; y 2 Vars(' ^ ),
M x \ M +y = ;; Proof. It is enough to observe that, for x; y 2 Vars(' ^ ), when M x 6= ;, all members of M x have rank , whereas by Lemma 4 no member of M +y can have rank .
Next we prove three lemmas which will enable us to conclude that M 0 models ' and as wanted; the second of these relies on Proposition 3, whose statement and proof are delayed till Appendix A.2.
Lemma 5. For all w; w0 2 Left ( ),
M w = M w0 () M w = M w0.
Proof. Let w; w0 2 Left ( ). By construction, the formula ' contains the following conjuncts, which are all satis ed by the set assignment M : { w = w0 { w 6= ;, { :Disj(w; w0) ! w = w0,
! w = w0.
Thus, in view of M j= w = w0 ! w = w0, if M w = M w0 then we have M w = M w0.
Conversely, if M w = M w0 then from M j= w 6= ; we get M j= :Disj(w; w0). Hence, from M j= :Disj(w; w0) ! w = w0, we get M w = M w0. on (6) (7) (8) Lemma 6. For all x; y 2 Vars(' ^ ),
M x = M y () M 0x = M 0y: Proof. If M x = M y, then by (7) we have M +x = M +y. Thus,
M 0x = M x [ M +x = M y [ M +y = M 0y: Conversely, if M 0x = M 0y, then by (7) again we have M x[M +x = M y[M +y, so that Corollary 1 and Proposition 3(b) (see Appendix A.2) yield M x = M y.
Another useful consequence of de nitions (6) and (7) is the following result. Lemma 7. For w 2 Left ( ) and x 2 Vars(' ^ equivalent: ), the following statements are (a) M 0w 2 M +x, (b) M w M x, and (c) M w \ M x 6= ;.
Proof. The implication (b) =) (a) follows readily from the de nition (7) of M +.
Concerning the implication (a) =) (c), let us assume that M 0w 2 M +x, for some w 2 Left ( ) and x 2 Vars(' ^ ). Then, by (7), there must exist a w0 2 Left ( ) such that (i) M 0w = M 0w0 and (ii) M w0 M x. By (i) and Lemma 6, we have M w = M w0, which in turn by Lemma 5 implies M w = M w0. Hence, by (ii), M w M x. Next, since w 6= ; is in ', we have M w 6= ;, so that the inclusion M w M x yields M w \ M x 6= ;.
Finally, the implication (c) =) (a) follows at once from (7), since ' contains the conjunct :Disj(w; x) ! w x.
We have now reached the salient conclusion yielded by the de nition of M 0 and by the preparatory proofs carried out so far: Lemma 8. The set assignment M 0 satis es the conjunction ' ^ .
Proof. We shall prove that M 0 satis es (a) all literals in of type x 2 y, (b) all literals in ' of type x = y n z, (c) all literals in ' of type x 6= y n z. in M +y
Concerning (a), let x 2 y be a conjunct in . Then the literal x y occurs ' , so that M x M y holds, and therefore by (7) and (6) we have M 0x 2
M 0y. Hence, M 0 j= x 2 y.
Concerning (b), let x = y n z be in '. Recalling that M j= ', we have M x = M y n M z. Hence, by (6), Corollary 1, and Proposition 3(a), in order to show that M 0 satis es the literal x = y n z it is enough to prove that M +x = M +y n M +z holds, which we do next.
If M 0w 2 M +x, for some w 2 Left ( ) such that M w M x, then M w M y nM z, so that M w M y and M w \ M z = ;. By Lemma 7, M w M y yields M 0w 2 M +y and M w \M z = ; implies M 0w 2= M 0z. Thus, M 0w 2 M +y nM +z. By the arbitrariness of w 2 Left ( ), we get
M +x
M +y n M +z: (9) Conversely, if M 0w 2 M +ynM +z for some w 2 Left ( ), then, again by Lemma 7, we have M w M y and M w \ M z = ;. Hence, M w M y n M z = M x, so that by another application of Lemma 7 we get M 0w 2 M +x. The arbitrariness of w 2 Left ( ) yields M +y n M +z M +x. Together with (9), the latter inclusion implies M +x = M +y n M +z, completing the proof of (b).
Finally, concerning (c), let x 6= y n z be in '. Then we have M x 6= M y n M z, so that by Proposition 3(a) we readily obtain M 0x 6= M 0y [ M 0z. Plainly, the graph GM is acyclic. For, should GM contain a cycle (xi0 ; xi1 ; : : : ; xik ; xi0 ), then we would have the membership cycle M xi0 2 M xi1 2 2 M xik 2 M xi0 , contradicting the axiom of foundation.
Hence, we can de ne the following notion of height h : V ! N by putting h(x) := length of the longest path in GM leading to x, for every x 2 V (in particular, h(x) = 0 whenever x has no predecessors in GM ).
Next let x1; x2; :::; xn be any indexing of the variables in Vars(' ^ ) complying with the height h, namely such that h(xi) < h(xj) =) i < j: We are now ready to de ne an extension M over Vars( ' ) n Vars(' ^ ) of the set assignment M which satis es ' . For x 2 Vars(' ^ ), we put of course M x := M x. Then, for x 2 Left ( ), we set M x := fM xg. Finally, we put M xe1 := f1g and recursively, for i = 1; : : : ; n 1,
M xei+1 := (M xi
e M xei [ fi + 1g if h(xi+1) = h(xi) ; otherwise:
From the de nition of M , it follows that, for i; j 2 f1; : : : ; ng: (H1) h(xi) < h(xj) =) M xei ( M xj, and
e (H2) h(xi) = h(xj) =) M xi = M xj.
e e
Next, we prove that M satis es ' .
Lemma 9. The set assignment M satis es
Proof. Let x 2 y occur in . By construction, M x = fM xg. In addition, since M j= x 2 y, we have M x 2 M y = M y, so that M x M y. Thus, by the arbitrariness of x 2 y in , we have
M j= ^ (x 6= ? ^ x
y):
Next, let x; y 2 Left ( ) and assume that M j= :Disj(x; y), namely M x \ M y 6= ;. Since by construction M x = fM xg and M y = fM yg, it follows that M x = M y, and therefore M x = M y. Hence, by the arbitrariness of x; y 2 Left( ), we have
M j=
^ x;y2Left( ) by the arbitrariness of x; y 2 Left ( ).
Next, let x 2 Left( ) and y 2 Vars(' ^ ) be such that M j= x y, i.e., M x M y. Hence, we have fM xg M y, and therefore M x 2 M y. The latter membership relation implies that the graph GM associated with the assignment M contains the arc (x; y), and so h(x) < h(y). Thus, by (H1) we have M xe ( M y, e and therefore we have
M j=
^ y2xV2aLresf(t'(^) ) (x y ! xe ( ye); by the arbitrariness of x 2 Left( ) and y 2 Vars(' ^ ).
Finally, let x; y 2 Vars('^ ) and assume that M x = M y, so that M x = M y. By (10), the nodes in GM labeled x and y have the same predecessors. Therefore, h(x) = h(y), so that by (H2) we have M x = M ye. Hence, by the arbitrariness of e x; y 2 Vars(' ^ ), we have
M j=
^ (x = y ! xe = ye): (11) (12) (13) (14) (15) (16) From (11){(16), it follows that the assignment M satis es '.
Summing up, from Lemmas 3, 8, and 9, we have: Theorem 2. Membership conjunctions are O(n2)-expressible from BST into BST+.
Design and analysis of the translation algorithm In order to prove Lemma 3, we provide a detailed speci cation of the algorithm that generates from the conjunction ' ^ the formula ' . 1: Initialize Vars(' ^ ) and Left ( ) as empty lists of set variables; 2: Initialize ' as an empty list of conjuncts; 3: for all set variable x that appears in ' do 4: add x to Vars(' ^ ); 5: for all conjunct x 2 y that appears in do 6: add x and y to Vars(' ^ ); 7: add x to Left ( ); 8: add (x 6= ; ^ x y to ' ); 9: for all x 2 Left ( ) do 10: for all y 2 Vars(' ^ ) do 11: add (:Disj(x; y) ! x y ^ x y ! x~ ( y~) to ' ; 12: for all x; y 2 Left ( ) do 13: add (:Disj(x; y) ! x = y ^ x = y ! x = y ^ x = y ! x~ = y~) to ' .
Adding elements to Vars(' ^ ), Left ( ), and ' will require constant time if these are implemented as lists of set variables and conjuncts.
The for-loop at lines 3 and 4 can be performed in (j'j)-time, where j'j is the total lenght of the conjunction '; similarly the for-loop from line 5 to line 8 can be performed in (j j)-time. The for-loop from line 9 to line 11 is iterated (jLeft ( ) Vars(' ^ )j) times and the for-loop at lines 12 and 13 is iterated jLeft ( )j2 times.
The overall time complexity is then j' ^ j + jLeft ( ) Vars(')j + jLeft ( )j2 , and since most commonly a conjunction ' ^ is such that j' ^ j = O jVars(' ^ )j2 and jLeft ( )j = (jVars(' ^ )j), we can say that ' can be generated in jVars(' ^ )j2 time. 4
Future work By a technique close to to the one proposed above for translating conjunctions of literals of the forms x = y n z, x 6= y n z, and x 2 y, it is possible to translate conjunctions of literals of the three forms x = y n z, x 6= y n z, and x = f y g into propositional combinations of BST literals. (This is an enhancement proper of the translation: in fact, x 2 y can be restated as s = f x g ^ z = z nz ^ z = sny.)
Moreover, we will strive to enhance the nested-to- at translation so as to enable it to handle rank comparison and cardinality comparison constructs.
We also have in mind a linear-cost at-to-nested translation, exploiting membership to eliminate the equality relator from conjunctions of BST literals in terms of membership literals.
With Mattia Furlan, who recently earned a bachelor degree from the University of Trieste, we have spotted out the following valid formulae involving Boolean di erence: (D:1) x n (y n y) = x (D:2) (x n y) n z = (x n z) n y (D:3) x n (x n y) = y n (y n x) (D:4) (x n y) n y = x n y
Existence of zero Permutativity Commutativity (of intersection)
Double subtraction Let us take the universal closures of these formulae as the axioms of a theory based on quanti cational rst-order logic with equality. These axioms characterize an algebraic variety, whose instances we provisionally dub here di erence algebras. We have an open issue: Is every di erence algebra D = (D; nD) isomorphic to an algebra of the form S = (S; n) which interprets the operator `n' as ordinary subtraction between sets? Here, of course, S must be a family of sets closed w.r.t. subtraction, hence w.r.t. \, because X \ Y = X n (X n Y ) holds for all sets X; Y . Perhaps, in order to settle this issue positively, we should somehow manage to apply Stone's celebrated representation theorem, stating that every Boolean algebra is isomorphic to a eld of sets. However, we see no direct way of relying on that theorem, because there are di erence algebras D whose support domain D fails to be closed w.r.t. symmetric di erence intended as an operation h Y ; Z i 7! Y 4D Z such that, for all X; Y; Z in D,
X = Y 4D Z
$ moreover, it is not clear to us how one can embed a generic di erence algebra into one which is a Boolean ring proper, because it enjoys this closure property.
X nD (Y nD Z) = Z nD Y ^ Y nD Z = X nD Z ;
Some auxiliary results
A lower bound on the number of sets of a positive integer rank Here we gure out inequalities preparatory to the proof of Proposition 2 below. Proposition 1. (a) For every k > 3, we have k > 2 + blog kc; (b) for every k > 2, we have 2k k > 2 k blog kc .
Proof. We prove (a) by induction on k > 3. For k = 3, we have 3 = 2 + blog 3c: For k > 3, by induction we have k 1 > 2 + blog(k
1)c: k > 2 + blog(k
1)c + 1 > 2 + blog kc: 22 2 = 2 = 2(2
blog 2c):
Concerning (b), we proceed by induction on k > 2. For k = 2, we have For k > 2, by induction we have: 2k 1 (k 1) > 2 k 1 blog(k 1)c A.1 Hence, so that and therefore By (a), we have so that jVnj
# jVn 1j = jVn 1j > 2
n 2;
jVn 1j > 2n 1:
blog jVnjc > 2n 1: Since Vn = P(Vn 1), we have jVnj = 2jVn 1j. Thus, by (17) and since jVn 1j is a power of 2, we obtain Finally, from Proposition 1(b) and (18) (since jVnj > 2), we have jVn#j = jVn+1j
Next we come to a proposition which lies in the background of this paper: Proposition 2. For every positive integer n, the number of well-founded sets of rank equal to n is greater than or equal to 2n 1, namely Proof. We proceed by induction on n > 1. For n = 1, we have jV1#j = 1 = 21 1. For n > 1, by induction we have: 2k k > 2k 2(k 1) > 4 k 1 blog(k 1)c > 4 k 1 blog kc : 4 k blog kc > 2 k blog kc ; (17) (18)
Two useful syllogisms The syllogisms validated by our next proposition play a role in the proofs of Lemma 6 and Lemma 8 as presented above.
Proposition 3. For all sets A; B; C; A0; B0; C0 such that
A [ B [ C \ A0 [ B0 [ C0 = ;; (19) (a) A [ A0 n B [ B0 = C [ C0 () A n B = C ^ A0 n B0 = C0 ; (b) A [ A0 = B [ B0 A = B ^ A0 = B0 .
() Proof. Concerning (a), by the left distributivity of [ over n, we have (A [ A0) n (B [ B0) = A n (B [ B0) [ A0 n (B [ B0) : In addition, from (19) it follows that
A n (B [ B0) [ A0 n (B [ B0) = (A n B) [ (A0 n B0): Hence, we have:
(A [ A0) n (B [ B0) = (A n B) [ (A0 n B0): Thus, if C = A n B and C0 = A0 n B0, the latter equation readily yields
A [ A0 n B [ B0 = C [ C0:
On the other hand, if A [ A0 n B [ B0 = C [ C0, setting U := A [ B [ C and U 0 := A0 [ B0 [ C0, by (19) we have
A n B = U \ (A n B) [ (A0 n B0) = U \ (C [ C0) = C and
A0 n B0 = U 0 \ (A n B) [ (A0 n B0) = U 0 \ (C [ C0) = C0:
A = (A [ B) \ A = (A [ B) \ A [ (A [ B) \ A0 = (A [ B) \ (A [ A0) = (A [ B) \ (B [ B0) Likewise, by interchanging in the previous proof A with A0 and B with B0, one can readily prove that A0 = B0 holds as well.