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.
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 [
In [
In this paper we present a decidability result for the satisfiability problem of the set-theoretic language 4LQS R (Four-Level Quantified Syllogistic with Restricted 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 [
Clearly, 4LQS R can express all the set-theoretical constructs which are already 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 language. 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
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 collections 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 X1, Y 1, Z1, . . .; (iii) V2 contains variables of sort 2, denoted by X2, Y 2, Z2, . . .; (iv) V3 contains variables of sort 3, denoted by X3, Y 3, Z3, . . .. 4LQS quantifier-free atomic formulae are classified as: level 0: x = y, x ∈ X1, for x, y ∈ V0, X1 ∈ V1; level 1: X1 = Y 1, X1 ∈ X2, for X1, Y 1 ∈ V1, X2 ∈ V2; level 2: X 2 = Y 2, x, y x, y ∈ V0, X 3 ∈ V3.
= X 2, x, y ∈ X 3, X 2 ∈ X 3, for X 2, Y 2 ∈ V2, 4LQS quantified atomic formulae are classified as: level 1: (∀z1) . . . (∀zn)ϕ0, with ϕ0 any propositional combination of quantifierfree atomic formulae, and z1, . . . , zn variables of sort 0; level 2: (∀Z11) . . . (∀Zm1)ϕ1, where Z11, . . . , Zm1 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 quantifierfree 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 quantifierfree 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, -- XX1121,, .. .. .. ,, XXpm21 ∈∈VV21,, - u1, . . . , un ∈ D, -- UU1121,, .. .. .. ,, UUpm21 ∈∈ppooww((pDo)w,(D)).
By M[x1/u1, . . . , xn/un, X11/U11, . . . , X m1/U m1, 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 coincides with M on all remaining variables. Throughout the paper we use the abbreviations: Mz for M[z1/u1, . . . , zn/un], MZ1 for M[Z11/U11, . . . , Zm1/U m1], and MZ2 for M[Z12/U12, . . . , Zp2/Up2].
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/U m1] |= ϕ1, for all U11, . . . , U m1 ∈ 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
4LQS R is the subcollection of the formulae ψ of 4LQS for which the following restrictions hold.
I. For every atomic formula (∀Z11), . . . , (∀Zm1)ϕ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 ¬ϕ0 → n m
Restriction (I) is similar to the one described in [
Through several examples, in [
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
We will solve the satisfiability problem for 4LQS R, i.e. the problem of establishing 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 Rconjunctions (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. Let ψ be a formula of 4LQS R and let ψDNF be a disjunctive normal form of ψ. Then ψ is satisfiable if and only if at least one of the disjuncts of ψDNF is satisfiable. We recall that the disjuncts of ψDNF 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)zz11,,......,,zznn , where z1, . . . , zn are newly introduced 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.
In view of the above reductions, we can limit ourselves to consider the satisfiability 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 X2 : X2 ∈ 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 [
Step 2: Let {F1, . . . , Fk} = F \{M X1 : X1 ∈ 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 X1 : X1 ∈ (V1 ∪V1F )} and |∆ 1| ≤ |T |−1 holds (cf. Step 1 above). – ∆ 2 satisfies |J ∩ ∆ 2| ≥ min(3, |J |), for every J ∈ {M X1 : X1 ∈ (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 (∀Zi1,h1 ) . . . (∀Zi1,hmi )ϕi we associate the collection ϕi,k1 , . . . , ϕi,k i of atomic formulae of the form (∀z1) . . . (∀zn)ϕ0 present in the matrix of ψi, and call the variables Zi1,h1, . . . , Zi1,hmi the arguments of ϕi,k1 , . . . , ϕi,k i . Let us put Φ = {ϕi,kj : 1 ≤ j ≤ i and 1 ≤ i ≤ r}. such that Then, for each ϕ ∈ Φ of the form (∀z1) . . . (∀zn)ϕ0 having Z11, . . . , Zm1 as arguments, and for each ordered m-tuple (Xh11, . . . , Xh1m ) of variables in V1 ∪ V1F , if M (ϕ0)ZX11h11,,......,,XZm1h1m = false we insert in D∗ elements u1, . . . , un ∈ D
M [z1/u1, . . . , zn/un](ϕ0)ZX11h11,,......,,XZmh11m = false , otherwise we leave D∗ unchanged.
Relativized interpretations. We introduce the notion of relativized interpretation, 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 =
M x , if M x ∈ D∗ d∗ , otherwise , M ∗X1 = M X1 ∩ D∗ , M ∗X2 = ((M X2 ∩ pow(D∗)) \ {M ∗X1 : X1 ∈ (V1 ∪ V1F )})
∪{M ∗X1 : X1 ∈ (V1 ∪ V1F ), M X1 ∈ M X2} , M ∗ x, y = {{M ∗x}, {M ∗x, M ∗y}} ,
M ∗X3 = ((M X3 ∩ pow(pow(D∗))) \ {M ∗X2 : X2 ∈ V2}) ,
∪{M ∗X2 : X2 ∈ V2, M X2 ∈ M X3} .
Concerning M ∗X2 and M ∗X3, 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 construction of D∗: (A) if M X1 = M Y 1, then (M X1 M Y 1) ∩ D∗ = ∅,2 (B) if M X2 = M Y 2, there is a J ∈ (M X2 M Y 2) ∩ {M X1 : X1 ∈ (V1 ∪ VF )} such that J ∩ D∗ = ∅, (C) if M x, y = M X2, there is a J ∈ (M X2 M x, y ) ∩ {M X1 : X1 ∈ (V1 ∪ VF )} such that J ∩ D∗ = ∅, and if J ∈ M X2, 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). 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) (b) (c) (d) (e) (f ) (g) (h)
M∗ |= x = y iff M |= x = y, for all x, y ∈ V0 such that M x, M y ∈ D∗; M∗ |= x ∈ X 1 iff M |= x ∈ X 1, for all X 1 ∈ V1 and x ∈ V0 such that M x ∈ D∗; M∗ |= X 1 = Y 1 iff M |= X 1 = Y 1, for all X 1, Y 1 ∈ V1 such that condition (A) holds; MM∗∗ ||== XX 21 ∈= XY 22 iiffff MM ||== XX21 =∈ XY22,, ffoorr aallll XX21, Y∈2(V∈1V∪2 VsFuc),h Xth2at∈coVn2d;ition (B) holds; 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; 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; 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.
In view of the next technical lemmas, we introduce the following notations. Let u1, . . . , un ∈ D∗, U11, . . . , U m1 ∈ pow(D∗), and U12, . . . , Up2 ∈ pow(pow(D∗)). Then we put and
M∗,z = M∗[z1/u1, . . . , zn/un], M∗,Z1 = M∗[Z11/U11, . . . , Zm1/U m1],
M∗,Z2 = M∗[Z12/U12, . . . , Zp2/Up2],
Mz,∗ = Rel(Mz, D∗, V1, V1F , V2), MZ1,∗ = Rel(MZ1 , D∗, V1 ∪ {Z11, . . . , Zm1}, V1F , V2),
MZ2,∗ = Rel(MZ2 , D∗, F ∗, V1, V1F , V2 ∪ {Z12, . . . , Zp2}).
The next three lemmas claim that, under certain conditions, the following pairs of 4LQS R-interpretations M∗,z and Mz,∗, M∗,Z1 and MZ1,∗, M∗,Z2 and MZ2,∗ can be identified.
Lemma 2. Let u1, . . . , un ∈ D∗, and let z1, . . . , zn ∈ V0. Then, for every x, y ∈ V0, X1 ∈ V1, X2 ∈ V2, X3 ∈ V3, we have: (i) M ∗,zx = M z,∗x, (ii) M ∗,zX1 = M z,∗X1, (iii) M ∗,zX2 = M z,∗X2, (iv) M ∗,zX3 = M z,∗X3.
Lemma 3. Let Z11, . . . , Zm1 ∈ V1 \ (V1 ∪ V1F ) and U11, . . . , U m1 ∈ pow(D∗) \ {M ∗X1 : X1 ∈ (V1∪V1F )}. Then, the 4LQS R-interpretations M∗,Z1 and MZ1,∗ coincide.
Lemma 4. Let Z12, . . . , Zp2 ∈ V2 \V2 and U12, . . . , Up2 ∈ pow(pow(D∗))\{M ∗X2 : X2 ∈ V2}. Then the 4LQS R-interpretations M∗,Z2 and MZ2,∗ coincide. The following lemma proves that satisfiability is preserved in the case of quantified atomic formulae.
Lemma 5. Let (∀z1) . . . (∀zn)ϕ0, (∀Z11) . . . (∀Zm1)ϕ1, (∀Z12) . . . (∀Zp2)ϕ2, and (∀Z2)(Z2 ∈ X3 ↔ ¬(∀z1, z2)¬( z1, z2 = Z2)) 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 |= (∀Z2)(Z2 ∈ X3 ↔ ¬(∀z1, z2)¬( z1, z2 = Z2)), then M∗ |= (∀Z2)(Z2 ∈ X3 ↔ ¬(∀z1, z2)¬( z1, z2 = Z2)).
Proof. (i) Assume by contradiction that there exist u1, . . . , un ∈ D∗ such that pMre∗te,zd|=diffϕe0r.eTnthleyni,nthMere∗,zmaunstd bine aMn za.toRmeiccalfloinrmguthlaatϕϕ00inisϕa0 pthroaptoissitiinotnear-l combination of quantifier-free atomic formulae of any level, we can suppose tXh2at=ϕ0Yis2.XT2he=n YM2 ∗a,znXd,2 w=ithout loss of generality, assume that M∗,z |=
M ∗,zY 2, so that, by Lemma 2, M z,∗X2 =
M z,∗Y 2. Then, Lemma 1 yields M zX2 = M zY 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 [
By Lemma 1, X2 ∈ X3 is interpreted in the same way in M∗ and in M. By case (i) of this lemma, if M∗ |= ¬(∀z1, z2)¬( z1, z2 = X2) then M |= ¬(∀z1, z2)¬( z1, z2 = X2). Thus, the only case to be considered is when M∗ |= (∀z1, z2)¬( z1, z2 = X2). Assume that M |= ¬(∀z1, z2)¬( z1, z2 = X2). Then M X2 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 = X2). 2. If U = M ∗X2, for every X2 ∈ V2, either Z2 ∈ X3 or ¬(∀z1, z2)¬( z1, z2 = Z2) has to be interpreted in a different way in M∗,Z2 and in MZ2 . By Lemmas 4 and 1, and by case (i) of this lemma, Z2 ∈ X3 has the same eZv2a)lutahteinon Min ZM2 ∗|=,Z2¬a(n∀dz1i,nzM2)¬Z(2z,1a,nzd2 if=MZ∗,2Z)2. |T=h¬e(o∀nzl1y, zc2a)s¬e( tzh1a,tz2sti=ll has to be analyzed is when M∗,Z2 |= (∀z1, z2)¬( z1, z2 = Z2). By Lemma 4, MZ2,∗ |= (∀z1, z2)¬( z1, z2 = Z2). Let us assume that MZ2 |= (∀z1, z2)¬( z1, z2 = Z2). Then U must be a pair {{u}, {u, v}}, u, v ∈ D. Since U ∈ pow(pow(D∗)), then u, v ∈ D∗, contradicting that MZ2,∗ |= (∀z1, z2)¬( z1, z2 = Z2).
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 therefore its satisfiability problem is solvable). 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 satisfiability 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 ϕDNF be a disjunctive normal form of ϕ. Then there is a disjunct ψ of ϕDNF 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)kLn)|Φ|. 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
As discussed in [
(∀z)(z ∈ X 1 ↔ ϕ(z)) (∀X i−1)(X i−1 ∈ X i ↔ ϕ(X i−1)) (2) (3) provided that they satisfy the syntactic constraints of 4LQS R.
Since 4LQS R is a superlanguage of 3LQS R, as shown in [
3LSSP can plainly be decided by the decision procedure presented in [
Other constructs of set theory which are expressible in the 4LQS R formalism,
as shown in [
Xi1 and Z ∩ Xi1 = ∅, for all 1 ≤ i ≤ n} 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 characterize 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.
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 [
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 [
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 ψ.
For every propositional letter p, let τS15(p) = Xp1, where Xp1 ∈ V1, and let τS25 : S5 → 4LQS R be the function defined recursively as follows: – τS25(p) = Λ, – τS25(¬ϕ) = (∀z)(z ∈ X¬1ϕ ↔ ¬(z ∈ Xϕ1)) ∧ τS25(ϕ), – τS25(ϕ1 ∧ ϕ2) = (∀z)(z ∈ Xϕ11∧ϕ2 ↔ (z ∈ Xϕ11 ∧ z ∈ Xϕ12)) ∧ τS25(ϕ1) ∧ τS25(ϕ2), – τS25(ϕ1 ∨ ϕ2) = (∀z)(z ∈ Xϕ11∨ϕ2 ↔ (z ∈ Xϕ11 ∨ z ∈ Xϕ12)) ∧ τS25(ϕ1) ∧ τS25(ϕ2), (∀z)(z ∈ Xϕ1 ) → (∀z)(z ∈ X1 ϕ) ∧ ¬(∀z)(z ∈ Xϕ1) → (∀z)¬(z ∈ – τS25( ϕ) = – τS25(♦ϕ) =
X1 ϕ) ∧ τS25(ϕ),
¬(∀z)¬(z ∈ Xϕ1 ) → (∀z)(z ∈ X♦1ϕ) ∧ (∀z)¬(z ∈ Xϕ1) → (∀z)¬(z ∈ X♦1ϕ) ∧ τS25(ϕ), where Λ is the empty formula and X¬1ϕ, Xϕ1, Xϕ11∧ϕ2, Xϕ11∨ϕ2, Xϕ11, Xϕ12 ∈ V1.
Finally, for every ϕ in S5, if ϕ is a propositional letter in P we put τS5(ϕ) = τS15(ϕ), otherwise τS5(ϕ) = τS25(ϕ).
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
(∀Z1)(Z1 ∈ R2 ↔ (Z1 ∈ pow=1(U ) ∨ Z1 ∈ pow=2(U ))) , 2. as a variable of sort 3, R3, such that (∀Z2)(Z2 ∈ R3 ↔ ¬(∀z1, z2)¬( z1, z2 = Z2)) ∧ (∀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ϕ.
It can be checked that τS5(ϕ) is polynomial in the size of ϕ and that its
satisfiability can be verified in nondeterministic polynomial time since it belongs
to (4LQS R)1. Consequently, the decision algorithm presented in this paper
together with the translation function introduced above can be considered an
optimal 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 [
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: (∀Z2)(Z2 ∈ R3 ↔ ¬(∀z1)(∀z2)¬( z1, z2 = Z2)) ∧(∀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. For every ϕ ∈ K45 we put τK45(ϕ) = τK145(ϕ), if ϕ is a propositional letter and τK45(ϕ) = τK245(ϕ) otherwise. τ 1
K45(p) = Xp1, with Xp1 ∈ V1, for every propositional letter p, and τ 2
K45(ϕ) is defined inductively over the structure of ϕ. We report the definition of τK245(ϕ) only when ϕ = ψ and ϕ = ♦ψ, as the other cases are identical to τS25(ϕ), defined in the previous section: – τK245( ψ) = (∀z1)((¬(∀z2)¬( z2, z1 ∈ R3)) → z1 ∈ Xψ1 ) → (∀z)(z ∈ X 1 ψ) ∧¬(∀z1)¬((¬(∀z2)¬( z2, z1 ∈ R3)) ∧ ¬(z1 ∈ Xψ1 )) → (∀z)¬(z ∈
X 1 ψ) ∧ τK245(ψ);
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ϕ. 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
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 accessibility 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 operations on relations, we plan to investigate the possibility of translating fragments of Boolean modal logics into 4LQS R.
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 ∈ X1 iff M |= x ∈ X1, for all X1 ∈ V1 and x ∈ V0 such that
M x ∈ D∗; (c) M∗ |= X1 = Y 1 iff M |= X1 = Y 1, for all X1, Y 1 ∈ V1 such that condition (A) holds; (d) M∗ |= X1 ∈ X2 iff M |= X1 ∈ X2, for all X1 ∈ (V1 ∪ VF ), X2 ∈ V2; (e) M∗ |= X2 = Y 2 iff M |= X2 = Y 2, for all X2, Y 2 ∈ V2 such that condition (B) holds; (f ) M∗ |= x, y = X2 iff M |= x, y = X2, for all x, y ∈ V0 such that
M x, M y ∈ D∗ and X2 ∈ V2 such that condition (C) holds; (g) M∗ |= x, y ∈ X3 iff M |= x, y ∈ X3, for all x, y ∈ V0 such that
M x, M y ∈ D∗ and X2 ∈ V2 such that condition (C) holds; (h) M∗ |= X2 ∈ X3 iff M |= X2 ∈ X3, for all x, y ∈ V0 such that M x, M y ∈
D∗ and X2 ∈ 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 X1 ∈ V1 and let x ∈ V0 be such that M x ∈ D∗. Then M ∗x = M x, so that M ∗x ∈ M ∗X1 iff M x ∈ M X1 ∩ D∗ iff M x ∈ M X1. (c) If M X1 = M Y 1, then plainly M ∗X1 = M ∗Y 1. On the other hand, if M X1 = M Y 1, then, by condition (A), (M X1 M Y 1) ∩ D∗ = ∅ and thus M ∗X1 = M ∗Y 1. (d) If M X1 ∈ M X2, then M ∗X1 ∈ M ∗X2. On the other hand, suppose by contradiction that M X1 ∈/ M X2 and M ∗X1 ∈ M ∗X2. Then, there must necessarily be a Z1 ∈ (V1 ∪ V1F ) with M Z1 ∈ M X2, M Z1 = M X1, and M ∗X1 = M ∗Z1. Since M Z1 = M X1 and (M Z1 M X1) ∩ D∗ = ∅, by condition (A), we have M ∗X1 = M ∗Z1, which is a contradiction. (e) If M X2 = M Y 2, then M ∗X2 = M ∗Y 2. On the other hand, if M X2 = M Y 2, by condition (B), there is a J ∈ (M X2 M Y 2) ∩ {M X1 : X1 ∈ (V1 ∪ V1F )} such that J ∩ D∗ = ∅. Let J = M X1, for some X1 ∈ (V1 ∪ V1F ), and suppose (d), M ∗X1 ∈ M ∗X2 and M ∗X1 ∈/ M ∗∈Y M2aXn2d ahnedncMeMX1∗X∈/2M=YM2.∗YTh2.en, by without loss of generality that M X1 (f) If M x, y = M X2, then M ∗ x, y = M ∗X2. If M x, y = M X2, then there is a J ∈ (M X2 M x, y ) ∩ {M X1 : X1 ∈ (V1 ∪ V1F )} satisfying the constraints of condition (C). Let J = M X1, for some X1 ∈ (V1 ∪ V1F ), and suppose that M X1 ∈ M X2 and M X1 ∈/ M x, y . Then M ∗X1 ∈ M ∗X2 and since M ∗X1 = {M x} and M ∗X1 = {M x, M y}, it follows that M ∗X1 / ∈ M ∗ x, y . On the other hand, if M X1 ∈ M x, y and M X1 ∈/ M X2, then either M X1 = {M x} or M X1 = {M x, M y}. In both cases M X1 = M ∗X1 and thus if M X1 ∈/ M X2, it plainly follows that M ∗X1 ∈/ M ∗X2. (g) Let x, y ∈ V0 and X3 ∈ V3 be such that M x, y ∈ MX3. Then M∗ x, y ∈ M∗X3. On the other hand, suppose by contradiction that M x, y ∈/ MX3 and M∗ x, y ∈ M∗X3. Then, there must be an X2 ∈ V2 such that M∗X2 ∈ M∗X3, M∗X2 = M∗ x, y , and MX2 = M x, y . But this is impossible by (f). (h) If MX2 ∈ MX3 then M∗X2 ∈ M∗X3. Now suppose by contradiction that MX2 ∈/ MX3 and that M∗X2 ∈ V2 such that MX2 = MY 2 and M∗∈XM2=∗XM3.∗YTh2,enw,heicithheisr nthoterpeoisssiablYe 2by (e), or there is a x, y , with x, y ∈ V0, Mx, My ∈ D∗, such that MX2 = M x, y and M∗X2 = 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, X1 ∈ V1, X2 ∈ V2, X3 ∈ V3, we have: (i) M∗,zx = Mz,∗x, (ii) M∗,zX1 = Mz,∗X1, (iii) M∗,zX2 = Mz,∗X2, (iv) M∗,zX3 = Mz,∗X3.
Proof. (i) Since u1, . . ., un ∈ D∗, the thesis follows immediately. (ii) Let X1 ∈ V1, then M∗,zX1 = M∗X1 = MX1∩D∗ = MzX1∩D∗ = Mz,∗X1. (iii) Let X2 ∈ V2, then we have the following equalities:
M∗,zX2 = M∗X2 = ((MX2 ∩ pow(D∗)) \ {M∗X1 : X1 ∈ (V1 ∪ V1F)}) ∪ {M∗X1 : X1 ∈ (V1 ∪ V1F), MX1 ∈ MX2} , = ((MzX2 ∩ pow(D∗)) \ {Mz,∗X1 : X1 ∈ (V1 ∪ V1F)})
∪ {Mz,∗X1 : X1 ∈ (V1 ∪ V1F), MzX1 ∈ MzX2} = Mz,∗X2 . (iv) Let X3 ∈ V3, then the following holds:
M∗,zX3 = M∗X3 = ((MX3 ∩ pow(pow(D∗))) \ {M∗X2 : X2 ∈ V2}) ∪ {M∗X2 : X2 ∈ V2, MX2 ∈ MX3} , = ((MzX3 ∩ pow(pow(D∗))) \ {Mz,∗X2 : X2 ∈ V2})
∪ {Mz,∗X2 : X2 ∈ V2, MzX2 ∈ MzX3} = Mz,∗X3 . Lemma 3. Let Z11, . . . , Zm1 ∈ V1 \ (V1 ∪ V1F) and U11, . . ., Um1 ∈ pow(D∗) \ {M∗X1 : X1 ∈ (V1∪V1F)}. Then, the 4LQSR-interpretations M∗,Z1 and MZ1,∗ coincide.
Proof. We prove the lemma by showing that M∗,Z1 and MZ1,∗ agree over variables of all sorts. 1. Clearly M∗,Z1x = M∗x = MZ1,∗x, for all individual variables x ∈ V0. 2. Let X1 ∈ V1. If X1 ∈/ {Z11, . . . , Zm1}, then
MZ1,∗X1 = MZ1X1 ∩ D∗ = MX1 ∩ D∗ = M∗X1 = M∗,Z1X1 .
On the other hand, if X1 = Zj1 for some j ∈ {1, . . ., m}, we have
MZ1,∗Zj1 = MZ1Zj1 ∩ D∗ = Uj1 ∩ D∗ = Uj1 = M∗,Z1Zj1 . 3. Let X2 ∈ V2. Then we have
M∗,Z1X2 = M∗X2 = ((MX2 ∩ pow(D∗)) \ {M∗X1 : X1 ∈ (V1 ∪ V1F)}) ∪ {M∗X1 : X1 ∈ (V1 ∪ V1F), MX1 ∈ MX2} , MZ1,∗X2 = ((MZ1X2 ∩ pow(D∗))
\{MZ1,∗X1 : X1 ∈ ((V1 ∪ V1F) ∪ {Z11, . . . , Zm1})}) ∪{MZ1,∗X1 : X1 ∈ ((V1 ∪ V1F) ∪ {Z11, . . ., Zm1}),
MZ1X1 ∈ MZ1X2} = ((MX2 ∩ pow(D∗))
\({M∗X1 : X1 ∈ (V1 ∪ V1F)} ∪ {Uj : j = 1, . . ., m})) ∪({M∗X1 : X1 ∈ (V1 ∪ V1F), MX1 ∈ MX2} ∪({Uj : j = 1, . . ., m} ∩ MX2)).
By putting the above relations can be rewritten as
P1 = MX2 ∩ pow(D∗), P2 = {M∗X1 : X1 ∈ (V1 ∪ V1F)}, P3 = {Uj : j = 1, . . . , m}, P4 = {M∗X1 : X1 ∈ (V1 ∪ V1F), MX1 ∈ MX2}, P5 = {Uj : j = 1, . . . , m} ∩ MX2,
M∗,Z1X2 = (P1 \ P2) ∪ P4
MZ1,∗X2 = (P1 \ (P2 ∪ P3)) ∪ P4 ∪ P5 .
Therefore we have (P1 \ P2) ∪ P4 = (P1 \ (P2 ∪ P3)) ∪ P4 ∪ (P1 ∩ P3) MZ1,∗X3 = ((MZ1X3 ∩ pow(pow(D∗))) \ {MZ1,∗X2 : X2 ∈ V2}) ∪{MZ1,∗X2 : X2 ∈ V2, MZ1X2 ∈ MZ1X3} = ((MX3 ∩ pow(pow(D∗))) \ {M∗X2 : X2 ∈ V2})
∪{M∗X2 : X2 ∈ V2, MX2 ∈ MX3} = M∗X3 .
Since M∗,Z1X3 = MZ1,∗X3 the thesis follows.
A.4 Proof of Lemma 4 Lemma 4. Let Z12, . . ., Zp2 ∈ V2\V2 and U12, . . . , Up2 ∈ pow(pow(D∗))\{M∗X2 : X2 ∈ V2}. Then the 4LQSR-interpretations M∗,Z2 and MZ2,∗ coincide. Proof. We show that M∗,Z2 and MZ2,∗ coincide by proving that they agree over variables of all sorts. 1. Plainly ∈MV∗,1Z,2txhe=nMM∗∗x,Z=2XM1 Z=2,M∗x∗, Xfo1r =eveMryZx2,∗∈XV10.. 2. Let X1 3. Let X2 ∈ V2 such that X2 ∈/ {Z12, . . . , Zp2}, then
M∗,Z2X2 = M∗[Z12/U12, . . . , Zp2/Up2]X2 = M∗X2, and
MZ2,∗X2 = ((MZ2X2 ∩ pow(D∗)) \ {MZ2,∗X1 : X1 ∈ (V1 ∪ V1F)}) ∪{MZ2,∗X1 : X1 ∈ (V1 ∪ V1F), MZ2X1 ∈ MZ2X2} = ((MX2 ∩ pow(D∗)) \ {M∗X1 : X1 ∈ (V1 ∪ V1F)})
∪{M∗X1 : X1 ∈ (V1 ∪ V1F), MX1 ∈ MX2} = M∗X2 .
Since M∗,Z2X2 = MZ2,∗X2 the thesis follows. On the other hand, if X2 ∈ {Z12, . . . , Zp2}, say X2 = Zj2, then M∗,Z2X2 = Uj2, and
MZ2,∗X2 = ((MZ2X2 ∩ pow(D∗)) \ {MZ2,∗X1 : X1 ∈ (V1 ∪ V1F)})
M∗,Z2X3 = M∗X3 = ((MX3 ∩ pow(pow(D∗))) \ {M∗X2 : X2 ∈ V2}) ∪ {M∗X2 : X2 ∈ V2, MX2 ∈ MX3} MZ2,∗X3 = ((MZ2X3 ∩ pow(pow(D∗)))
\ {MZ2,∗X2 : X2 ∈ V2 ∪ {Z12, . . . , Zp2}}) ∪{MZ2,∗X2 : X2 ∈ V2 ∪ {Z12, . . . , Zp2}, MZ2X2 ∈ MZ2X3} = ((MX3 ∩ pow(pow(D∗)))
\ ({M∗X2 : X2 ∈ V2} ∪ {Uj2 : j = 1, . . . , p})) ∪{M∗X2 : X2 ∈ V2, MX2 ∈ MX3} ∪({Uj2 : j = 1, . . . , p} ∩ MX3) .
By putting
M∗,Z2X3 = (P1 \ P2) ∪ P4
MZ2,∗X3 = (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 i.e., we have M∗,Z2X3 = MZ2,∗X3.
(P1 \ P2) ∪ P4 = (P1 \ (P2 ∪ P3)) ∪ P4 ∪ (P1 ∩ P3)
= (P1 \ (P2 ∪ P3)) ∪ P4 ∪ P5
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 inductive hypothesis, M |= y ∈ Xψ1 . Since M |= τS5( ψ), it holds that M |= (∀z1)(z1 ∈ Xψ1 ) → (∀z2)(z2 ∈ X1 ψ). Then we have M [z1/w, z2/w] |= (z1 ∈ Xψ1 ) → (z2 ∈ X1 ψ) and, since M y = w, we have also that M |= (y ∈ Xψ1 ) → (y ∈ X1 ψ). By the inductive hypothesis and by modus ponens we obtain M |= y ∈ X1 ψ, 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 ∈ X1 ψ). By the inductive hypothesis and some predicate logic manipulations, we have M |= ¬(y ∈ Xψ1 ) → ¬(y ∈ X1 ψ), and by modus ponens we infer M |= ¬(y ∈ X1 ψ), 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 ponens we obtain M |= (∀z2)(z2 ∈ X♦1ψ) and finally, by predicate logic, M |= y ∈ X♦1ψ.
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, by modus ponens, M |= (∀z2)¬(z2 ∈ X♦1ψ). Finally, by predicate logic, M |= y ∈ X♦1ψ, 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 Rinterpretation 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 ∈ X1 ψ). Hence M [z1/v, z2/u, z/w] |= ( z2, z1 ∈ R3 → z1 ∈ Xψ1 ) → z ∈ X1 ψ and thus M |= ( x2, x1 ∈ R3 → x1 ∈ Xψ1 ) → y ∈ X1 ψ. 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 ∈ X1 ψ). By the above instantiations and by the hypotheses, we have that M |= (( x2, x1 ∈ R3) ∧ ¬(x1 ∈ Xψ1 )) → ¬(y ∈ X1 ψ) and M |= ( x2, x1 ∈ R3) ∧ ¬(x1 ∈ Xψ1 ). 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 M |= ( x2, x1 ∈ R3) ∧ x1 ∈ Xψ1 . 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 ∈ R3) ∨ ¬(x1 ∈ Xψ1 )). Finally, by modus ponens we infer the thesis.