We present a nondeterministic polynomial-time decision procedure for an extension of multi-level syllogistic with the singleton operator, the Cartesian product, various map constructs, and special predicates asserting respectively that a map term is single valued, injective, and bijective, but with no map image or domain operators. We also prove that the extension of multi-level syllogistic with a map image operator has an ExpTime-hard decision problem, via a reduction of the decision problem for the description logic ALC.
The decision problem in set theory has been intensively investigated in the last
decades. The initial motivations can be traced back in 1978, when Jack Schwartz1
envisaged an interactive proof checker supposed to accept sequences of logical
formulae, such that any formula in the sequence follows logically from earlier
formulae (cf. [
Multi-level syllogistic (in short, MLS) has been the rst unquanti ed sublanguage of set theory to be studied in this context. We recall that MLS involves besides set variables and the `null set' constant ;, also the common Boolean set operators [, \, n, the set predicates 2, , and =, and the propositional connectives.
Over the years, decision procedures or proofs of undecidability have been
provided for several extensions of MLS and also for various quanti ed fragments
of set theory, contributing to the rise of the eld of Computable Set Theory
(see [
The quite recent implementation of the proof-veri cation system
tnaNova/Referee described in [
In this paper we present an e ective procedure (namely, having a
nondeterministic polynomial-time complexity) for an extension of MLS with the singleton
operator, the Cartesian product, and various map constructs, which we denote
MLSS2;m. More speci cally, MLSS2;m is a two-sorted language with set and map
variables. Set variables range over sets of the von Neumann cumulative hierarchy
of sets and map variables range over collections of pairs of sets (this acceptation
of the term `map' agrees with the map data structure in the SETL language;
see [
A similar two-sorted language, extended with domain and range operators,
but with no Cartesian product and no Boolean set operators among map terms,
has been considered in [
We mention also a one-sorted version of the language considered in [
The paper is organized as follows. Section 2 gives the precise syntax and semantics of the language MLSS2;m of our interest. A decision procedure for MLSS2;m and its complexity analysis are then reported in Section 3. In Section 4 we prove that the extension of MLS with the image operator has an ExpTimehard decision problem. Finally, we brie y give some hints to future work in Section 5. 2
The language MLSS2;m 2.1
Syntax MLSS2;m (Multi-Level Syllogistic with singleton, Cartesian product, and various map constructs) is a two-sorted language which contains: (i) a countably in nite collection of set variables Vars s = fx; y; z; : : :g; (ii) a countably in nite collection of map variables Vars m = ff; g; h; : : :g; (iii) the predicate symbols 2, =, , injective( ), single valued( ), bijective( ); (iv) the operator symbols \, [, n, (Cartesian product), f g (singleton), ( ) j, ( )j , ( ) j (map restriction operators), ( ) 1 (map inverse); (v) the constant ; (empty set); (vi) parentheses (to construct compound terms); (vii) the logical connectives :, ^, _, !, $ (to construct compound formulae).
MLSS2;m-set terms are recursively de ned as follows:
MLSS2;m-map terms are recursively de ned as follows: 1. each map variable is a map term; 2. if X; Y are set terms and F; G are map terms then { X Y , { FXj, FjY , FXjY (left, right, and left-right restriction, respectively), { F 1, F [ G, F \ G, F n G are map terms.
MLSS2;m-atomic formulae are de ned from set terms and map terms in the following way. Let X; Y be set terms and F; G be map terms, then 1. X 2 Y , X Y , X = Y , 2. [X; Y ] 2 F , F G, F = G, 3. injective(F ), single valued(F ), bijective(F ) are atomic formulae. Observe that a formula of type [X; Y ] 2 F is to be considered just as a ternary relationship among X, Y , and F , since we did not introduce any set term of type [X; Y ].
Then the set of MLSS2;m-formulae is the smallest set containing all the MLSS2;m-atomic formulae and that is closed with respect to the logical connectives :, ^, _, !, $. Usually, to denote MLSS2;m-formulae we will use the metavariables ' and .
For an MLSS2;m-formula ', we denote by Varss(') and Varsm(') the collections of set variables and of map variables occurring in ', respectively, and we put Vars(') = Def Varss(') [ Varsm('). 2.2
Semantics The semantics of MLSS2;m is based upon the von Neumann standard cumulative hierarchy V of sets de ned by:
V0 = ; V +1 = P(V ) ; for each ordinal
V = S < V ; for each limit ordinal
V = S 2On V ; where, given a set S, P(S) is the power set of S, and On indicates the class of all ordinals. It can be proved that the membership relation is well-founded in V and, therefore, no membership cycle can occur in V.
We denote with rank(u) the least ordinal such that u V (i.e., u 2 V +1), for every set u in V.
An assignment is a total function M : Varss [ Varsm ! V that maps each set and map variable into a set of the von Neumann hierarchy V, such that M f is a set of ordered pairs, for any f 2 Varsm. It is not relevant which representation is chosen for ordered pairs, as long as the basic ordered pair property holds. One possibility could be to adopt Kuratowski's de nition and put [u; v] = Def ffug; fu; vgg, for all sets u and v.
An assignment M is said to be injective with respect to a set of variables S Varss, if M x 6= M y, for all distinct variables x; y in S.
Assignments extend naturally to set terms and map terms. For instance, we have:
M (X
Y ) = f[u; v] : u 2 M X ^ v 2 M Y g ; M FXj = f[u; v] : [u; v] 2 M F ^ u 2 M Xg ; M F Y = f[u; v] : [u; v] 2 M F ^ v 2 M Y g ;
j
M FXjY = f[u; v] : [u; v] 2 M F ^ u 2 M X ^ v 2 M Y g ; where X; Y are set terms and F is a map term.3 3 For simplicity, in the following we will use the same operator and predicate symbols also at the semantic level. So, for instance, for any map m and set s, msj will denote the map f[u; v] : [u; v] 2 m ^ u 2 sg. This will generate no confusion.
Assignments evaluate atomic formulae of type X 2 Y , X Y , X = Y , F G, and F = G, to a truth value true or false in the standard way. Atomic formulae of the other types are evaluated as follows:
M ([X; Y ] 2 F ) is true () [M X; M Y ] 2 M F; M (single valued(F )) is true () (8u; v; v0)(f[u; v]; [u; v0]g M F ! v = v0); M (injective(F )) is true () (8u; u0; v)(f[u; v]; [u0; v]g M F ! u = u0); M (bijective(F )) is true () (8u; v; u0; v0)(f[u; v]; [u0; v0]g M F ! (u = u0 $ v = v0)): Finally, evaluation of compound formulae by an assignment M follows the standard rules of propositional logic.
Let M be an assignment and ' a formula of MLSS2;m. We say that M satis es ' (and write M j= ') if M evaluates ' to true. In this case M is said to be a model for '. A formula ' is satis able if there is an assignment that satis es it. Two formulae ' and are equisatis able, when ' is satis able if and only if is also satis able. A formula ' is injectively satis able with respect to a set of variables S if there is an injective assignment with respect to the set of variables S that satis es it.
The satis ability problem for MLSS2;m is then the problem of establishing for any given formula of MLSS2;m whether it is satis able or not.
Since the evaluation of an MLSS2;m-formula by an assignment depends solely on the values which it assumes over the variables occurring in the formula, in most cases we will deal with partial assignments, though we will refer to them just as `assignments'.
By way of a simple normalization process of the type described in [2, x3.8], it is easy to show that the satis ability problem for MLSS2;m-formulae reduces to the satis ability problem for normalized MLSS2;m-conjunctions, namely conjunctions of MLSS2;m-literals of the types reported in Table 1.4 For instance, to see that literals of type single valued(f ) and :single valued(f ) can be dismissed, it is enough to observe that :single valued(f ) is equisatis able with [x; y] 2 f ^ [x; y0] 2 f ^ y 2 z ^ y0 2= z ; where x; y; y0; z are newly introduced set variables, and that single valued(f ) is equivalent to injective(f 1), which in turn is equisatis able with g = f 1 ^ injective(g), where g is a newly introduced map variable. 3
In this section we describe a nondeterministic polynomial-time decision
procedure for the satis ability problem for normalized MLSS2;m-conjunctions. The
key idea behind such procedure is that a normalized MLSS2;m-conjunction is
4 Plainly, the expressions x 2= y and [x; y] 2= f in Table 1 are shorthands for the literals
:(x 2 y) and :([x; y] 2 f ), respectively.
x 2 y
x = y [ z
g = fxj
x 2= y
x = y n z
g = f 1
satis able if and only if there exists a nite structure, to be introduced later,
which witnesses this fact, in a sense that will be clari ed below. In addition,
the total size of such structure has a bound depending solely on the size of the
conjunction, This decision procedure is a generalization of the one presented in
[
To begin with, it is convenient to introduce some notations and de nitions.
Given a relation % over a set N and a nonempty subset V N , we say that % is V -extensional if h % ai 6= h % a0i, for all distinct a; a0 2 V , where h % ai = Def fb 2 N : b % ag :
Next, let 2b be an acyclic relation over a nite set N and let V N . We introduce a notion of height relative to V , for x 2 V , with the following recursion: V -height(x) = 0 if y 2b= x, with y 2 V , max V -height(y) : y 2 V ^ y 2b x + 1 otherwise.
We will use MLSS2;m-relation systems to witness the satis ability of normalized MLSS2;m-conjunctions. These are de ned as follows.
De nition 1 (MLSS2;m-relation system). An MLSS2;m-relation system is a tuple G =
V; T; F; 2b; ffb : f 2 F g , where { V and T are nite disjoint collections of set variables such that V 6= ;, { F is a nite collection of map variables, { 2b is an acyclic relation over V [ T , { nfb : f 2 F o is a collection of relations over V [ T . tu
MLSS2;m-relation systems allow to de ne special assignments, which are called realizations.
De nition 2 (Realization of an MLSS2;m-relation system). Let G = V; T; F; 2b; ffb: f 2 F g be an MLSS2;m-relation system and let fut : t 2 T g be a collection of sets. Then the realization of G relative to fut : t 2 T g is the assignment R over (V [ T ) [ F de ned recursively by: R x = R z : z 2b x ; for x 2 V , R t = R z : z 2b t [ futg ; for t 2 T , R f = n[R x; R y] : x fb y; for x; y 2 V [ T o ; for f 2 F . tu
The following lemma states conditions on MLSS2;m-relation systems which guarantee that it has realizations satisfying speci c MLSS2;m-literals. It will be used later to prove the correctness of the decision procedure outlined in Theorem 1 below.
Lemma 1. Let G = V; T; F; 2b; ffb: f 2 F g and let fut : t 2 T g be a collection of sets such that (a) 2b is V -extensional; (b) ut 6= ut0 , for all distinct t; t0 2 T ; (c) ut 6= R x, for all t 2 T; x 2 V [ T .
Then be an MLSS2;m-relation system (ix) R f = R g [ R h () fb = gb [ bh, for all f; g; h 2 F ; (x) R f = R g n R h () fb = gb n bh, for all f; g; h 2 F ; (xi) R f = (R g) 1 () fb = (g) 1, for all f; g 2 F ;
b (xii) injective(R f ) () injective(fb), for every f 2 F .
Proof. (i) To prove that R is injective with respect to V [ T we reason as follows. Let x; x0 be two distinct set variables in V [ T . We have to prove that R x 6= R x0. To begin with, let us assume that fx; x0g \ T 6= ;, and let, without loss of generality, x 2 T . If R x = R x0, then ux 2 R x0, which by (c) implies ux = ux0 , contradicting (b). Thus R x 6= R x0. Instead, if x; x0 2 V , we proceed by induction on = max(V -height(x); V -height(x0)). In the base case = 0, by V -extensionality, there must exist a t 2 T such that t 2b x if and only if t2b=x0. Suppose, without loss of generality, that t 2b x and t2b=x0. Thus R t 2 R x n R x0. Indeed, if R t 2 R x0, then there exists y 2 V [ T such that y 2b x0 and R t = R y. But then, as in the previous case, we would have that t and y have to be identical and therefore t 2b x0, which is a contradiction. Thus R x 6= R x0. For the inductive step, suppose by contradiction that R x = R x0, whereas (i) is true for every distinct y; y0 2 V such that max(V -height(y); V -height(y0)) < max(V -height(x); V -height(x0)) : (1) By V -extensionality, since x and x0 are distinct, there must be a y 2 V [ T such that y 2b x if and only if y2b=x0. Suppose, without loss of generality, that y 2b x and y2b=x0. Since R x = R x0, there must be a y0 2 V [ T such that y0 2b x0 and R y = R y0. But then, from the base case if fy; y0g \ T 6= ;, or from the inductive hypothesis if y; y0 2 V , y and y0 must be identical. This implies that w 2b v0, a contradiction. Thus we have R x 6= R x0 even if x; x0 2 V , whenever x and x0 are distinct.
Next we prove (ii). Plainly, if x 2b x0 then R x 2 R x0. On the other hand, if R x 2 R x0, then by (c) there must exist a y 2 V [ T such that y 2b x0 and R x = R y. But then, by (i), x and y must coincide and therefore x 2b x0.
In order to prove (iii), let x; y; z 2 V and assume rst that R x = R y [ R z. Then for every x0 2 V [ T we have: x0 2 h 2b xi () R x0 2 R x () R x0 2 R y [ R z () R x0 2 R y or R x0 2 R z () x0 2 h 2b yi or x0 2 h 2b zi () x0 2 h 2b yi [ h 2b zi, so that h 2b xi = h 2b yi [ h 2b zi. Analogously one can prove that h 2b xi = h 2b yi [ h 2b zi implies R x = R y [ R z.
Properties (iv) and (v) can be proved much as (iii).
(vi) follows immediately the very de nition of R f and from the injectivity of the realization R w.r.t. V [ T , already proved in (i).
To prove (vii), let f 2 F , x; y 2 V and suppose initially that R f = R x R y. Let x0; y0 be such that x0 fb y0. Then, by De nition 2, [R x0; R y0] 2 R f , so that R x0 2 R x and R y0 2 R y. Thus, (ii) yields x0 2b x and y0 2b y, and therefore fb h 2b xi h 2b yi. Similarly, it can be shown that h 2b xi h 2b yi fb, which together with the previous inclusion implies fb = h 2b xi h 2b yi. Conversely, assume that fb = h 2b xi h 2b yi. By (i), (vi), and De nition 2, [u; v] 2 Rf holds if and only if there are x0; y0 2 V [ T such that R x0 = u, R y0 = v, and x0 fb y0. From our assumption, it follows that x0 2b x and y0 2b y. Thus, by (ii), we have that u 2 R x and v 2 R y, so that R f R x R y. To show that R x R y R f , let [u; v] 2 R x R y. Since x; y 2 V , there exist x0; y0 in V [ T such that R x0 = u, R y0 = v, x0 2b x, and y0 2b y. Hence, by our assumption, x0 fb y0, and therefore [u; v] 2 R f , proving that R x R y R f .
To prove (viii), assume rst that R f = (R g)R xj. Then fb = (g) b h 2bxij follows plainly from (ii) and (vi). Next suppose that fb = (gb)h 2bxij and let u; v be any two sets such that [u; v] 2 R f . Then there exist x0; y0 in V [ T such that R x0 = u, R y0 = v, and x0 fb y0. But then, since fb = (g) b b h 2bxij, we have x0gv0, and x0 2b x, so that [u; v] 2 R g and u 2 R x, which in turn implies [u; v] 2 (R g)R xj, and therefore R f (R g)R xj. The converse inclusion can be proved analogously, completing the proof of (viii).
Properties (ix), (x), and (xi) are direct consequences of (vi).
Finally, let us prove (xii). First suppose that R f is injective and let x; y; y0 2 V [ T such that x fb y and x fb y0. By (vi), [R x; R y] and [R x; R y0] are in R f . Thus, by the assumed injectivity of R f and by (i), it follows that y = y0, proving that the map fb is injective. Conversely, let us assume that fb is injective. If [u; v] and [u; v0] are in R f , then there must exist x; y; y0 in V [ T such that R x = u, R y = v, R y0 = v0, x fb y, and x fb y0. The injectivity of fb implies y = y0, so that v = R y = R y0 = v0, proving that R f is injective too. tu
To any given assignment M and given collections of set and map variables, it is possible to associate a particular MLSS2;m-relation system, called canonical, which represents all membership relations among pairs of sets (M x; M y) and pairs of type ([M x; M y]; M f ), where x; y are set variables and f is a map variable belonging to the given collections of variables.
De nition 3 (Canonical MLSS2;m-relation system). Given { two disjoint nite collections V and T of set variables, such that V 6= ;, { a nite collection F of map variables, { an assignment M over (V [ T ) [ F , injective with respect to the variables in
V [ T , then the canonical MLSS2;m-relation system GM of M relative to (V; T; F ) is the MLSS2;m-relation system (cf. De nition 1)
G
M = Def V; T; F; 2bM; ffbM: f 2 F g ; where { x 2bM y () M x 2 M y, for every x; y 2 V [ T , { x fbM y () [M x; M y] 2 M f , for every x; y 2 V [ T and f 2 F . tu
The following lemma states some properties of canonical MLSS2;m-relation systems which will be used to prove the completeness of the decision procedure given in Theorem 1.
Lemma 2. Let V , T , F , M , and GM = De nition 3. Then, the following properties hold: (xiv) if injective(M f ) then injective(fbM ), for f 2 F .
Proof. (i) plainly follows from the de nition of 2bM and the acyclicity of the membership relation on sets. The remaining statements are immediate consequences of De nition 3. tu
The decidability of the satis ability problem for normalized MLSS2;mconjunctions is proved in the following theorem.
Theorem 1. Let ' be a normalized MLSS2;m-conjunction, V = Varss('), and F = Varsm('). Then ' is injectively satis able w.r.t. V if and only if there exist: { a nite collection T = ft1; : : : ; tmg of set variables, disjoint from V , with m = jT j jV j 1, { an MLSS2;m-relation system G = V; T; F; 2b; ffb : f 2 F g such that (a) 2b is V -extensional; (b) if x 2 y occurs in ' then x 2b y, for x; y 2 V ; (c) if x 2= y occurs in ' then x 2b= y, for x; y 2 V ; (d) if [x; y] 2 f occurs in ' then x fb y, for x; y 2 V; f 2 F ; (e) if [x; y] 2= f occurs in ' then [x; y] 2= fb, for x; y 2 V; f 2 F ; (f ) if x = y [ z occurs in ' then h 2b xi = h 2b yi [ h 2b zi, for x; y; z 2 V ; (g) if x = y n z occurs in ' then h 2b xi = h 2b yi n h 2b zi, for x; y; z 2 V ; (h) if f = g [ h occurs in ' then fb = gb [ bh, for f; g; h 2 F ; (i) if f = g n h occurs in ' then fb = gb n bh, for every f; g; h 2 F ; (j) if f = x y occurs in ' then fb = h 2b xi h 2b yi, for x; y 2 V , f 2 F ; (k) if f = gxj occurs in ' then fb = fbh 2bxij, for x 2 V , f 2 F ; (l) if injective(f ) occurs in ' then fb is injective, for every x 2 V , f 2 F ; V; T; F; 2b; ffb : f 2 F g Proof. We show rst that the conditions of the theorem are su cient for ' to be injectively satis able w.r.t. V . Thus, let T = ft1; : : : ; tmg and G = be as in the hypotheses and such that (a){(l) hold.
We use Lemma 1 to prove that some realization of the MLSS2;m-relation system G is an injective model for ' w.r.t. V . To this end, it is enough to exhibit a collection of sets futi : ti 2 T g such that (A) uti 6= utj , for all distinct ti; tj 2 T , and (B) uti 6= R x, for all ti; 2 T and v 2 V [ T , where R is the realization of G relative to futi : ti 2 T g and (V; T ). Let us put uti = Def fn; ig, for ti 2 T , where n = jV j.5 The sets uti are obviously pairwise 5 We are assuming the von Neumann representation of natural numbers 0 =Def ;, 1 =Def f0g, 2 =Def f0; 1g, and so on. distinct. In addition, we have rank(uti ) = n + 1, for uti 2 T . Hence, to prove (B), we can just show that rank(R x) 6= n + 1, for each x 2 V [ T . Thus, lmetemxb2ersVhi[p rTe.laItfiount)i t2h+enRraxnk((wRhver)e>2n++de1n.oOtenstthheeottrhaenrshitaivned,cilfosuutrie2=o+f Rthxe for all uti 2 T , by induction on V -height(x) it follows that rank(R x) < n.
Properties (b){(l) and Lemma 1 guarantee that R satis es all literals in '. For instance, if the literal x 2 y occurs in ', then by (b) we have x 2b y, so that Lemma 1(ii) yields R x 2 R y. Reasoning in a similar way, one can show that R satis es all the conjuncts in '. Additionally, by Lemma 1(i), R is injective w.r.t. V [ T , completing the proof of the su ciency part of the theorem.
Conversely, let M be a model for ' which is injective w.r.t. the collection of variables V = Varss('). We show next how to construct a collection T = ft1; : : : ; tmg of set variables with m = jT j jV j 1, and an MLSS2;m-relation such that conditions (a){(l) of Lemma 1 system G = V; T; F; 2b; ffb : f 2 F g are satis ed.
It is convenient to introduce the following notion (cf. [
Proof. If jSj 1, our claim is vacuously true. Otherwise, let jSj > 1 and, inductively, let us assume that our claim holds for any set S0 such that jS0j < jSj. Then, pick s 2 S. By our inductive hypothesis the set S n fsg admits a set 0 which distinguishes it and such that j 0j jSj 2. If 0 distinguishes S, we are done. Otherwise, there is an s0 2 S n fsg such that s \ 0 = s0 \ 0. Let d 2 (s n s0) [ (s0 n s) and consider = Def 0 [ fdg. We assert that distinguishes S. Indeed, if this were not the case there would exist an s00 2 S n fs; s0g such that s \ = s00 \ , so that s \ 0 = s00 \ 0 and, therefore, s0 \ 0 = s00 \ 0, contradicting our assumption that 0 distinguishes S n fsg. It only remains to observe that j j jSj 1. tu
In view of the above claim, let M be a set which distinguishes fM x : x 2 V g
and is such that j M j jV j 1. Also, let m = j M n fM x : x 2 V gj jV j 1
and let T = ft1; : : : ; tmg be a collection of m distinct set variables not belonging
to V . Let us extend/rede ne M over the variables in T in such a way that
fM ti : ti 2 T g = M nfM x : x 2 V g and let GM = V; T; F; 2bM; ffbM : f 2 F g
be the canonical MLSS2;m-relation system of M relative to (V; T ) and F . From
the well-foundedness of the membership relation in V, we have immediately that
2bM is acyclic. Additionally, by construction, if x; x0 2 V are any two distinct
variables, then there exists y 2 V [T such that M y 2 ((M xnM x0)[(M x0 nM x)).
Hence y 2bM x () y 2b=M x0, proving the V -extensionality of 2bM (condition (a)).
Conditions (b){(l) follows from Lemma 2 and from the fact that M satis es
all the literals of '. For instance, if x 2 y occurs in ', then we have plainly
6 See [
Since an MLSS2;m-conjunction of literals of the types listed in Table 1 is satis able if and only if there exists an equivalence relation on Varss( ) such that e is injectively satis able (w.r.t. Varss( e)), where e is the MLSS2;mconjunction obtained from by identifying -equivalent set variables, namely by replacing them by a common representative, we have the following result. Corollary 1. The ordinary satis ability problem for the class of MLSS2;mformulae is solvable. tu tu Theorem 1 leads to a nondeterministic polynomial-time decision test for the injective satis ability problem for normalized MLSS2;m-conjunctions (w.r.t. the collection of its set variables).
Lemma 3. The injective satis ability problem for normalized conjunctions w.r.t. set variables is NP-complete.
MLSS2;mProof. To begin with, the NP-hardness of the class of formulae of our interest
follows immediately from the NP-hardness of MLSS (cf. [
Varss('); T; Varsm('); 2b; ffb : f 2 Varsm(')g ; with jT j < jVarss(')j, such that conditions (a){(l) of Theorem 1 are satis ed. Since the size of G is at most quadratic in the size of ' and since conditions (a){ (l) can be veri ed in polynomial-time, it follows that the injective satis ability problem for normalized MLSS2;m-conjunctions is in NP and, therefore, is NPcomplete. tu
In view of Corollary 1 and the remarks just before its statement, we have also the NP-completeness of the ordinary satis ability problem for normalized MLSS2;m-conjunctions. To this end, it is enough to observe that given an equivalence relation on the set variables of a normalized MLSS2;m-conjunction ', then 'e can be computed in linear time (obviously, relative to the size of '). Thus we have: Corollary 2. The ordinary satis ability problem for normalized MLSS2;mconjunctions is NP-complete.
Remarks on the domain and image operators The same approach of Theorem 1 can not readily be applied to deal also with the extension of MLSS2;m with literals of the type x = dom(f ), where the semantics of the dom( ) operator is the obvious one, namely
M (dom(f )) = Def fs : [s; u] 2 M f; for some set ug ; for any assignment M .
Consider for instance a formula ' containing the literals x = dom(f0) and y 2 x and let M be a model for '. Let GM = canonical MLSS2;m-relation system of M , relative to a certain set T of auxiliary variables and let us assume that M x = fM yg and M f0 = f[M y; v]g, where v 6= M z for every set variable z 2 V [ T . Then fb0M= ; and
; = dom(fb0M) 6= h 2b xi = fyg : Most likely, any extension of the decision test contained in Theorem 1 to deal also with literals of type x = dom(f ) will involve the introduction in T of exponentially many auxiliary set variables in the size of the input formula. This is supported by the fact that any decidable extension of MLS with the literals of type y = f [x] (map image operator) is ExpTime-hard (see next section) and the fact that the literal y = f [x] can be expressed in any extension of MLSS2;m with literals of type x0 = dom(f 0) by the literal
On the other hand, we observe that the language MLSS2;m allows one to express literals of the types dom(f ) and f [x] y, in view of the equivalences y = dom((fxj) 1) : dom(f ) f [x] y x () f = fxj
() f = fxjy : 4
In this section we provide a complexity lower bound for the satis ability problem of the decidable extension MLSIm of MLS with literals of the type y = f [x].7 The semantics of the image operator f [x] is the obvious one, namely
M (f [x]) = Def fv : [u; v] 2 M f , for some u 2 M xg ; for any assignment M .
Our result is achieved by reducing the decision problem for the description logic ALC to the satis ability problem for MLSIm.
ALC is a two-sorted language which contains:
7 MLSIm is a subfragment of a an extension of MLSS with some map constructs, whose
decidability has been proved in [
{ concept names are concepts; { >; ? are concepts; { if C; D are concepts, then :C, C u D, and C t D are concepts; { if C is a concept and R is a role name, then 8R:C and 9R:C are concepts.
{ C v D (inclusion axiom), { C D (equivalence axiom), where C; D are ALC-concepts.
The semantics of ALC is given in terms of interpretations.8 An interpretation I consists of a nonempty set I , also called the domain of the interpretation, and of an interpretation function assigning to each concept name A 2 N c a set AI I , and to every role name R 2 N r, a binary relation RI I I .
An interpretation I extends recursively to concepts as follows: >I ?I (:C)I (C t D)I (C u D)I (8R:C)I (9R:C)I = Def = Def ;; = Def = Def = Def = Def = Def
I ;
I n CI ; CI [ DI ; CI \ DI ; u 2 I : (8v 2 I )([u; v] 2 RI ! v 2 CI ) ; u 2 I : (9v 2 CI )([u; v] 2 RI ) :
Let I be an interpretation and let C; D be two concepts. Then I satis es C v D (resp., C D) if CI DI (resp., CI = DI ). In addition, let T be a nite collection of axioms. Then I satis es T if and only if it satis es each axiom in T ; also, I satis es the concept C with respect to T if it satis es T and CI 6= ;. An ALC-concept C is said to be satis able with respect to a nite collection of axioms T if there exists an interpretation I that satis es C with respect to T , otherwise it is unsatis able. If I satis es a concept C (resp., a nite collection of axioms T ), then I is said to be a model for C (resp., T ).
In [8, Theorem 3.27, page 132] the ExpTime-hardness of the problem of deciding if a given concept C is unsatis able with respect to a given nite collection T of inclusion axioms is proved for the sublogic AL of ALC. Hence, we have: 8 Here we recall just the descriptive semantic. There are several other semantics that are out of the scope of this paper. Theorem 2. The problem of deciding whether a given ALC-concept C is unsatis able with respect to a given nite collection T of ALC-inclusion axioms is ExpTime-hard. tu
Next we show how the satis ability problem for ALC-concepts with respect to a nite set of axioms can be reduced to the satis ability of MLSIm-formulae. Since 9R:C :(8R:(:C)), without loss of generality we can consider only concepts that do not contain any occurrence of universal restriction.
Theorem 3. The satis ability problem for MLSIm is ExpTime-hard. Proof. In view of Theorem 2, it is enough to exhibit a reduction from ALC to MLSIm. Thus, given a nite collection T of ALC-inclusion axioms and an ALCconcept C, we show how to construct an MLSIm-formula which is satis able if and only if the concept C is satis able w.r.t. T .
Let Cpts N c and Rls N r be the collections of the concept names and of the role names, respectively, occurring in C and in T . Additionally, let be a function that injectively associates every concept name in Cpts to a set variable of the language MLSIm and every role name in Rls to a map variable of MLSIm. The function extends naturally to concepts and axioms in the following recursive way: (>) (?) (:C) (C u D) (C t D) (9R:C) (C v D) (C D) = Def U = Def ; = Def U n (C) = Def (C) \ (D) = Def (C) [ (D) = Def ( (R))[ (C)] = Def = Def (C) (D) (C) = (D) ; where U is a set variable of MLSIm not in [Cpts].
Let ' = Def 1 ^ 2 ^ 3 be the MLSIm-formula in which: 1 2 3 = Def = Def = Def
U 6= ; ^ VA2Cpts (A) V ( )
2T (C) 6= ;:
U ^ VR2Rls( (R))[U]
U We observe that the size of the MLSS2;m-formula ' is linear in the total size of T and C.
Next we show that ' is satis able (relative to the semantics of MLSIm) if and only if C is satis able w.r.t. T (relative to the semantics of ALC).
To begin with, let us assume that ' is satis able, and let M be a model for '. We construct an interpretation I, induced by M , with domain I = Def M U, by putting for every concept name A and role name R occurring in T or in C. Otherwise, the action of the interpretation I over the remaining concept and role names can be de ned arbitrarily, as long as the constraints AI I and RI I I hold, for each concept name A and role name R not occurring in T or in C.
Notice that since M models correctly all the literals in 1, then we actually have AI I and RI I I for all concept names A and role names R, respectively, showing that I is a valid interpretation. Moreover, for every concept D involving only variables that occur in T and in C we have
DI = M ( (D)) : (2) We prove (2) by structural induction on the concept D. If D is of type >, ?, :D0, D0 t D00, or D0 t D00, then (2) follows directly from the de nition of I. Thus, the only interesting case occurs when the concept D is of type (9R:D0), with R a role name in Rls and D0 a concept structurally simpler than D.
Let us show that (9R:D0)I = M ( (9R:D0)).
Let v 2 (9R:D0)I . Then there is a u 2 D0I = M ( (D0)) such that [v; u] 2 RI = ((M ( (R)))MUj) 1. The latter implies [u; v] 2 (M ( (R)))MUj, so that [u; v] 2 M ( (R)) (since u 2 M U), and therefore v 2 (M ( (R)))[M ( (D0))] = M ( (9R:D0)). Hence, (9R:D0)I M ( (9R:D0)).
To show the converse inclusion, let now v 2 M ( (9R:D0)). Then v 2 (M ( R))[M ( (D0))], so that [u; v] 2 M ( (R)) for some u 2 M ( (D0)). Therefore [u; v] 2 (M ( (R)))M(U)j (since by inductive hypothesis M ( (D0)) = D0I
I = M (U) and therefore u 2 M (U)). Hence, [v; u] 2 ((M ( (R)))M(U)j) 1 = RI . And since u 2 D0I , then v 2 (9R:D0)I . Therefore M ( (9R:D0)) (9R:D0)I which together with the previous inclusion yields (9R:D0)I = M ( (9R:D0)).
From (2) and the fact that M models correctly all the conjuncts of 2, it follows that I is a model for T . Additionally, since M satis es 3, it also follows that I satis es C, so that the interpretation I induced by the model M satis es C w.r.t. T . This completes the rst half of the proof.
Conversely, let I be a model for C w.r.t. T . Without loss of generality, we may assume that I is a set belonging to the von Neumann hierarchy V (otherwise, we embed I in V).
We construct an assignment MI induced by I as follows:
MI (U) = Def I ; M ( (A)) = Def AI ;
I M ( (R)) = Def (RI ) 1
I for all concept names A and role names R occurring in T and in C (as usual, we do not need to be speci c on the remaining variables of MLSIm), and show that MI is a model for '.
Much as was done before, we prove by structural induction that for every concept D involving only concept and role names occurring in T and C. As before, the only relevant case to be considered is when D is of type M ( (D)) = DI ;
I (3) (9R:D0). To prove (3) for a concept D of type (9R:D0), it is enough to show that MI ( (R))[MI ( (D0))] = (9R:D0)I .
Let u 2 (9R:D0)I . Then there is a v 2 D0I such that [u; v] 2 RI . Therefore [v; u] 2 M ( (R)) and since by inductive hypothesis v 2 M ( (D0)), it follows
I I that u 2 MI (( (R))[ (D0)]). Hence we have (9R:D0)I MI ( (R))[MI ( (D0))].
To prove the converse inclusion, let u 2 MI ( (R))[ (D0)]). Hence, there exists v 2 MI ( (D0)) such that [v; u] 2 MI ( (R)) = (RI ) 1. But then [u; v] 2 RI and since by inductive hypothesis M ( (D0)) = D0I , we have v 2 D0I , and thus
I u 2 (9R:D0)I . Therefore we have MI ( (R))[MI ( (D0))] (9R:D0)I , which together with the previously established inclusion yields M ( (R))[M ( (D0))] = I I (9R:D0)I .
Having established (3), it is immediate to check that the assignment MI satis es the MLSS2;m-formula ', completing the proof of the theorem. tu 5
We have introduced the unquanti ed fragment MLSS2;m of set theory, involving besides the basic set constructors, also the Cartesian product operator and some map constructs. We have shown that the satis ability problem for MLSS2;mformulae is NP-complete. We have also proved that any decidable extension of the basic fragment MLS extended with map literals of the form y = f [x] has an ExpTime-hard decision problem. Such lower bound has been obtained by exhibiting a reduction from the description logic ALC.
We plan to further investigate the relationship between description logics and other MLS extensions in order to nd new lower bounds. In particular, we conjecture that the presence of the map union and map di erence operators together with the image operator leads to NExpTime-hardness.
We also intend to extend the fragment MLSS2;m with some further map constructs such as re exive closure, transitive closure, symmetric closure, and restricted forms of map composition.
Furthermore, we plan to continue our investigations of decision procedure for a one-sorted variant of the language MLSS2;m in which maps (and the Cartesian product) are regarded just as primitive sets.