We continue our investigation aimed at spotting small fragments of Set Theory (in this paper, sublanguages of Boolean Set Theory) that might be of use in automated proof-checkers based on the set-theoretic formalism. Here we propose a method that leads to a cubictime satis ability decision test for the language involving, besides variables intended to range over the von Neumann set-universe, the Boolean operator [ and the logical relators = and 6=. It can be seen that the dual language involving the Boolean operator \ and, again, the relators = and 6=, also admits a decidable cubic-time satis ability test; noticeably, the same algorithm can be used for both languages. Suitable pre-processing can reduce richer Boolean languages to the said two fragments, so that the same cubic satis ability test can be used to treat the relators ; * and the predicates ` = ?' and `Disj( ; )', meaning `the argument is empty' and `the arguments are disjoint sets', along with their opposites ` 6= ?' and `:Disj( ; )'. Those richer languages are `polynomial maximal', in the sense that all languages strictly containing them have an NP-hard satis ability problem.
The eld named Computable Set Theory [
Long before the envisaged proof-veri er tnaNova [
By instantiating ? as [, we obtain the fragment BST([; =; 6=); by instantiating it as \, we obtain the fragment BST(\; =; 6=).
The paper is organized as follows. In Section 2 we introduce an equivalence relation ' between non-null subsets of the set of variables occurring in a formula ' of either fragment and elicit some of its key properties. Then, in Section 3, we present our main decidability results together with a cubic-time satis ability test, stressing the commonalities between the two decidable theories. In Section4, we report about extending the presented results to richer languages within BST. Then we draw conclusions. 2
Any given formula ' of BST(?; =; 6=) can be represented by two sets: ' := n ' := n fx1; fu1; ; xhg; fy1; ; umg; fv1; ; ykg j x1 ? ; vpg j u1 ? ? xh = y1 ? ? um 6= v1 ? ? yk is in 'o; ? vp is in 'o:
A central role will be played by the following relation ' on P+(Vars(')), where Vars(') is de ned to be the collection of all variables occurring in ', and P+(S) := P(S)nf;g for any set S. Speci cally, ' is the intersection|hence the inclusion minimal|of all equivalence relations on P+(Vars(')) that satisfy the following closure conditions: (Cl1) ' ,
B [ C, for all A; B; C 2 P+(Vars(')).
We will in fact prove, for any ' in BST(?; =; 6=), that ' is satis able if and only if fu1; : : : ; umg 6 ' fv1; : : : ; vpg holds for every literal of the form (6=) in '. We will exploit a useful closure operator to test conditions of the form Z1 6 ' Z2. Speci cally, we will prove that the set
Z := [fW j W ' Zg; called the '-closure of Z (or, more simply, the closure of Z, when the relation ' is understood), is the largest set '-equivalent to Z and then will provide a quadratic algorithm for computing it. Accordingly, a set Z such that Z = Z will be said to be '-closed or just closed.
Lemma 1. Let Z 2 P+(Vars(')). Then the closure Z of Z, namely the set [ fW j W ' Zg, is the largest subset of Vars (') that is '-equivalent to Z. Proof. Let W1; W2 be such that W1 ' Z and W2 ' Z. By applying (Cl2) twice, we have: W1 [ W2 ' Z [ W2 ' Z: In view of the niteness of fW j W ' Zg, by induction it follows that [ fW j W ' Zg ' Z : In addition, for every W 0 such that W 0 ' Z, we plainly have W 0 [fW j W ' Zg. This yields that [fW j W ' Zg is the largest set in P+(Vars(')) that is '-equivalent to Z.
The equivalence relation ' captures which equalities among terms must be true in every model, if any, of a given formula ': this is shown in the next lemma.
A set assignment M is any function sending a collection dom(M ) of set variables into the von Neumann universe of all sets V := [ 2On V , resulting from the union 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 and to every literal of BST(?; =; 6=) such that Vars( ) dom(M ), for any set assignment M :
when Vars(`i) dom(M ), for i = 1; : : : ; k.
M ( ? ) := M ? M
; (true
if M = M M ( = ) :=
false otherwise; M ( 6= ) := :M ( = ) : M (`1 ^ ^ `k) := M `1 ^ ^ M `k
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. For convenience, in what follows we will use the shortening notations M fx1; : : : ; xkg := fM x1; : : : ; M xkg ; Ffx1; : : : ; xkg := x1 ? ? xk ;
Ffs1; : : : ; skg := s1 ? ? sk ; where M represents a set assignment, x1; : : : ; xk and s1; : : : ; sk denote variables and sets, respectively, and the ?'s stand for alike symbols/operations `[' or `\'.
Lemma 2. Let ' be any formula in BST(?; =; 6=), and let M be any set assignment over Vars (') satisfying '. Then
Z1 ' Z2 =)
FM Z1 = FM Z2; for all Z1; Z2 2 P+(Vars(')).
that the equivalence relation ' is inclusion-minimal, it is su cient to prove
M over P+(Vars(')) de ned by Z1
M Z2 (D=e=)f.
FM Z1 = FM Z2 satis es the closure conditions (Cl1) and (Cl2).
Concerning (Cl1), if fL; Rg 2 ' then FM L = FM R, so L proving ' M .
As for (Cl2), let A M B and C therefore Vars('). Then FM A = FM B, and
FM (A [ C) = (FM A) ? (FM C) = (FM B) ? (FM C) = FM (B [ C); from which A [ C
We next prove the following key property, which will be used in the correctness proof of our fast algorithm presented in Section 3.1 for computing 'closures.
Lemma 3. Given a BST(?; =; 6=)-formula ', let Z 2 P+(Vars(')) be such that L
Z () R
Z ; for every fL; Rg 2 ' .
Then, for all W1; W2 2 P+(Vars(')) such that W1 ' W2, we have W1
Z () Proof. Let ' and Z be as in the hypothesis. In view of the -minimality of ', it su ces to prove that the equivalence relation over P+(Vars(')) de ned by W1 Z W2 (D=e=)f.
W1
Z () W2
Z (3) satis es the closure conditions (Cl1) and (Cl2).
As for (Cl1), just from the hypothesis it follows that L Z R, for every fL; Rg 2 ' . Concerning (Cl2), let A Z B and C Vars('), and assume that A [ C Z. Then, A Z and C Z, so that by (3) we have B [ C Z. Symmetrically, it can be shown that B [ C Z implies A [ C Z. Hence, A [ C
Z () B [ C
Z holds and, by (3), we readily have A [ C Z B [ C. The arbitrariness of A, B, and C yields that even the closure condition (Cl2) holds for Z.
Finally, from the -minimality of ', we have ' Z. Therefore, if W1 ' W2, then W1 Z W2, which by (3) implies W1 Z () W2 Z.
Further useful properties of the '-closure operator and of the equivalence relation ' are reported in the following lemma.
Lemma 4. Let Z; Z1; Z2 2 P+(Vars(')). Then
' Z; (a) (b) (c) (d) (e) (f) (g)
Z Z and Z Z = Z; if Z1 Z1 if Z1 Z1 if Z1
' Z2, then Z1 Z2; ' Z2 if and only if Z1 = Z2;
Z2, then Z1 Z2; Z2 if and only if Z1 Z2;
Z or Z2 Z holds and Z1 ' Z2, then Z ' Z [ Z1 [ Z2.
Proof. Property (a) follows directly from Lemma 1.
Concerning (b): the transitivity of ' yields Z ' Z so that, by the de nition of Z, Z Z holds. By (a) we have Z Z, therefore Z = Z.
As for (c), if Z1 ' Z2, then Z1 Z2 = Z2.
Concerning (d), if Z1 ' Z2, then the transitivity of ' yields Z1 ' Z2. Thus, by (c), we get Z1 = Z2. Conversely if Z1 = Z2, then Z1 ' Z2, thus by transitivity Z1 ' Z2 holds.
Regarding (e), let Z1 Z2. Since by (a) Z2 Z2 and Z1 ' Z1 hold, by (Cl2) we have
Z2 = Z1 [ (Z2 n Z1) ' Z1 [ (Z2 n Z1) = Z1 [ Z2 : Thus, by (c), we get the inclusion Z1 [ Z2 Z2, and therefore Z1 Z2.
Concerning (f), if Z1 Z2, then by (e) and (b) we have Z1 Z2 = Z2. Conversely, if Z1 Z2, then by (a) we have Z1 Z1 Z2.
Finally, as for (g), suppose that we have Z1 ' Z2 and either Z1 Z or Z2 Z holds. By (Cl2), we have Z [ Z1 ' Z [ Z2. But fZ [ Z1; Z [ Z2g = fZ; Z [ Z1 [ Z2g, hence Z ' Z [ Z1 [ Z2 follows.
Satis ability in BST([; =; 6=) and in BST(\; =; 6=) Below we will present a necessary condition that also su ces to ensure that a given formula in either BST([; =; 6=) or BST(\; =; 6=) is satis able. Noticeably, this condition is essentially the same for both languages, so that the same algorithm can be used to test formulae of either language for satis ability. Theorem 1. Let ' be a BST([; =; 6=)-formula. Then ' is satis able if and only if L 6 ' R (namely L 6= R) holds for every literal of the form [L 6= [R in '. Proof. (Necessity.) Let M be a model for '. By way of contradiction, assume that there exists a literal [L 6= [R such that L ' R. Then by Lemma 2 we would have [M L = [M R, a contradiction. Therefore for all literals [L 6= [R we must have L 6 ' R, completing the necessity part of the proof.
(Su ciency.) Next, let us assume that, for each fL; Rg 2 ' , we have L 6 ' R. We will construct a set assignment M that satis es '.
Let us assign a nonempty set bV to each V such that V 2 [ ' in such a way that the bV 's are pairwise distinct.3 Then we de ne the set assignment M over Vars(') by putting, for each x 2 Vars('),
M x := fbV j x 2= V and V 2 [ ' g; so that we have [M U := fbV j U * V and V 2 [ ' g; (4) for every U Vars(').
We rst show that [M L = [M R holds whenever fL; Rg 2 ' . Thus, let fL; Rg 2 ' and let bV 2 [M L, for some V 2 ' such that L * V . Then L * V , by Lemma 4(f). Since fL; Rg 2 ' , then by (Cl1) we have L ' R, so that, by (d) and (f) of Lemma 4, R * V follows. Hence bV 2 [M R, and by the arbitrariness of bV we have [M L [M R.
Analogously one can prove [M R [M L, so [M L = [M R holds, as we intended to show.
Next we prove that [M L 6= [M R holds, whenever fL; Rg 2 ' . Thus, let fL; Rg 2 ' , so that by our assumption we have L 6 ' R. Hence, by Lemma 4(d), L 6= R. W.l.o.g., let us assume that L * R. Since R R (by Lemma 4(a)) and plainly R 2 [ ' , then bR 2= [M R, by (4). On the other hand, by Lemma 4(f), L * R, hence bR 2 [M L, again by (4), and therefore [M L 6= [M R, concluding the proof of the theorem.
In a dual manner, one can also prove the following result: 3 For de niteness, such bV 's can be drawn
f;g; ff;gg; fff;ggg; : : : of Zermelo's non-zero numerals.
Theorem 2. Let ' be a BST(\; =; 6=)-formula. Then ' is satis able if and only if L 6 ' R (namely L 6= R) holds for every literal of the form \L 6= \R in '. from the collection
A cubic-time satis ability test for BST([; =; 6=) and for BST(\; =; 6=) Theorems 1 and 2 imply that any BST(?; =; 6=)-formula ', where ? 2 f[; \g, is satis able if and only if L 6= R holds for every literal FL 6= FR in '. Hence, they yield straight decision procedures for the theories BST(?; =; 6=), with ? 2 f[; \g.
The next step will then be to provide a quadratic algorithm for computing the closure Z of any input Z 2 P+(Vars(')), namely, the largest set in P+(Vars(')) which is '-equivalent to Z.
In Algorithm 1 below, we provide a high-level speci cation of the function Closure, intended to compute the closure Z of any given Z 2 P+(Vars(')), for a BST(?; =; 6=)-formula '. After proving its correctness, we will illustrate a lower-level implementation whose time complexity is quadratic (as opposed to the cubic-time complexity which would ensue from a naive implementation).
Require: A BST(?; =; 6=)-formula ' represented by the sets of pairs ' and ' . Ensure: Is ' satis able ? 1: for each fL; Rg in ' do 2: if Closure(L, ' ) = Closure(R, ' ) then 3: return false; 4: return true; 1: function Closure(Z, ' ) 2: 3: 4: 5:
Input: a set Z and the set ' Output: the '-closure Z of Z
Z Z; while there exists fL; Rg 2 ' such that L
Z Z [ L [ R; return Z; Z () R 6 Z do
We can now prove quite easily the correctness of the function Closure. Lemma 5. The function Closure computes closures correctly. Proof. Given a BST(?; =; 6=)-formula ', with input a set Z Vars(') and a collection ' the while-loop of the function Closure plainly terminates within a number k 6 j ' j of iterations. Let Zi be the value of the variable Z after i iterations, so that Z0 = Z. Preliminarily, we prove by induction on i = 0; 1; : : : ; k that Zi ' Z and Z Zi.
The base case i = 0 is trivial.
Next, let fL; Rg 2 ' be the pair selected by the while-loop during its i-th iteration, with i > 1. Hence, we have:
L ' R;
L
Zi 1 () R 6 Zi 1; and Zi = Zi 1 [ L [ R: Thus, by inductive hypothesis and Lemma 4(g), we have
Z from which Z ' Zi and Z Zi follow. Hence, by induction, we have Z ' Zf and Z Zf, where Zf := Zk is the nal value of the variable Z returned by the execution of Closure(Z; ' ).
In addition, the termination condition for the while-loop yields that L Zf () R Zf, for all fL; Rg 2 ' . Thus, from Lemma 3, it follows that W1
Z f () W2
Zf; (5) for all W1; W2 2 P+(Vars(')) such that W1 ' W2.
In order to prove that Zf = Z, we observe that, since Z ' Z and Z Zf, by (5) we have Z Zf. Moreover, by Lemma 4(a),(d) and since Z ' Zf, we readily get Zf Zf = Z. The latter inclusion, together with the previously established one Z Zf, implies Zf = Z, i.e., Zf is the closure of Z, proving that the call to Closure(Z; ' ) computes the closure Z of Z correctly.
Theorems 1 and 2, together with Lemma 5 and Lemma 4(d), readily yield that Algorithm 1 is a valid satis ability test for formulae in the languages BST([; =; 6=) and BST(\; =; 6=).
A quadratic implementation of the function Closure Next, we provide a quadratic implementation of the function Closure, which, for a given BST(?; =; 6=)-formula ', takes as input the collection ' and a set Z 2 P+(Vars(')) of which one wants to compute the closure Z. As internal data structures, the function Closure uses: a doubly linked list Ripe of sets of the form (L [ R) n Z, where fL; Rg 2 ' and Z is the internal variable whose value will converge to Z at termination; a doubly linked list Unripe of pairs of form (L n Z); (R n Z) , with fL; Rg 2 ' ; and an array Aux of m lists of pointers to nodes either in Ripe or in Unripe, where m is the number of the distinct variables x1; : : : ; xm in ', intended to allow fast retrieval of nodes in the lists Ripe and Unripe.
We will express the complexity of the main procedure in Algorithm 1 and of our e cient implementation of the function Closure in terms of the four quantities m; n; p; q, where m = jVars(')j is the number of distinct set variables in ', n = j'j is the size of ', p = j ' j is the number of literals of the form (=) in ', and q = j ' j is the number of literals of the form (6=) in '. Plainly, we have m; p; q 6 n.
Much as in [
Having sorted , we can easily collect the m 6 n distinct variables of ' and index them using the integers 1; : : : ; m. By means of such an indexing, in O(m(p + q)) time (where p = j ' j and q = j ' j) we can represent as an m-bit array each set of variables in [ ' [ [ ' , and accordingly represent ' and ' as lists of pairs of m-bit arrays. Such preliminary encoding phase can be carried out in O(m(p + q) + n) time.
We make use of the auxiliary functions Add(List, S) and Remove(List, Ptr) to add S to List (S can be either a set or a pair of sets) and to remove the node pointed to by Ptr from List, respectively. Since the two lists we use, namely Ripe and Unripe, are maintained as doubly linked lists, both operations can be performed in O(1) time. The function Add returns also a pointer to the newly inserted node. Finally, we use the function Extract(List) to access in O(1) time the pointer to the rst node of List while removing it.
The function Closure(Z; ' ) comprises two phases: an initialization phase, lines 2{8, and a computation phase, lines 9{25.
For each m-bit array, we maintain a counter of its bits set to 1, so that emptiness tests can be performed in O(1) time. Plainly, unions, set di erences, and inclusion tests of sets represented as m-bit arrays can easily be performed in O(m) time. Also, membership tests and the operations of singleton addition and singleton removal can be performed in O(1) time.
Thus, the initialization phase of the function Closure (lines 2{8) can be performed in O(mp) time.
At the end of the initialization phase and at each subsequent step, the lists Ripe and Unripe contain only sets disjoint from Z, and each of them has length at most p = j ' j. Speci cally, the list Ripe contains the set (L [ R) n Z, for all fL; Rg 2 ' such that L [ R 6 Z but either L Z or R Z holds. Instead, the list Unripe contains the pair hL n Z; R n Zi, for all fL; Rg 2 ' such that L 6 Z and R 6 Z both hold.
In view of the assignments at lines 15, 18, and 19, the disjointness property from Z of the sets (L [ R) n Z in Ripe and the sets L n Z and R n Z such that fL n Z; R n Zg is in Unripe is maintained at each iteration of the while-loop at lines 9{24. Hence, at each extraction of a set S from the list Ripe at line 10, none of the set variables in S has already been selected and processed by the for-loop 11{24. Therefore, each set variable in Vars(') is processed by the forloop at lines 11{24 at most once, yielding that, in the overall, the for-loop 11{24 is executed at most m times, for a total of O(mp) time, since each execution of the for-loop 11{24, say relative to a set variable xi, is dominated by the time taken by the internal for-loop 13{24, which is O(p). Indeed, (i) at the end of the initialization phase, the list Aux[i] contains at most p pointers to nodes in the lists Ripe and Unripe; (ii) once a pointer in the list Aux[i] is processed, it is then removed (line 24), so that it will never be processed again; and (iii) each line of the for-loop 13{24 can be executed in constant time.
Since each extraction at line 10 takes O(1) time and, as observed, the list Ripe has size at most p at the end of the initialization phase, it follows that the while-loop at lines 9{24 takes O(mp) time.
Thus, the overall complexity of the function Closure is O(mp) time. Since m; p 6 n, we have also that the function Closure takes quadratic time O(n2) in the size n of the formula ' to be tested for satis ability.
Finally, our satis ability tester (Algorithm 1) checks at most q pairs fL; Rg 2 ' in O(mpq) time, by computing the closures L and R by means of calls to the function Closure and comparing them. By taking into account also the preliminary encoding phase, which has a O(m(p + q) + n)-time complexity, the overall complexity of Algorithm 1 is O(mpq+n), which is O(n3) since m; p; q 6 n.
Concerning the space complexity of our satis ability tester, it is immediate to check that all data structures used in Algorithm 1 and in the function Closure require O(mp) space, namely O(n2) space since m; p 6 n.
Summarizing, we have proved the following result: Theorem 3. The satis ability decision problem for the language BST([; =; 6=), as well as for BST(\; =; 6=), can be solved in cubic time and quadratic space. Remark 1. It is not hard to see that our satis ability tester (Algorithm 1) and its auxiliary function Closure can be re ned in order that an explicit set assignment modeling the input conjunction ' is returned when ' is satis able.
Extensions of BST([; =; 6=) and BST(\; =; 6=)
In [
Regarding the languages BST([; =; 6=) and BST(\; =; 6=), we have: (a) the literal x = ? is O(n)-expressible in BST([; =); (b) the literal x = ? is O(n)-expressible in BST(\; =);4 (c) the literal x y is existentially expressible in BST([; =) and in BST(\; =); (d) the literal x * y is existentially expressible in BST([; 6=) and in BST(\; 6=); (e) the literal Disj(x; y) is existentially expressible in BST(\; =?) and therefore, by (b), it is O(n)-expressible in BST(\; =); (f) the literal :Disj(x; y) is existentially expressible in BST( ; 6=); therefore, by (c), it is existentially expressible in both of BST([; =; 6=) and BST(\; =; 6=).
Wrapping up, we have that (a), (c), (d), and (f) ensure that any BST([; =?; 6=?; :Disj; ; *; =; 6=)-formula can be reduced in linear time to an equisatis able BST([; =; 6=)-formula. Similarly (b), (c), (d), and (e), (f) ensure that any BST(\; =?; 6=?; Disj; :Disj; ; *; =; 6=)-formula can be reduced in linear time to an equisatis able BST(\; =; 6=)-formula. Therefore: Lemma 6. The satis ability decision problem for either one of the languages BST([; =?; 6=?; :Disj; ; *; =; 6=), BST(\; =?; 6=?; Disj; :Disj; ; *; =; 6=) can be solved in cubic time.
Remark 2. In [
Related work and conclusions
In [
We plan to address the satis ability problem for the theories BST([; 6 ; 6=) and BST(\; 6 ; 6=) by suitably adapting to them the equivalence relation ' and its related closure operator introduced in this paper for the fragments BST([; =; 6=) and BST(\; =; 6=). In view of the equivalences
A = B A = B () A 6
A [ B ^ B 6 A () A \ B 6
A ^ B 6
A; it turns out that the theories BST([; 6 ; 6=) and BST(\; 6 ; 6=) are extensions of BST([; =; 6=) and of BST(\; =; 6=), respectively. Notice that the relation A 6 B, which stands for A * B _ A = B, embodies a disjunction. It is therefore expected that the resulting satis ability tests for BST([; 6 ; 6=) and BST(\; 6 ; 6=) may have a complexity worse than cubic, though still polynomial.
We envisage a con uence of the line of research centered on satis ability
testers, to which this paper, along with [
Another foreseeable con uence has to do with a long-standing line of research
initiated by [
We are also grateful to the anonymous reviewers for their helpful comments.
In this appendix we highlight the reduction technique used in Section 4.
Most of our reductions are based on the standard notion of `context-free' expressibility: 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.
We also devised a more general notion of `context-sensitive' expressibility, embodying complexity-related information.
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 h '( y ) ; ( x ) i 7! ' ( x; y; z ) 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 (6) 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 ).
We are now ready to prove that the literal x = ? is O(n)-expressible in BST(\; =), albeit not existentially expressible in BST(\; =; 6=).
Lemma 7. The literal x = ? is not existentially expressibile in BST(\; =; 6=). Proof. Assume by way of contradiction that x = ? is existentially expressible in BST(\; =; 6=), so that there exists a BST(\; =; 6=)-formula (x; y) such that: j= x = ? () (9z) (x; z):
Since x = ? is plainly satis able then so it is , therefore it is satis ed by the set assignment x 7!M fbV j x 2 V g (dual to the assignment (4), and actually exploited in the proof of Theorem 2). Notice that M is such that, for each set variable y 2 Vars( ), M y 6= ; holds; and, since x 2 Vars( ) we obtain M j= (9z) ^ x 6= ;; contradicting (7), whence our claim follows.
Lemma 8. The literal x = ? is O(j'j)-expressible from BST(\; =) into BST(\; =). (6) (7) Proof. We will show that the map h '(y) ; x = ? i 7! (8) de ned for all '(y) 2 BST(\; =) , satis es (a), (b), and (c), where f is the function sending each formula ' to its length n = j j ' .
Plainly the map (8) can be computed by collecting all variables occurring in the formula ' while scanning it, hence it can be computed in O(n)-time.
Concerning (b), let M be a model for '(y) ^ \y2y y \ x = x. Then we have M x = M x \ M y, namely M x M y, for all y 2 Vars('). Put
M 0v := M v n M x; for every set variable v 2 Vars(') [ fxg. Plainly M 0x = M x n M x = ;, so that M 0 j= x = ?.
To see that M 0 j= '(y), consider any literal \L = \R of ', and note that: (since M j= ') therefore M 0 models each literal of '.
Finally, concerning (c), let M be a model for '(y) ^ x = ?. Then M x = ; so that \ M y \ M x = \ M y \ ; = ; = M x; y2y y2y by the genericity of M , we readily get j= '(y) ^ x = ? ! \ y \ x = x; y2y