On the satisfiability problem for a 4-level quantified syllogistic and some applications to modal logic Domenico Cantone and Marianna Nicolosi Asmundo Dipartimento di Matematica e Informatica, Università di Catania Viale A. Doria 6, I-95125 Catania, Italy e-mail: cantone@dmi.unict.it, nicolosi@dmi.unict.it Abstract. We introduce a fragment of multi-sorted stratified syllogistic, called 4LQS R , admitting variables of four sorts and a restricted form of quantification, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the sublanguage (4LQS R )k of 4LQS R , where the length of quantifier prefixes (over variables of sort 1) is bounded by k ≥ 0, and prove that its satisfiability problem is NP-complete. Finally we show that modal logics S5 and K45 can be expressed in (4LQS R )1 . 1 Introduction Most of the decidability results in computable set theory concern one-sorted multi-level syllogistics, namely collections of formulae admitting variables of one sort only, which range over the von Neumann universe of sets (see [6, 8] for a thorough account of the state-of-art until 2001). Only a few stratified syllogistics, where variables of several sorts are allowed, have been investigated, despite the fact that in many fields of computer science and mathematics often one has to deal with multi-sorted languages. For instance, in modal logics, one has to consider entities of different types, namely worlds, formulae, and accessibility relations. In [10] an efficient decision procedure was presented for the satisfiability of the Two-Level Syllogistic language (2LS). 2LS has variables of two sorts and admits propositional connectives together with the basic set-theoretic operators ∪, ∩, \, and the predicates =, ∈, and ⊆. Then, in [2], it was shown that the ex- tension of 2LS with the singleton operator and the Cartesian product operator is decidable. Tarski’s and Presburger’s arithmetics extended with sets have been analyzed in [4]. Subsequently, in [3], a three-sorted language 3LSSP U (Three- Level Syllogistic with Singleton, Powerset and general Union) has been proved decidable. Recently, in [7], it was shown that the Three-Level Quantified Syllo- gistic with Restricted quantifiers language (3LQS R ) is decidable. 3LQS R admits variables of three sorts and a restricted form of quantification. Its vocabulary contains only the predicate symbols = and ∈. In spite of that, 3LQS R allows to express several constructs of set theory. Among them, the most comprehensive one is the set former, which in turn enables one to express other operators like the powerset operator, the singleton operator, and so on. In this paper we present a decidability result for the satisfiability problem of the set-theoretic language 4LQS R (Four-Level Quantified Syllogistic with Re- stricted quantifiers). 4LQS R is an extension of 3LQS R which admits variables of four sorts and a restricted form of quantification over variables of the first three sorts. Its vocabulary contains the pairing operator ·, · and the predicate symbols = and ∈. We will prove that 4LQS R enjoys a small model property by showing how one can extract, out of a given model satisfying a 4LQS R -formula ψ, another model of ψ but of bounded finite cardinality. The construction of the finite model extends the decision algorithm described in [7]. Concerning complexity issues, we will show that the satisfiability problem for each of the sublanguages (4LQS R )k of 4LQS R , whose formulae are restricted to have quantifier prefixes over variables of sort 1 of length at most k ≥ 0, is NP-complete. Clearly, 4LQS R can express all the set-theoretical constructs which are al- ready expressible by 3LQS R . In addition, in 4LQS R one can plainly formalize several properties of binary relations also needed to define accessibility relations of well-known modal logics. 4LQS R can also express Boolean operations over relations and the inverse operation over binary relations. Finally, we will show that the modal logics S5 and K45 can be easily formalized in the (4LQS R )1 lan- guage. Since the satisfiability problems for S5 and K45 are NP-complete, in terms of computational complexity the algorithm we present here can be considered optimal for both logics. 2 The language 4LQS R Before defining the language 4LQS R , in Section 2.1 we present the syntax and the semantics of a more general four-level quantified fragment, denoted 4LQS . Then, in Section 2.2, we introduce some restrictions over the quantified formulae of 4LQS which characterize 4LQS R -formulae. 2.1 The more general language 4LQS Syntax of 4LQS . The four-level quantified language 4LQS involves four col- lections V0 , V1 , V2 , and V3 of variables. (i) V0 contains variables of sort 0, denoted by x, y, z, . . .; (ii) V1 contains variables of sort 1, denoted by X 1 , Y 1 , Z 1 , . . .; (iii) V2 contains variables of sort 2, denoted by X 2 , Y 2 , Z 2 , . . .; (iv) V3 contains variables of sort 3, denoted by X 3 , Y 3 , Z 3 , . . .. 4LQS quantifier-free atomic formulae are classified as: level 0: x = y, x ∈ X 1 , for x, y ∈ V0 , X 1 ∈ V1 ; level 1: X 1 = Y 1 , X 1 ∈ X 2 , for X 1 , Y 1 ∈ V1 , X 2 ∈ V2 ; level 2: X 2 = Y 2 , x, y = X 2 , x, y ∈ X 3 , X 2 ∈ X 3 , for X 2 , Y 2 ∈ V2 , x, y ∈ V0 , X 3 ∈ V3 . 4LQS quantified atomic formulae are classified as: level 1: (∀z1 ) . . . (∀zn )ϕ0 , with ϕ0 any propositional combination of quantifier- free atomic formulae, and z1 , . . . , zn variables of sort 0; level 2: (∀Z11 ) . . . (∀Zm 1 )ϕ1 , where Z11 , . . . , Zm 1 are variables of sort 1, and ϕ1 is any propositional combination of quantifier-free atomic formulae and of quantified atomic formulae of level 1; level 3: (∀Z12 ) . . . (∀Zp2 )ϕ2 , with ϕ2 any propositional combination of quantifier- free atomic formulae and of quantified atomic formulae of levels 1 and 2, and Z12 , . . . , Zp2 variables of sort 2. Finally, the formulae of 4LQS are all the propositional combinations of quantifier- free atomic formulae of levels 0, 1, 2, and of quantified atomic formulae of levels 1, 2, 3. Semantics of 4LQS . A 4LQS -interpretation is a pair M = (D, M ), where D is any nonempty collection of objects, called the domain or universe of M, and M is an assignment over the variables of 4LQS such that – M x ∈ D, for each x ∈ V0 ; – M X 1 ∈ pow(D), for each X 1 ∈ V1 ; – M X 2 ∈ pow(pow(D)), for all X 2 ∈ V2 ; – M X 3 ∈ pow(pow(pow(D))), for all X 3 ∈ V3 .1 Moreover we put M x, y = {{M x}, {M x, M y}}. Let - M = (D, M ) be a 4LQS -interpretation, - x1 , . . . , xn ∈ V0 , - X11 , . . . , Xm 1 ∈ V1 , - X1 , . . . , Xp2 ∈ V2 , 2 - u1 , . . . , un ∈ D, - U11 , . . . , Um1 ∈ pow(D), - U12 , . . . , Up2 ∈ pow(pow(D)). By M[x1 /u1 , . . . , xn /un , X11 /U11 , . . . , Xm 1 1 /Um , X12 /U12 , . . . , Xp2 /Up2 ] , we denote  the interpretation M = (D, M ) such that M xi = ui , for i = 1, . . . , n, M  Xj1 =   Uj1 , for j = 1, . . . , m, M  Xk2 = Uk2 , for k = 1, . . . , p, and which otherwise co- incides with M on all remaining variables. Throughout the paper we use the 1 abbreviations: Mz for M[z1 /u1 , . . . , zn /un ], MZ for M[Z11 /U11 , . . . , Zm 1 1 /Um ], Z2 2 2 2 2 and M for M[Z1 /U1 , . . . , Zp /Up ]. Let ϕ be a 4LQS -formula and let M = (D, M ) be a 4LQS -interpretation. The notion of satisfiability of ϕ by M (denoted by M |= ϕ) is defined inductively over the structure of the formula. Quantifier-free atomic formulae are interpreted in the standard way according to the usual meaning of the predicates ‘=’ and ‘∈’, and quantified atomic formulae are evaluated as follows: 1 We recall that, for any set s, pow(s) denotes the powerset of s, i.e., the collection of all subsets of s. 1. M |= (∀z1 ) . . . (∀zn )ϕ0 iff M[z1 /u1 , . . . , zn /un ] |= ϕ0 , for all u1 , . . . , un ∈ D; 2. M |= (∀Z11 ) . . . (∀Zm1 )ϕ1 iff M[Z11 /U11 , . . . , Zm1 /Um 1 ] |= ϕ1 , for all U11 , . . . , Um 1 ∈ pow(D); 3. M |= (∀Z12 ) . . . (∀Zp2 )ϕ2 iff M[Z12 /U12 , . . . , Zp2 /Up2 ] |= ϕ2 , for all U12 , . . . , Up2 ∈ pow(pow(D)). Finally, evaluation of compound formulae plainly follows the standard rules of propositional logic. Let ψ be a 4LQS -formula, if M |= ψ, i.e. M satisfies ψ, then M is said to be a 4LQS -model for ψ. A 4LQS -formula is said to be satisfiable if it has a 4LQS -model. A 4LQS -formula is valid if it is satisfied by all 4LQS - interpretations. 2.2 Characterizing 4LQS R 4LQS R is the subcollection of the formulae ψ of 4LQS for which the following restrictions hold. I. For every atomic formula (∀Z11 ), . . . , (∀Zm 1 )ϕ1 of level 2 occurring in ψ and every level 1 atomic formula of the form (∀z1 ) . . . (∀zn )ϕ0 occurring in ϕ1 , ϕ0 is a propositional combination of level 0 atoms and the condition n   m ¬ϕ0 → zi ∈ Zj1 (1) i=1 j=1 is a valid 4LQS -formula (in this case we say that the atom (∀z1 ) . . . (∀zn )ϕ0 is linked to the variables Z11 , . . . , Zm 1 ). II. Every atomic formula of level 3 in ψ is either of type (∀Z12 ), . . . , (∀Zp2 )ϕ2 , where ϕ2 is a propositional combination of quantifier-free atomic formulae, or of type (∀Z 2 )(Z 2 ∈ X 3 ↔ ¬(∀z1 )(∀z2 )¬(z1 , z2  = Z 2 ). Restriction (I) is similar to the one described in [7]. In particular, following [7], we recall that condition (1) guarantees that if a given interpretation assigns to z1 , . . . , zn elements of the domain that make ϕ0 false, then such elements must be contained in at least one of the sets assigned to Z11 , . . . , Zm1 . This fact is needed in the proof of statement (ii) of Lemma 5 to make sure that satisfiability is preserved in a suitable finite submodel (details, however, are not reported here and can be found in [7]). Through several examples, in [7] it is argued that condition (1) is not particu- larly restrictive. Indeed, to establish whether a given 4LQS -formula is a 4LQS R - formula, since condition (1) is a 2LS-formula, its validity can be checked using the decision procedure in [10], as 4LQS is a conservative extension of 2LS. In addition, in many cases of interest, condition (1) is just an instance of the simple propositional tautology ¬(A → B) → A, and thus its validity can be established just by inspection. Restriction (II) has been introduced to be able to express binary relations and several operations on relations keeping low, at the same time, the complexity of the decision procedure of Section 3.2. Finally, we observe that though the semantics of 4LQS R plainly coincides with the one given above for 4LQS -formulae, in what follows we prefer to refer to 4LQS -interpretations of 4LQS R -formulae as 4LQS R -interpretations. 3 The satisfiability problem for 4LQS R -formulae We will solve the satisfiability problem for 4LQS R , i.e. the problem of establish- ing for any given formula of 4LQS R whether it is satisfiable or not, as follows: (i) firstly, we will show how to reduce effectively the satisfiability problem for 4LQS R -formulae to the satisfiability problem for normalized 4LQS R - conjunctions (these will be defined below); (ii) secondly, we will prove that normalized 4LQS R -conjunctions enjoy a small model property. From (i) and (ii), the solvability of the satisfiability problem for 4LQS R follows immediately. Additionally, by further elaborating on point (i), it could easily be shown that indeed the whole collection of 4LQS R -formulae enjoys a small model property. 3.1 Normalized 4LQS R -conjunctions Let ψ be a formula of 4LQS R and let ψDN F be a disjunctive normal form of ψ. Then ψ is satisfiable if and only if at least one of the disjuncts of ψDN F is satisfiable. We recall that the disjuncts of ψDN F are conjunctions of literals, namely atomic formulae or their negation. In view of the previous observations, without loss of generality, we can suppose that our formula ψ is a conjunction of level 0, 1, 2 quantifier-free literals and of level 1, 2, 3 quantified literals. In addition, we can also assume that no variable occurs both bound and free in ψ and that distinct occurrences of quantifiers bind distinct variables. For decidability purposes, negative quantified conjuncts occurring in ψ can be removed as follows. Let M = (D, M ) be a model for ψ, and let ¬(∀z1 ) . . . (∀zn )ϕ0 be a negative quantified literal of level 1 in ψ. Since M |= ¬(∀z1 ) . . . (∀zn )ϕ0 if and only if M[z1 /u1 , . . . , zn /un ] |= ¬ϕ0 , for some u1 , . . . , un ∈ D, we can replace ¬(∀z1 ) . . . (∀zn )ϕ0 in ψ by ¬(ϕ0 )zz1 ,...,z n    , where z1 , . . . , zn are newly introduced 1 ,...,zn variables of sort 0. Negative quantified literals of levels 2 and 3 can be dealt with much in the same way and hence, we can further assume that ψ is a conjunction of literals of the following types: (1) quantifier-free literals of any level; (2) quantified atomic formulae of level 1; (3) quantified atomic formulae of levels 2 and 3 satisfying the restrictions given in Section 2.2. We call these formulae normalized 4LQS R -conjunctions. 3.2 A small model property for normalized 4LQS R -conjunctions In view of the above reductions, we can limit ourselves to consider the satisfia- bility problem for normalized 4LQS R -conjunctions only. Thus, let ψ be a normalized 4LQS R -conjunction and assume that M = (D, M ) is a model for ψ. We show how to construct, out of M, a finite 4LQS R -interpretation M∗ = (D , M ∗ ) which is a model of ψ and such that the size of D∗ depends solely on ∗ the size of ψ. We will proceed as follows. First we outline a procedure for the construction of a suitable nonempty finite universe D∗ ⊆ D. Then we show how to relativize M to D∗ according to Definition 1 below, thus defining a finite 4LQS R -interpretation M∗ = (D∗ , M ∗ ). Finally, we prove that M∗ satisfies ψ. Construction of the universe D ∗ . Let us denote by V0 , V1 , and V2 the collections of variables of sort 0, 1, and 2 occurring free in ψ, respectively. Then we construct D∗ according to the following steps: Step 1: Let F = F1 ∪ F2 , where – F1 ‘distinguishes’ the set S = {M X 2 : X 2 ∈ V2 }, in the sense that K ∩ F1 = K  ∩ F1 for every distinct K, K  ∈ S. Such a set F1 can be constructed by the procedure Distinguish described in [5]. As shown in [5], we can also assume that |F1 | ≤ |S| − 1. – F2 satisfies |M X 2 ∩ F2 | ≥ min(3, |M X 2 |), for every X 2 ∈ V2 . Plainly, we can also assume that |F2 | ≤ 3 · |V2 |. Step 2: Let {F1 , . . . , Fk } = F \{M X 1 : X 1 ∈ V1 } and let V1F = {X11 , . . . , Xk1 } ⊆ V1 be such that V1F ∩ V1 = ∅ and V1F ∩ V1B = ∅, where V1B is the collection of bound variables in ψ. Let M be the interpretation M[X11 /F1 , . . . , Xk1 /Fk ]. Since the variables in V1F do not occur in ψ (neither free nor bound), their evaluation is immaterial for ψ and therefore, from now on, we identify M and M. Step 3: Let ∆ = ∆1 ∪ ∆2 , where – ∆1 distinguishes the set T = {M X 1 : X 1 ∈ (V1 ∪V1F )} and |∆1 | ≤ |T |−1 holds (cf. Step 1 above). – ∆2 satisfies |J ∩ ∆2 | ≥ min(3, |J|), for every J ∈ {M X 1 : X 1 ∈ (V1 ∪ V1F )}. Plainly, we can assume that |∆2 | ≤ 3 · |V1 ∪ V1F |. We then initialize D∗ by putting D∗ := {M x : x in V0 } ∪ ∆ . Step 4: Let ψ1 , . . . , ψr be the conjuncts of ψ. To each conjunct ψi of the form 1 1 (∀Zi,h 1 ) . . . (∀Zi,h mi )ϕi we associate the collection ϕi,k1 , . . . , ϕi,ki of atomic formulae of the form (∀z1 ) . . . (∀zn )ϕ0 present in the matrix of ψi , and call 1 1 the variables Zi,h 1 , . . . , Zi,h m the arguments of ϕi,k1 , . . . , ϕi,ki . Let us put i Φ = {ϕi,kj : 1 ≤ j ≤ i and 1 ≤ i ≤ r}. Then, for each ϕ ∈ Φ of the form (∀z1 ) . . . (∀zn )ϕ0 having Z11 , . . . , Zm 1 as arguments, and for each ordered m-tuple (Xh1 , . . . , Xhm ) of variables in V1 ∪ 1 1 Z 1 ,..., Z 1 V1F , if M (ϕ0 )X11 ,...,Xm 1 = false we insert in D∗ elements u1 , . . . , un ∈ D h1 hm such that Z 1 ,..., Z 1 M [z1 /u1 , . . . , zn /un ](ϕ0 )X11 ,...,Xm 1 = false , h1 hm ∗ otherwise we leave D unchanged. Relativized interpretations. We introduce the notion of relativized interpre- tation, to be used together with the domain D∗ constructed above, to define, out of a model M = (D, M ) for a 4LQS R -formula ψ, a finite interpretation M∗ = (D∗ , M ∗ ) of bounded size satisfying ψ as well. Definition 1. Let M = (D, M ) be a 4LQS R -interpretation. Let D∗ , V1 , V1F , and V2 be as above, and let d∗ ∈ D∗ . The relativized interpretation of M with respect to D∗ , d∗ , V1 , V1F , and V2 , Rel(M, D∗ , d∗ , V1 , V1F , V2 ) = (D∗ , M ∗ ), is the interpretation such that  ∗ M x , if M x ∈ D∗ M x= d∗ , otherwise , M ∗ X 1 = M X 1 ∩ D∗ , M ∗ X 2 = ((M X 2 ∩ pow(D∗ )) \ {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F )}) ∪{M ∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M X 1 ∈ M X 2 } , M ∗ x, y = {{M ∗ x}, {M ∗ x, M ∗ y}} , M ∗ X 3 = ((M X 3 ∩ pow(pow(D∗ ))) \ {M ∗ X 2 : X 2 ∈ V2 }) , ∪{M ∗ X 2 : X 2 ∈ V2 , M X 2 ∈ M X 3 } . Concerning M ∗ X 2 and M ∗ X 3 , we observe that they have been defined in such a way that all the membership relations between variables of ψ of sorts 2 and 3 are the same in both the interpretations M and M∗ . This fact will be proved in the next section. For ease of notation, we will often omit the reference to the element d∗ ∈ D∗ and write simply Rel(M, D∗ , V1 , V1F , V2 ) in place of Rel(M, D∗ , d∗ , V1 , V1F , V2 ), when d∗ is clear from the context. The following useful properties are immediate consequences of the construc- tion of D∗ : (A) if M X 1 = M Y 1 , then (M X 1  M Y 1 ) ∩ D∗ = ∅,2 (B) if M X 2 = M Y 2 , there is a J ∈ (M X 2  M Y 2 ) ∩ {M X 1 : X 1 ∈ (V1 ∪ VF )} such that J ∩ D∗ = ∅, (C) if M x, y = M X 2 , there is a J ∈ (M X 2  M x, y) ∩ {M X 1 : X 1 ∈ (V1 ∪ VF )} such that J ∩ D∗ = ∅, and if J ∈ M X 2 , J ∩ D∗ = {M x} and J ∩ D∗ = {M x, M y}, 2 We recall that for any sets s and t, s  t denotes the symmetric difference of s and of t, namely the set (s \ t) ∪ (t \ s). for any x, y ∈ V0 , X 1 , Y 1 ∈ V1 , and X 2 , Y 2 ∈ V2 . 3.3 Soundness of the relativization Let M = (D, M ) be a 4LQS R -interpretation satisfying a given 4LQS R -formula ψ, and let D∗ , V1 , V1F , V2 , and M∗ be defined as above. The main result of this section is Theorem 1 which states that if M satisfies ψ, then M∗ satisfies ψ as well. The proof of Theorem 1 exploits the technical Lemmas 1, 2, 3, 4, and 5 below. In particular, Lemma 1 states that M satisfies a quantifier-free atomic formula ϕ fulfilling conditions (A), (B), and (C), if and only if M∗ satisfies ϕ too. Lemmas 2, 3, and 4 claim that suitably constructed variants of M∗ and the small models resulting by applying the construction of Section 3.2 to the corresponding variants of M can be considered identical. Finally, Lemma 5, stating that if M satisfies a quantified conjunction of ψ, then M∗ satisfies it as well, is proved by applying Lemmas 1, 2, 3, and 4. Proofs of Lemmas 1, 2, 3, and 4 are routine and can be found in Appendices A.1, A.2, A.3, and A.4, respectively. Lemma 1. The following statements hold: (a) M∗ |= x = y iff M |= x = y, for all x, y ∈ V0 such that M x, M y ∈ D∗ ; (b) M∗ |= x ∈ X 1 iff M |= x ∈ X 1 , for all X 1 ∈ V1 and x ∈ V0 such that M x ∈ D∗ ; (c) M∗ |= X 1 = Y 1 iff M |= X 1 = Y 1 , for all X 1 , Y 1 ∈ V1 such that condition (A) holds; (d) M∗ |= X 1 ∈ X 2 iff M |= X 1 ∈ X 2 , for all X 1 ∈ (V1 ∪ VF ), X 2 ∈ V2 ; (e) M∗ |= X 2 = Y 2 iff M |= X 2 = Y 2 , for all X 2 , Y 2 ∈ V2 such that condition (B) holds; (f ) M∗ |= x, y = X 2 iff M |= x, y = X 2 , for all x, y ∈ V0 such that M x, M y ∈ D∗ and X 2 ∈ V2 such that condition (C) holds; (g) M∗ |= x, y ∈ X 3 iff M |= x, y ∈ X 3 , for all x, y ∈ V0 such that M x, M y ∈ D∗ and X 2 ∈ V2 such that condition (C) holds; (h) M∗ |= X 2 ∈ X 3 iff M |= X 2 ∈ X 3 , for all x, y ∈ V0 such that M x, M y ∈ D∗ and X 2 ∈ V2 such that conditions (B) and (C) hold. 2 In view of the next technical lemmas, we introduce the following notations. Let u1 , . . . , un ∈ D∗ , U11 , . . . , Um 1 ∈ pow(D∗ ), and U12 , . . . , Up2 ∈ pow(pow(D∗ )). Then we put M∗,z = M∗ [z1 /u1 , . . . , zn /un ], 1 M∗,Z = M∗ [Z11 /U11 , . . . , Zm 1 1 /Um ], 2 M∗,Z = M∗ [Z12 /U12 , . . . , Zp2 /Up2 ], and Mz,∗ = Rel(Mz , D∗ , V1 , V1F , V2 ), 1 1 MZ ,∗ = Rel(MZ , D∗ , V1 ∪ {Z11 , . . . , Zm 1 }, V1F , V2 ), 2 2 MZ ,∗ = Rel(MZ , D∗ , F ∗ , V1 , V1F , V2 ∪ {Z12 , . . . , Zp2 }). The next three lemmas claim that, under certain conditions, the following pairs 1 1 2 of 4LQS R -interpretations M∗,z and Mz,∗ , M∗,Z and MZ ,∗ , M∗,Z and 2 MZ ,∗ can be identified. Lemma 2. Let u1 , . . . , un ∈ D∗ , and let z1 , . . . , zn ∈ V0 . Then, for every x, y ∈ V0 , X 1 ∈ V1 , X 2 ∈ V2 , X 3 ∈ V3 , we have: (i) M ∗,z x = M z,∗ x, (ii) M ∗,z X 1 = M z,∗ X 1 , (iii) M ∗,z X 2 = M z,∗ X 2 , (iv) M ∗,z X 3 = M z,∗ X 3 . 2 Lemma 3. Let Z11 , . . . , Zm 1 ∈ V1 \ (V1 ∪ V1F ) and U11 , . . . , Um 1 ∈ pow(D∗ ) \ R ∗,Z 1 1 ∗ 1 1  F {M X : X ∈ (V1 ∪V1 )}. Then, the 4LQS -interpretations M and MZ ,∗ coincide. 2 Lemma 4. Let Z12 , . . . , Zp2 ∈ V2 \V2 and U12 , . . . , Up2 ∈ pow(pow(D∗ ))\{M ∗ X 2 : 2 2 X 2 ∈ V2 }. Then the 4LQS R -interpretations M∗,Z and MZ ,∗ coincide. 2 The following lemma proves that satisfiability is preserved in the case of quan- tified atomic formulae. Lemma 5. Let (∀z1 ) . . . (∀zn )ϕ0 , (∀Z11 ) . . . (∀Zm 1 )ϕ1 , (∀Z12 ) . . . (∀Zp2 )ϕ2 , and 2 2 3 2 (∀Z )(Z ∈ X ↔ ¬(∀z1 , z2 )¬(z1 , z2  = Z )) be conjuncts of ψ. Then (i) if M |= (∀z1 ) . . . (∀zn )ϕ0 , then M∗ |= (∀z1 ) . . . (∀zn )ϕ0 ; (ii) if M |= (∀Z1 ) . . . (∀Zm )ϕ1 , then M∗ |= (∀Z1 ) . . . (∀Zm )ϕ1 ; (iii) if M |= (∀Z12 ) . . . (∀Zp2 )ϕ2 , then M∗ |= (∀Z12 ) . . . (∀Zp2 )ϕ2 ; (iv) if M |= (∀Z 2 )(Z 2 ∈ X 3 ↔ ¬(∀z1 , z2 )¬(z1 , z2  = Z 2 )), then M∗ |= (∀Z 2 )(Z 2 ∈ X 3 ↔ ¬(∀z1 , z2 )¬(z1 , z2  = Z 2 )). Proof. (i) Assume by contradiction that there exist u1 , . . . , un ∈ D∗ such that M∗,z |= ϕ0 . Then, there must be an atomic formula ϕ0 in ϕ0 that is inter- preted differently in M∗,z and in Mz . Recalling that ϕ0 is a propositional combination of quantifier-free atomic formulae of any level, we can suppose that ϕ0 is X 2 = Y 2 and, without loss of generality, assume that M∗,z |= X 2 = Y 2 . Then M ∗,z X 2 = M ∗,z Y 2 , so that, by Lemma 2, M z,∗ X 2 = M z,∗ Y 2 . Then, Lemma 1 yields M z X 2 = M z Y 2 , a contradiction. The other cases are proved in an analogous way. (ii) This case can proved much along the same lines as the proof of case (ii) of Lemma 4 in [7]. Here, one has only to take care of the fact that the collection of relevant variables of sort 1 for ψ are not just the variables occurring free in ψ, namely the ones in V1 , but also the variables in V1F , introduced to denote the elements distinguishing the sets M ∗ X 2 , for X 2 ∈ V2 . (iii) The proof is carried out as in case (ii). (iv) Assume by contradiction that there exists a U ∈ pow(pow(D∗ )) such that 2 M∗,Z |= (Z 2 ∈ X 3 ↔ ¬(∀z1 , z2 )¬(z1 , z2  = Z 2 )). We can distinguish two cases: 1. If there is a X 2 ∈ V2 such that M ∗ X 2 = U , then M∗ |= (X 2 ∈ X 3 ↔ ¬(∀z1 , z2 )¬(z1 , z2  = X 2 )) and either X 2 ∈ X 3 or ¬(∀z1 , z2 )¬(z1 , z2  = X 2 ) must be interpreted differently in M∗ and in M. By Lemma 1, X 2 ∈ X 3 is interpreted in the same way in M∗ and in M. By case (i) of this lemma, if M∗ |= ¬(∀z1 , z2 )¬(z1 , z2  = X 2 ) then M |= ¬(∀z1 , z2 )¬(z1 , z2  = X 2 ). Thus, the only case to be con- sidered is when M∗ |= (∀z1 , z2 )¬(z1 , z2  = X 2 ). Assume that M |= ¬(∀z1 , z2 )¬(z1 , z2  = X 2 ). Then M X 2 must be a pair {{u}, {u, v}}, for some u, v ∈ D. But then by the construction of the universe D∗ , we have u, v ∈ D∗ , contradicting the hypothesis that M∗ |= (∀z1 , z2 )¬(z1 , z2  = X 2 ). 2. If U = M ∗ X 2 , for every X 2 ∈ V2 , either Z 2 ∈ X 3 or ¬(∀z1 , z2 )¬(z1 , z2  = 2 2 Z 2 ) has to be interpreted in a different way in M∗,Z and in MZ . By Lemmas 4 and 1, and by case (i) of this lemma, Z 2 ∈ X 3 has the same 2 2 2 evaluation in M∗,Z and in MZ , and if M∗,Z |= ¬(∀z1 , z2 )¬(z1 , z2  = 2 Z 2 ) then MZ |= ¬(∀z1 , z2 )¬(z1 , z2  = Z 2 ). The only case that still 2 has to be analyzed is when M∗,Z |= (∀z1 , z2 )¬(z1 , z2  = Z 2 ). By 2 Lemma 4, MZ ,∗ |= (∀z1 , z2 )¬(z1 , z2  = Z 2 ). Let us assume that 2 MZ |= (∀z1 , z2 )¬(z1 , z2  = Z 2 ). Then U must be a pair {{u}, {u, v}}, u, v ∈ D. Since U ∈ pow(pow(D∗ )), then u, v ∈ D∗ , contradicting that 2 MZ ,∗ |= (∀z1 , z2 )¬(z1 , z2  = Z 2 ). Next, we can state our main result. Theorem 1. Let M be a 4LQS R -interpretation satisfying ψ. Then M∗ |= ψ. Proof. We have to prove that M∗ |= ψ  for each literal ψ  occurring in ψ. Each ψ  must be of one of the types introduced in Section 3.1. By applying Lemmas 1 or 5 to every ψ  (according to its type) we obtain the thesis. From the above reduction and relativization steps, it is not hard to derive the following result: Corollary 1. The fragment 4LQS R enjoys a small model property (and there- fore its satisfiability problem is solvable). 2 3.4 Complexity issues Let (4LQS R )k be the sublanguage of 4LQS R in which the quantifier prefixes of quantified atoms of level 2 have length not exceeding k. Then the following result holds. Lemma 6. The satisfiability problem for (4LQS R )k is NP-complete, for any k ∈ N. Proof. NP-hardness is trivially proved by reducing an instance of the satisfiabil- ity problem of propositional logic to our problem. To prove that our problem is in NP, we reason as follows. Let ϕ be a satisfiable (4LQS R )k -formula. Let ϕDN F be a disjunctive normal form of ϕ. Then there is a disjunct ψ of ϕDN F that is satisfied by a (4LQS R )k -interpretation M = (D, M ). After the normalization step, ψ is a normalized (4LQS R )k -conjunction satisfied by M and, according to the procedure of Section 3.2, we can construct a small interpretation M∗ = (D∗ , M ∗ ) satisfying ψ and such that |D∗ | is polynomial in the size of ψ. This can be shown by recalling that |F1 | ≤ |S| − 1 ≤ |V2 | − 1 and that |F2 | ≤ 3|V2 | (cf. Step 1 of the procedure in Section 3.2). Thus, clearly, |F | ≤ 4|V2 | − 1. Analogously, from Step 3, |∆| ≤ 4(|V1 | + (4|V2 | − 1)) − 1, and |D∗ | (in the initialization phase) is bounded by |V0 | + 4|V1 | + 16|V2 | − 5. Finally, after Step 4, if we let Ln denote the maximal length of the quantifier prefix of ϕ = (∀z1 ) . . . (∀zn )ϕ0 , with ϕ varying in Φ, then |D∗ | ≤ |V0 | + 4|V1 | + 16|V2 | − 5 + ((|V1 | + 4|V2 | − 1)k Ln )|Φ|. Thus the size of D∗ is polynomial in the size of ψ. Since M∗ |= ψ can be verified in polynomial time and the size of ψ is polynomial w.r.t. the size of ϕ, it results that the satisfiability problem for (4LQS R )k is in NP, and therefore it is NP-complete. 4 Expressiveness of the language 4LQS R As discussed in [7], 4LQS R can express a restricted variant of the set former, which in turn allows to express other significant set operators such as binary union, intersection, set difference, the singleton operator, the powerset operator (over subsets of the universe only), etc. More specifically, atomic formulae of type X 1 = {z : ϕ(z)} or X i = {X i−1 : ϕ(X i−1 )}, for i ∈ {2, 3}, can be expressed in 4LQS R by the formulae (∀z)(z ∈ X 1 ↔ ϕ(z)) (2) (∀X i−1 )(X i−1 ∈ X i ↔ ϕ(X i−1 )) (3) provided that they satisfy the syntactic constraints of 4LQS R . Since 4LQS R is a superlanguage of 3LQS R , as shown in [7] 4LQS R can ex- press the stratified syllogistic 2LS and the sublanguage 3LSSP of 3LSSP U not involving the set-theoretic construct of general union. We recall that 3LSSP U admits variables of three sorts and, besides the usual set-theoretical constructs, it involves the ‘singleton set’ operator {·}, the powerset operator pow, and the general union operator Un. 3LSSP can plainly be decided by the decision procedure presented in [3] for the whole 3LSSP U . Other constructs of set theory which are expressible in the 4LQS R formalism, as shown in [7], are: Binary relation (∀Z 2 )(Z 2 ∈ R3 ↔ ¬(∀z1 , z2 )¬(z1 , z2  = Z 2 )) Reflexive (∀z1 )(z1 , z1  ∈ R3 ) Symmetric (∀z1 , z2 )(z1 , z2  ∈ R3 → z2 , z1  ∈ R3 ) Transitive (∀z1 , z2 , z3 )((z1 , z2  ∈ R3 ∧ z2 , z3  ∈ R3 ) → z1 , z3  ∈ R3 ) Euclidean (∀z1 , z2 , z3 )((z1 , z2  ∈ R3 ∧ z1 , z3  ∈ R3 ) → z2 , z3  ∈ R3 ) Weakly-connected (∀z1 , z2 , z3 )((z1 , z2  ∈ R3 ∧ z1 , z3  ∈ R3 ) → (z2 , z3  ∈ R3 ∨ z2 = z3 ∨ z3 , z2  ∈ R3 )) Irreflexive (∀z1 )¬(z1 , z1  ∈ R3 ) Intransitive (∀z1 , z2 , z3 )((z1 , z2  ∈ R3 ∧ z2 , z3  ∈ R3 ) → ¬z1 , z3  ∈ R3 ) Antisymmetric (∀z1 , z2 )((z1 , z2  ∈ R3 ∧ z2 , z1  ∈ R3 ) → (z1 = z2 )) Asymmetric (∀z1 , z2 )(z1 , z2  ∈ R3 → ¬(z2 , z1  ∈ R3 )) Table 1. 4LQS R formalization of conditions of accessibility relations Intersection R3 = R13 ∩ R23 (∀Z 2 )(Z 2 ∈ R3 ↔ (Z 2 ∈ R13 ∧ Z 2 ∈ R23 )) Union R3 = R13 ∪ R23 (∀Z 2 )(Z 2 ∈ R3 ↔ (Z 2 ∈ R13 ∨ Z 2 ∈ R23 )) Complement R13 = R23 (∀Z 2 )(Z 2 ∈ R13 ↔ ¬(Z 2 ∈ R23 )) Set difference R = R1 \ R2 (∀Z 2 )(Z 2 ∈ R3 ↔ (Z 2 ∈ R13 ∧ ¬(Z 2 ∈ R23 ))) 3 3 3 Set inclusion R13 ⊆ R23 (∀Z 2 )(Z 2 ∈ R13 → Z 2 ∈ R23 ) Table 2. 4LQS R formalization of Boolean operations over relations – the literal X 2 = pow≤h (X 1 ), where pow≤h (X 1 ) denotes the collection of all the subsets of X 1 having at most h elements; – the literal X 2 = pow=h (X 1 ), where pow=h (X 1 ) denotes the collection of subsets of X 1 with exactly h elements; – the unordered Cartesian product X 2 = X11 ⊗ . . . ⊗ Xn1 ; – the literal A = pow∗ (X11 , . . . , Xn1 ), where pow∗ (X11 , . . . , Xn1 ) is a variant of the powerset which denotes the collection n  {Z : Z ⊆ Xi1 and Z ∩ Xi1 = ∅, for all 1 ≤ i ≤ n} i=1 introduced in [1]. 4.1 Other applications of 4LQS R Within the 4LQS R language it is also possible to define binary relations over elements of a domain together with several conditions on them which character- ize accessibility relations of well-known modal logics. These formalizations are illustrated in Table 1. Usual Boolean operations over relations can be defined as shown in Table 2. Within the 4LQS R fragment it is also possible to define the inverse of a given binary relation R13 , namely R23 = (R13 )−1 , by means of the 4LQS R -formula (∀z1 , z2 )(z1 , z2  ∈ R13 ↔ z2 , z1  ∈ R23 ). In the next section we will show how the 4LQS R fragment can be used to formalize some normal modal logics. 4.2 Some normal modal logics expressible in 4LQS R The modal language LM is based on a countably infinite set of propositional letters P = {p1 , p2 , . . .}, the classical propositional connectives ‘¬’, ‘∧’ , and ‘∨’, the modal operators ‘’, ‘♦’ (and the parentheses). LM is the smallest set such that P ⊆ LM , and such that if ϕ, ψ ∈ LM , then ¬ϕ, ϕ ∧ ψ, ϕ ∨ ψ, ϕ, ♦ϕ ∈ LM . Lower case letters like p denote elements of P and Greek letters like ϕ and ψ represent formulae of LM . Given a formula ϕ of LM , we indicate with SubF (ϕ) the set of the subformulae of ϕ. The modal depth of a formula ϕ is the maximum nesting depth of modalities occurring in ϕ. A normal modal logic is any subset of LM which contains all the tautologies and the axiom K : (p1 → p2 ) → (p1 → p2 ) , and which is closed with respect to modus ponens, substitution, and necessitation (the reader may consult a text on modal logic like [9] for more details). A Kripke frame is a pair W, R such that W is a nonempty set of possible worlds and R is a binary relation on W called accessibility relation. If R(w, u) holds, we say that the world u is accessible from the world w. A Kripke model is a triple W, R, h, where W, R is a Kripke frame and h is a function mapping propositional letters into subsets of W . Thus, h(p) is the set of all the worlds where p is true. Let K = W, R, h be a Kripke model and let w be a world in K . Then, for every p ∈ P and for every ϕ, ψ ∈ LM , the relation of satisfaction |= is defined as follows: – K , w |= p iff w ∈ h(p); – K , w |= ϕ ∨ ψ iff K , w |= ϕ or K , w |= ψ; – K , w |= ϕ ∧ ψ iff K , w |= ϕ and K , w |= ψ; – K , w |= ¬ϕ iff K , w |= ϕ; – K , w |= ϕ iff K , w |= ϕ, for every w ∈ W such that (w, w ) ∈ R; – K , w |= ♦ϕ iff there is a w ∈ W such that (w, w ) ∈ R and K , w |= ϕ. A formula ϕ is said to be satisfied at w in K if K , w |= ϕ; ϕ is said to be valid in K (and we write K |= ϕ), if K , w |= ϕ, for every w ∈ W . The smallest normal modal logic is K, which contains only the modal axiom K and whose accessibility relation R can be any binary relation. The other normal modal logics admit together with K other modal axioms drawn from the ones in Table 3. Translation of a normal modal logic into the 4LQS R language is based on the semantics of propositional and modal operators. For any normal modal logic, the formalization of the semantics of modal operators depends on the axioms that characterize the logic. In the case of the logics S5 and K45, proved to be NP-complete in [11], and introduced next, the 4LQS R formalization of the modal formulae ϕ and ♦ϕ turns out to be straightforward and thus these logics can be entirely translated into the 4LQS R language. This is illustrated in what follows. Axiom Schema Condition on R (see Table 1) T p → p Reflexive 5 ♦p → ♦p Euclidean B p → ♦p Symmetric 4 p → p Transitive D p → ♦p Serial: (∀w)(∃u)R(w, u) Table 3. Axioms of normal modal logics The logic S5. Modal logic S5 is the strongest normal modal system. It can be obtained from the logic K in several ways. One of them consists in adding axioms T and 5 from Table 3 to the logic K. Given a formula ϕ, a Kripke model K = W, R, h, and a world w ∈ W , the semantics of the modal operators can be defined as follows: – K , w |= ϕ iff K , v |= ϕ, for every v ∈ W , – K , w |= ♦ϕ iff K , v |= ϕ, for some v ∈ W . This makes it possible to translate a formula ϕ of S5 into the 4LQS R language. For the purpose of simplifying the definition of the translation function τS5 given below, the concept of “empty formula” is introduced, to be denoted by Λ, and not interpreted in any particular way. The only requirement on Λ needed for the definition given next is that Λ ∧ ψ and ψ ∧ Λ are to be considered as syntactic variations of ψ, for any 4LQS R -formula ψ. 1 For every propositional letter p, let τS5 (p) = Xp1 , where Xp1 ∈ V1 , and let 2 R τS5 : S5 → 4LQS be the function defined recursively as follows: 2 – τS5 (p) = Λ, 2 1 – τS5 (¬ϕ) = (∀z)(z ∈ X¬ϕ ↔ ¬(z ∈ Xϕ1 )) ∧ τS5 2 (ϕ), 2 – τS5 (ϕ1 ∧ ϕ2 ) = (∀z)(z ∈ Xϕ1 1 ∧ϕ2 ↔ (z ∈ Xϕ1 1 ∧ z ∈ Xϕ1 2 )) ∧ τS5 2 2 (ϕ1 ) ∧ τS5 (ϕ2 ), 2 – τS5 (ϕ1 ∨ ϕ2 ) = (∀z)(z ∈ Xϕ1 1 ∨ϕ2 ↔ (z ∈ Xϕ1 1 ∨ z ∈ Xϕ1 2 )) ∧ τS5 2 2 (ϕ1 ) ∧ τS5 (ϕ2 ), 2 – τS5 (ϕ) = (∀z)(z ∈ Xϕ1 ) → (∀z)(z ∈ Xϕ 1 ) ∧ ¬(∀z)(z ∈ Xϕ1 ) → (∀z)¬(z ∈ 1 2 Xϕ ) ∧ τS5 (ϕ), 2 – τS5 (♦ϕ) = ¬(∀z)¬(z ∈ Xϕ1 ) → (∀z)(z ∈ X♦ϕ 1 ) ∧ (∀z)¬(z ∈ Xϕ1 ) → (∀z)¬(z ∈ 1 2 X♦ϕ ) ∧ τS5 (ϕ), 1 where Λ is the empty formula and X¬ϕ , Xϕ1 , Xϕ1 1 ∧ϕ2 , Xϕ1 1 ∨ϕ2 , Xϕ1 1 , Xϕ1 2 ∈ V1 . Finally, for every ϕ in S5, if ϕ is a propositional letter in P we put τS5 (ϕ) = 1 2 τS5 (ϕ), otherwise τS5 (ϕ) = τS5 (ϕ). Even though the accessibility relation R is not used in the translation, we can give its formalization in the 4LQS R fragment. Let U be defined so that (∀z)(z ∈ U ), then R can be defined in the following two ways: 1. as a variable of sort 2, R2 , such that (∀Z 1 )(Z 1 ∈ R2 ↔ (Z 1 ∈ pow=1 (U ) ∨ Z 1 ∈ pow=2 (U ))) , 2. as a variable of sort 3, R3 , such that (∀Z 2 )(Z 2 ∈ R3 ↔ ¬(∀z1 , z2 )¬(z1 , z2  = Z 2 )) ∧ (∀z1 )(z1 , z1  ∈ R3 ) ∧(∀z1 , z2 , z3 )((z1 , z2  ∈ R3 ∧ z1 , z3  ∈ R3 ) → z2 , z3  ∈ R3 ). Correctness of the above translation is guaranteed by the following lemma, whose proof can be found in Appendix A.5. Lemma 7. For every formula ϕ of the logic S5, ϕ is satisfiable in a model K = W, R, h iff there is a 4LQS R -interpretation satisfying x ∈ Xϕ . 2 It can be checked that τS5 (ϕ) is polynomial in the size of ϕ and that its sat- isfiability can be verified in nondeterministic polynomial time since it belongs to (4LQS R )1 . Consequently, the decision algorithm presented in this paper to- gether with the translation function introduced above can be considered an op- timal procedure (in terms of its computational complexity class) to decide the satisfiability of any formula ϕ of S5. Moreover, it can be noticed that if we apply the first definition of R, S5 can be expressed by the language 3LQS R presented in [7]. The logic K45. The normal modal logic K45 is obtained from the logic K by adding axioms 4 and 5 described in Table 3 to K. Semantics of the modal operators  and ♦ for the logic K45 can be described as follows. Given a formula ϕ of K45 and a Kripke model K = W, R, h, – K |= ϕ iff K , v |= ϕ, for every v ∈ W s.t. there is a w ∈ W with (w , v) ∈ R, – K |= ♦ϕ iff K , v |= ϕ, for some v ∈ W s.t. there is a w ∈ W with (w , v) ∈ R. It is convenient, before translating K45 into the 4LQS R fragment, to introduce the 4LQS R -formula which describes the semantics of the accessibility relation R of the logic K45: (∀Z 2 )(Z 2 ∈ R3 ↔ ¬(∀z1 )(∀z2 )¬(z1 , z2  = Z 2 )) ∧(∀z1 , z2 , z3 )((z1 , z2  ∈ R3 ∧ z2 , z3  ∈ R3 ) → z1 , z3  ∈ R3 ) ∧(∀z1 , z2 , z3 )((z1 , z2  ∈ R3 ∧ z1 , z3  ∈ R3 ) → z2 , z3  ∈ R3 ). The transformation function τK45 : K45 → 4LQS R is constructed as for S5. 1 For every ϕ ∈ K45 we put τK45 (ϕ) = τK45 (ϕ), if ϕ is a propositional letter and τK45 (ϕ) = τK45 (ϕ) otherwise. τK45 (p) = Xp1 , with Xp1 ∈ V1 , for every propositional 2 1 2 letter p, and τK45 (ϕ) is defined inductively over the structure of ϕ. We report 2 the definition of τK45 (ϕ) only when ϕ = ψ and ϕ = ♦ψ, as the other cases are 2 identical to τS5 (ϕ), defined in the previous section: 2 – τK45 (ψ) = (∀z1 )((¬(∀z2 )¬(z2 , z1  ∈ R3 )) → z1 ∈ Xψ1 ) → (∀z)(z ∈ Xψ 1 ) 3 1 ∧¬(∀z1 )¬((¬(∀z2 )¬(z2 , z1  ∈ R )) ∧ ¬(z1 ∈ Xψ )) → (∀z)¬(z ∈ 1 2 Xψ ) ∧ τK45 (ψ); 2 – τK45 (♦ψ) = ¬(∀z1 )¬((¬(∀z2 )¬(z2 , z1  ∈ R3 )) ∧ z1 ∈ Xψ1 ) → (∀z)(z ∈ X♦ψ 1 ) 3 1 1 2 ∧(∀z1 )(((∀z2 )¬(z2 , z1  ∈ R )) ∨ ¬(z1 ∈ Xψ ))) → (∀z)¬(z ∈ X♦ψ ) ∧ τK45 (ψ). The following lemma, proved in Appendix A.6, shows the correctness of the translation. Lemma 8. For every formula ϕ of the logic τK45 , ϕ is satisfiable in a model K = W, R, h iff there is a 4LQS R -interpretation satisfying x ∈ Xϕ . 2 As for S5, it can be checked that τK45 (ϕ) is polynomial in the size of ϕ and that its satisfiability can be verified in nondeterministic polynomial time since it belongs to the sublanguage (4LQS R )1 of 4LQS R . Thus, the decision algorithm we have presented and the translation function introduced above represent an optimal procedure (in terms of its computational complexity class) to decide satisfiability of any formula ϕ of K45. 5 Conclusions We have presented a decidability result for the satisfiability problem for the fragment 4LQS R of multi-sorted stratified syllogistic embodying variables of four sorts and a restricted form of quantification. As the semantics of the modal formulae ϕ and ♦ϕ in the modal logics S5 and K45 can be easily formalized in 4LQS R , it follows that 4LQS R can express both logics S5 and K45. Currently, in the case of modal logics characterized by having a liberal ac- cessibility relation like K, we are not able to translate the modal formulae ϕ and ♦ϕ in 4LQS R . The same problem concerns also the composition operation on binary relations and the set-theoretical operation of general union. We intend to investigate such a question more in depth and verify whether a formalization of these constructs is still possible in 4LQS R or if an extension of the language 4LQS R is required. In the same direction, we aim at finding a characterization of the conditions that an accessibility relation has to fulfil in order for a modal logic to be formalized in 4LQS R . We also intend to find classes of modal formulae with bounded modal nesting and multi-modal logics that can be embedded in the 4LQS R framework. Finally, since 4LQS R is able to express Boolean opera- tions on relations, we plan to investigate the possibility of translating fragments of Boolean modal logics into 4LQS R . References 1. D. Cantone. Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operators. Journal of Automated Reasoning, volume 7, number 2, pages 193–230, Kluwer Academic Publishers, Hingham, MA, USA, 1991. 2. D. Cantone and V. Cutello. A decidable fragment of the elementary theory of relations and some applications. In ISSAC ’90: Proceedings of the international symposium on Symbolic and algebraic computation, pages 24–29, New York, NY, USA, 1990. ACM Press. 3. D. Cantone and V. Cutello. Decision procedures for stratified set-theoretic syllo- gistics. In Manuel Bronstein, editor, Proceedings of the 1993 International Sym- posium on Symbolic and Algebraic Computation, ISSAC’93 (Kiev, Ukraine, July 6-8, 1993), pages 105–110, New York, 1993. ACM Press. 4. D. Cantone, V. Cutello, and J. T. Schwartz. Decision problems for Tarski and Presburger arithmetics extended with sets. In CSL ’90: Proceedings of the 4th Workshop on Computer Science Logic, pages 95–109, London, UK, 1991. Springer- Verlag. 5. D. Cantone and A. Ferro Techniques of computable set theory with applications to proof verification. Comm. Pure Appl. Math., pages 901–945, vol. XLVIII, 1995. Wiley. 6. D. Cantone, A. Ferro, and E. Omodeo. Computable set theory. Clarendon Press, New York, NY, USA, 1989. 7. D. Cantone and M. Nicolosi Asmundo. On the satisfiability problem for a 3-level quantified syllogistic. In Proceedings of CEDAR’08”. Sydney, Australia, 11 August, 2008. 8. D. Cantone, E. Omodeo, and A.Policriti. Set Theory for Computing - From deci- sion procedures to declarative programming with sets. Springer-Verlag, Texts and Monographs in Computer Science, 2001. 9. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, Cambridge Tracts in Theoretical Computer Science, 2001. 10. A. Ferro and E.G. Omodeo. An efficient validity test for formulae in extensional two-level syllogistic. Le Matematiche, 33:130–137, 1978. 11. R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal of Computing, 6: 467-480, 1977. A Proofs of some lemmas A.1 Proof of Lemma 1 Lemma 1. The following statements hold: (a) M∗ |= x = y iff M |= x = y, for all x, y ∈ V0 such that M x, M y ∈ D∗ ; (b) M∗ |= x ∈ X 1 iff M |= x ∈ X 1 , for all X 1 ∈ V1 and x ∈ V0 such that M x ∈ D∗ ; (c) M∗ |= X 1 = Y 1 iff M |= X 1 = Y 1 , for all X 1 , Y 1 ∈ V1 such that condition (A) holds; (d) M∗ |= X 1 ∈ X 2 iff M |= X 1 ∈ X 2 , for all X 1 ∈ (V1 ∪ VF ), X 2 ∈ V2 ; (e) M∗ |= X 2 = Y 2 iff M |= X 2 = Y 2 , for all X 2 , Y 2 ∈ V2 such that condition (B) holds; (f ) M∗ |= x, y = X 2 iff M |= x, y = X 2 , for all x, y ∈ V0 such that M x, M y ∈ D∗ and X 2 ∈ V2 such that condition (C) holds; (g) M∗ |= x, y ∈ X 3 iff M |= x, y ∈ X 3 , for all x, y ∈ V0 such that M x, M y ∈ D∗ and X 2 ∈ V2 such that condition (C) holds; (h) M∗ |= X 2 ∈ X 3 iff M |= X 2 ∈ X 3 , for all x, y ∈ V0 such that M x, M y ∈ D∗ and X 2 ∈ V2 such that conditions (B) and (C) hold. Proof. (a) Let x, y ∈ V0 be such that M x, M y ∈ D∗ . Then M ∗ x = M x and M ∗ y = M y, so we have immediately that M∗ |= x = y iff M |= x = y. (b) Let X 1 ∈ V1 and let x ∈ V0 be such that M x ∈ D∗ . Then M ∗ x = M x, so that M ∗ x ∈ M ∗ X 1 iff M x ∈ M X 1 ∩ D∗ iff M x ∈ M X 1 . (c) If M X 1 = M Y 1 , then plainly M ∗ X 1 = M ∗ Y 1 . On the other hand, if M X 1 = M Y 1 , then, by condition (A), (M X 1  M Y 1 ) ∩ D∗ = ∅ and thus M ∗ X 1 = M ∗Y 1. (d) If M X 1 ∈ M X 2 , then M ∗ X 1 ∈ M ∗ X 2 . On the other hand, suppose by contradiction that M X 1 ∈ / M X 2 and M ∗ X 1 ∈ M ∗ X 2 . Then, there must necessarily be a Z ∈ (V1 ∪ V1F ) with M Z 1 ∈ M X 2 , M Z 1 = M X 1 , and 1  M ∗ X 1 = M ∗ Z 1 . Since M Z 1 = M X 1 and (M Z 1  M X 1 ) ∩ D∗ = ∅, by condition (A), we have M ∗ X 1 = M ∗ Z 1 , which is a contradiction. (e) If M X 2 = M Y 2 , then M ∗ X 2 = M ∗ Y 2 . On the other hand, if M X 2 = M Y 2 , by condition (B), there is a J ∈ (M X 2  M Y 2 ) ∩ {M X 1 : X 1 ∈ (V1 ∪ V1F )} such that J ∩ D∗ = ∅. Let J = M X 1 , for some X 1 ∈ (V1 ∪ V1F ), and suppose without loss of generality that M X 1 ∈ M X 2 and M X 1 ∈ / M Y 2 . Then, by ∗ 1 ∗ 2 ∗ 1 (d), M X ∈ M X and M X ∈ / M Y and hence M X = M ∗ Y 2 . ∗ 2 ∗ 2 (f) If M x, y = M X , then M x, y = M ∗ X 2 . If M x, y = M X 2 , then 2 ∗ there is a J ∈ (M X 2  M x, y) ∩ {M X 1 : X 1 ∈ (V1 ∪ V1F )} satisfying the constraints of condition (C). Let J = M X 1 , for some X 1 ∈ (V1 ∪ V1F ), and suppose that M X 1 ∈ M X 2 and M X 1 ∈ / M x, y. Then M ∗ X 1 ∈ M ∗ X 2 and since M X = {M x} and M X = {M x, M y}, it follows that M ∗ X 1 ∈ ∗ 1 ∗ 1 / M ∗ x, y. On the other hand, if M X 1 ∈ M x, y and M X 1 ∈ / M X 2 , then either M X 1 = {M x} or M X 1 = {M x, M y}. In both cases M X 1 = M ∗ X 1 and thus if M X 1 ∈ / M X 2 , it plainly follows that M ∗ X 1 ∈ / M ∗X 2 . (g) Let x, y ∈ V0 and X 3 ∈ V3 be such that M x, y ∈ M X 3 . Then M ∗ x, y ∈ M ∗ X 3 . On the other hand, suppose by contradiction that M x, y ∈ / M X3 and M x, y ∈ M X . Then, there must be an X ∈ V2 such that M ∗ X 2 ∈ ∗ ∗ 3 2  M ∗ X 3 , M ∗ X 2 = M ∗ x, y, and M X 2 = M x, y. But this is impossible by (f). (h) If M X 2 ∈ M X 3 then M ∗ X 2 ∈ M ∗ X 3 . Now suppose by contradiction that M X2 ∈ / M X 3 and that M ∗ X 2 ∈ M ∗ X 3 . Then, either there is a Y 2 ∈ V2 such that M X 2 = M Y 2 and M ∗ X 2 = M ∗ Y 2 , which is not possible by (e), or there is a x, y, with x, y ∈ V0 , M x, M y ∈ D∗ , such that M X 2 = M x, y and M ∗ X 2 = M ∗ x, y, but this is absurd by (f). A.2 Proof of Lemma 2 Lemma 2. Let u1 , . . . , un ∈ D∗ , and let z1 , . . . , zn ∈ V0 . Then, for every x, y ∈ V0 , X 1 ∈ V1 , X 2 ∈ V2 , X 3 ∈ V3 , we have: (i) M ∗,z x = M z,∗ x, (ii) M ∗,z X 1 = M z,∗ X 1 , (iii) M ∗,z X 2 = M z,∗ X 2 , (iv) M ∗,z X 3 = M z,∗ X 3 . Proof. (i) Since u1 , . . . , un ∈ D∗ , the thesis follows immediately. (ii) Let X 1 ∈ V1 , then M ∗,z X 1 = M ∗ X 1 = M X 1 ∩D∗ = M z X 1 ∩D∗ = M z,∗ X 1 . (iii) Let X 2 ∈ V2 , then we have the following equalities: M ∗,z X 2 = M ∗ X 2 = ((M X 2 ∩ pow(D∗ )) \ {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F )}) ∪ {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M X 1 ∈ M X 2 } , = ((M z X 2 ∩ pow(D∗ )) \ {M z,∗ X 1 : X 1 ∈ (V1 ∪ V1F )}) ∪ {M z,∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M z X 1 ∈ M z X 2 } = M X2 .z,∗ (iv) Let X 3 ∈ V3 , then the following holds: M ∗,z X 3 = M ∗ X 3 = ((M X 3 ∩ pow(pow(D∗ ))) \ {M ∗ X 2 : X 2 ∈ V2 }) ∪ {M ∗ X 2 : X 2 ∈ V2 , M X 2 ∈ M X 3 } , = ((M z X 3 ∩ pow(pow(D∗ ))) \ {M z,∗ X 2 : X 2 ∈ V2 }) ∪ {M z,∗ X 2 : X 2 ∈ V2 , M z X 2 ∈ M z X 3 } = M z,∗ X 3 . A.3 Proof of Lemma 3 Lemma 3. Let Z11 , . . . , Zm 1 ∈ V1 \ (V1 ∪ V1F ) and U11 , . . . , Um 1 ∈ pow(D∗ ) \ 1 1 {M ∗ X 1 : X 1 ∈ (V1 ∪V1F )}. Then, the 4LQS R -interpretations M∗,Z and MZ ,∗ coincide. 1 1 Proof. We prove the lemma by showing that M∗,Z and MZ ,∗ agree over vari- ables of all sorts. 1 1 1. Clearly M ∗,Z x = M ∗ x = M Z ,∗ x, for all individual variables x ∈ V0 . 2. Let X 1 ∈ V1 . If X 1 ∈ / {Z11 , . . . , Zm 1 }, then 1 1 1 M Z ,∗ X 1 = M Z X 1 ∩ D∗ = M X 1 ∩ D∗ = M ∗ X 1 = M ∗,Z X 1 . On the other hand, if X 1 = Zj1 for some j ∈ {1, . . . , m}, we have 1 1 1 M Z ,∗ Zj1 = M Z Zj1 ∩ D∗ = Uj1 ∩ D∗ = Uj1 = M ∗,Z Zj1 . 3. Let X 2 ∈ V2 . Then we have 1 M ∗,Z X 2 = M ∗ X 2 = ((M X 2 ∩ pow(D∗ )) \ {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F )}) ∪ {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M X 1 ∈ M X 2 } , 1 1 M Z ,∗ X 2 = ((M Z X 2 ∩ pow(D∗ )) 1 \{M Z ,∗ X 1 : X 1 ∈ ((V1 ∪ V1F ) ∪ {Z11 , . . . , Zm 1 })}) 1 ∪{M Z ,∗ X 1 : X 1 ∈ ((V1 ∪ V1F ) ∪ {Z11 , . . . , Zm 1 }), 1 1 M Z X 1 ∈ M Z X 2} = ((M X 2 ∩ pow(D∗ )) \({M ∗ X 1 : X 1 ∈ (V1 ∪ V1F )} ∪ {Uj : j = 1, . . . , m})) ∪({M ∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M X 1 ∈ M X 2 } ∪({Uj : j = 1, . . . , m} ∩ M X 2 )) . By putting P1 = M X 2 ∩ pow(D∗ ), P2 = {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F )}, P3 = {Uj : j = 1, . . . , m}, P4 = {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M X 1 ∈ M X 2 }, P5 = {Uj : j = 1, . . . , m} ∩ M X 2 , the above relations can be rewritten as 1 M ∗,Z X 2 = (P1 \ P2 ) ∪ P4 1 M Z ,∗ X 2 = (P1 \ (P2 ∪ P3 )) ∪ P4 ∪ P5 . Moreover, it is easy to verify that the following relations hold: P2 ∩ P3 = ∅ P5 = P1 ∩ P3 P4 ⊆ P2 . Therefore we have (P1 \ P2 ) ∪ P4 = (P1 \ (P2 ∪ P3 )) ∪ P4 ∪ (P1 ∩ P3 ) = (P1 \ (P2 ∪ P3 )) ∪ P4 ∪ P5 1 1 i.e., we have M ∗,Z X 2 = M Z ,∗ X 2 . 1 4. Let X 3 ∈ V3 , then M ∗,Z X 3 = M ∗ [Z11 /U11 , . . . , Zm 1 1 /Um ]X 3 = M ∗ X 3 and 1 1 1 M Z ,∗ X 3 = ((M Z X 3 ∩ pow(pow(D∗ ))) \ {M Z ,∗ X 2 : X 2 ∈ V2 }) 1 1 1 ∪{M Z ,∗ X 2 : X 2 ∈ V2 , M Z X 2 ∈ M Z X 3 } = ((M X 3 ∩ pow(pow(D∗ ))) \ {M ∗ X 2 : X 2 ∈ V2 }) ∪{M ∗ X 2 : X 2 ∈ V2 , M X 2 ∈ M X 3 } = M ∗X 3 . 1 1 Since M ∗,Z X 3 = M Z ,∗ X 3 the thesis follows. A.4 Proof of Lemma 4 Lemma 4. Let Z12 , . . . , Zp2 ∈ V2 \V2 and U12 , . . . , Up2 ∈ pow(pow(D∗ ))\{M ∗ X 2 : 2 2 X 2 ∈ V2 }. Then the 4LQS R -interpretations M∗,Z and MZ ,∗ coincide. 2 2 Proof. We show that M∗,Z and MZ ,∗ coincide by proving that they agree over variables of all sorts. 2 2 1. Plainly M ∗,Z x = M ∗ x = M Z ,∗ x, for every x ∈ V0 . 2 2 2. Let X 1 ∈ V1 , then M ∗,Z X 1 = M ∗ X 1 = M Z ,∗ X 1 . 3. Let X 2 ∈ V2 such that X 2 ∈ / {Z12 , . . . , Zp2 }, then 2 M ∗,Z X 2 = M ∗ [Z12 /U12 , . . . , Zp2 /Up2 ]X 2 = M ∗ X 2 , and 2 2 2 M Z ,∗ X 2 = ((M Z X 2 ∩ pow(D∗ )) \ {M Z ,∗ X 1 : X 1 ∈ (V1 ∪ V1F )}) 2 2 2 ∪{M Z ,∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M Z X 1 ∈ M Z X 2 } = ((M X 2 ∩ pow(D∗ )) \ {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F )}) ∪{M ∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M X 1 ∈ M X 2 } = M X2 . ∗ 2 2 Since M ∗,Z X 2 = M Z ,∗ X 2 the thesis follows. On the other hand, if X 2 ∈ 2 {Z12 , . . . , Zp2 }, say X 2 = Zj2 , then M ∗,Z X 2 = Uj2 , and 2 2 2 M Z ,∗ X 2 = ((M Z X 2 ∩ pow(D∗ )) \ {M Z ,∗ X 1 : X 1 ∈ (V1 ∪ V1F )}) 2 2 2 ∪{M Z ,∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M Z X 1 ∈ M Z X 2 } = (Uj2 \ {M ∗ X 1 : X 1 ∈ (V1 ∪ V1F )}) ∪({M ∗ X 1 : X 1 ∈ (V1 ∪ V1F ), M X 1 ∈ Uj2 }) = Uj2 . Clearly the thesis follows also in this case. 4. Let X 3 ∈ V3 . Then we have 2 M ∗,Z X 3 = M ∗ X 3 = ((M X 3 ∩ pow(pow(D∗ ))) \ {M ∗ X 2 : X 2 ∈ V2 }) ∪ {M ∗ X 2 : X 2 ∈ V2 , M X 2 ∈ M X 3 } 2 2 M Z ,∗ X 3 = ((M Z X 3 ∩ pow(pow(D∗ ))) 2 \ {M Z ,∗ X 2 : X 2 ∈ V2 ∪ {Z12 , . . . , Zp2 }}) 2 2 2 ∪{M Z ,∗ X 2 : X 2 ∈ V2 ∪ {Z12 , . . . , Zp2 }, M Z X 2 ∈ M Z X 3 } = ((M X 3 ∩ pow(pow(D∗ ))) \ ({M ∗ X 2 : X 2 ∈ V2 } ∪ {Uj2 : j = 1, . . . , p})) ∪{M ∗ X 2 : X 2 ∈ V2 , M X 2 ∈ M X 3 } ∪({Uj2 : j = 1, . . . , p} ∩ M X 3 ) . By putting P1 = M X 3 ∩ pow(pow(D∗ )) P2 = {M ∗ X 2 : X 2 ∈ V2 } P3 = {Uj2 : j = 1, . . . , p} P4 = {M ∗ X 2 : X 2 ∈ V2 , M X 2 ∈ M X 3 } P5 = {Uj2 : j = 1, . . . , p} ∩ M X 3 then the above relations can be rewritten as 2 M ∗,Z X 3 = (P1 \ P2 ) ∪ P4 2 M Z ,∗ X 3 = (P1 \ (P2 ∪ P3 )) ∪ P4 ∪ P5 . Moreover, it is easy to verify that the following relations hold: P2 ∩ P3 = ∅ P5 = P1 ∩ P3 P4 ⊆ P2 . Therefore we have (P1 \ P2 ) ∪ P4 = (P1 \ (P2 ∪ P3 )) ∪ P4 ∪ (P1 ∩ P3 ) = (P1 \ (P2 ∪ P3 )) ∪ P4 ∪ P5 2 2 i.e., we have M ∗,Z X 3 = M Z ,∗ X 3 . A.5 Proof of Lemma 7 Lemma 7. For every formula ϕ of the logic S5, ϕ is satisfiable in a model K = W, R, h iff there is a 4LQS R -interpretation satisfying x ∈ Xϕ . Proof. Let w̄ be a world in W . We construct a 4LQS R -interpretation M = (W, M ) as follows: – M x = w̄, – M Xp1 = h(p), where p is a propositional letter and Xp1 = τS5 (p), – M τS5 (ψ) = true, for every ψ ∈ SubF (ϕ), where ψ is not a propositional letter. To prove the lemma, it would be enough to show that K , w̄ |= ϕ iff M |= x ∈ Xϕ1 . However, it is more convenient to prove the following more general property: Given a w ∈ W , if y ∈ V0 is such that M y = w, then K , w |= ϕ iff M |= y ∈ Xϕ1 , which we do by structural induction on ϕ. Base case: If ϕ is a propositional letter, by definition, K , w |= ϕ iff w ∈ h(ϕ). But this holds iff M y ∈ M Xϕ1 , which is equivalent to M |= y ∈ Xϕ1 . Inductive step: We consider only the cases in which ϕ = ψ and ϕ = ♦ψ, as the other cases can be dealt with similarly. – If ϕ = ψ, assume first that K , w |= ψ. Then K , w |= ψ and, by induc- tive hypothesis, M |= y ∈ Xψ1 . Since M |= τS5 (ψ), it holds that M |= (∀z1 )(z1 ∈ Xψ1 ) → (∀z2 )(z2 ∈ Xψ 1 ). Then we have M [z1 /w, z2 /w] |= (z1 ∈ Xψ1 ) → (z2 ∈ Xψ 1 ) and, since M y = w, we have also that M |= (y ∈ Xψ1 ) → (y ∈ Xψ 1 ). By the inductive hypothesis and by 1 modus ponens we obtain M |= y ∈ Xψ , as required. On the other hand, if K , w |= ψ, then K , w |= ψ and, by inductive hypothesis, M |= y ∈ Xψ1 . Since M |= τS5 (ψ), then M |= ¬(∀z1 )(z1 ∈ Xψ1 ) → (∀z2 )¬(z2 ∈ Xψ 1 ). By the inductive hypothesis and some predi- cate logic manipulations, we have M |= ¬(y ∈ Xψ1 ) → ¬(y ∈ Xψ 1 ), and 1 by modus ponens we infer M |= ¬(y ∈ Xψ ), as we wished to prove. – Let ϕ = ♦ψ and, to begin with, assume that K , w |= ♦ψ. Then, there is a w such that K , w |= ψ, and a y  ∈ V0 such that M y  = w . Thus, by inductive hypothesis, we have M |= y  ∈ Xψ1 and, by predicate logic, M |= ¬(∀z1 )¬(z1 ∈ Xψ1 ). By the very definition of M , M |= τS5 (♦ψ) and thus M |= ¬(∀z1 )¬(z1 ∈ Xψ1 ) → (∀z2 )(z2 ∈ X♦ψ 1 ). Then, by modus 1 ponens we obtain M |= (∀z2 )(z2 ∈ X♦ψ ) and finally, by predicate logic, 1 M |= y ∈ X♦ψ . On the other hand, if K , w |= ♦ψ, then K , w |= ψ, for any w ∈ W and, since w = M y  for any y  ∈ V0 , it holds that M |= y  ∈ Xψ1 and thus, by predicate logic, M |= (∀z1 )¬(z1 ∈ Xψ1 ). Reasoning as above, M |= (∀z1 )¬(z1 ∈ Xψ1 ) → (∀z2 )¬(z2 ∈ X♦ψ 1 ) and, 1 by modus ponens, M |= (∀z2 )¬(z2 ∈ X♦ψ ). Finally, by predicate logic, 1 M |= y ∈ X♦ψ , as required. A.6 Proof of Lemma 8 Lemma 8. For every formula ϕ of the logic τK45 , ϕ is satisfiable in a model K = W, R, h iff there is a 4LQS R -interpretation satisfying x ∈ Xϕ . Proof. We proceed as in the proof of Lemma 7, by constructing a 4LQS R - interpretation M = (W, M ) which has the following property: Given a w ∈ W and a y ∈ V0 such that M y = w, it holds that K , w |= ϕ iff M |= y ∈ Xϕ1 . We proceed by structural induction on ϕ. As with Lemma 7, we consider only the cases in which ϕ = ψ and ϕ = ♦ψ. – Let ϕ = ψ and assume that K , w |= ψ. Let v be a world of W such that there is a u ∈ W with u, v ∈ R3 , and let x1 , x2 ∈ V0 be such that v = M x1 and u = M x2 . We have that K , v |= ψ and, by inductive hypothesis, M |= x1 ∈ Xψ1 . Since M |= τK45 (ψ), then M |= (∀z1 )((¬(∀z2 )¬(z2 , z1  ∈ R3 )) → z1 ∈ Xψ1 ) → (∀z)(z ∈ Xψ 1 ). Hence M [z1 /v, z2 /u, z/w] |= (z2 , z1  ∈ R → z1 ∈ Xψ ) → z ∈ Xψ and thus M |= (x2 , x1  ∈ R3 → x1 ∈ Xψ1 ) → 3 1 1 1 y ∈ Xψ . Since M |= x2 , x1  ∈ R3 → x1 ∈ Xψ1 , by modus ponens we have the thesis. The thesis follows also in the case in which there is no u such that u, v ∈ R3 . In fact, in that case M |= x2 , x1  ∈ R3 → x1 ∈ Xψ1 holds for any x2 ∈ V0 . Consider next the case in which K , w |= ψ. Then, there must be a v ∈ W such that there is a u with u, v ∈ R3 and K , v |= ψ. Let x1 , x2 ∈ V0 be such that M x1 = v and M x2 = u. Then, by inductive hypothesis, M |= x1 ∈ Xψ1 . By definition of M , we have M |= ¬(∀z1 )¬((¬(∀z2 )¬(z2 , z1  ∈ R3 ))∧¬(z1 ∈ Xψ1 )) → (∀z)¬(z ∈ Xψ 1 ). By the above instantiations and by the hypothe- ses, we have that M |= ((x2 , x1  ∈ R3 ) ∧ ¬(x1 ∈ Xψ1 )) → ¬(y ∈ Xψ 1 ) and 3 1 M |= (x2 , x1  ∈ R ) ∧ ¬(x1 ∈ Xψ ). Thus, by modus ponens, we obtain the thesis. – Let ϕ = ♦ψ and assume that K , w |= ♦ψ. Then there are u, v ∈ W such that u, v ∈ R and K , v |= ψ. Let x1 , x2 ∈ V0 be such that M x1 = v and M x2 = u. Then, by inductive hypothesis, M |= x1 ∈ Xψ1 . Since M |= τK45 (♦ψ), it follows that M |= ¬(∀z1 )¬((¬(∀z2 )¬(z2 , z1  ∈ R3 )) ∧ z1 ∈ Xψ1 ) → (∀z)(z ∈ X♦ψ 1 ). By the hypotheses and the variable instantiations above it follows that M |= ((x2 , x1  ∈ R3 ) ∧ x1 ∈ Xψ1 ) → y ∈ X♦ψ 1 and 3 1 M |= (x2 , x1  ∈ R ) ∧ x1 ∈ Xψ . Finally, by an application of modus ponens the thesis follows. On the other hand, if K , w |= ♦ψ, then for every v ∈ W , either there is no u ∈ W such that u, v ∈ R, or K , v |= ψ. Let x1 , x2 ∈ V0 be such that M x1 = v and M x2 = u. If K , v |= ψ, by inductive hypothesis, we have that M |= y ∈ Xψ1 . Since M |= (∀z1 )(((∀z2 )¬(z2 , z1  ∈ R3 )) ∨ ¬(z1 ∈ Xψ1 )) → (∀z)¬(z ∈ X♦ψ 1 ), by the hypotheses and by the variable instantiations above we get M |= (¬(x2 , x1  ∈ R3 ) ∨ ¬(x1 ∈ Xψ1 )) → ¬(y ∈ X♦ψ 1 ) and M |= (¬(x2 , x1  ∈ 3 1 R ) ∨ ¬(x1 ∈ Xψ )). Finally, by modus ponens we infer the thesis.