Capturing k-ary existential second order logic with k-ary inclusion–exclusion logic

Capturing k-ary Existential Second Order Logic with k-ary Inclusion-Exclusion Logic Raine Rönnholm University of Tampere, 33014 Tampere, Finland Abstract In this paper we analyze k-ary inclusion-exclusion logic, INEX[k], which is obtained by extending first order logic with k-ary inclusion and exclusion atoms. We show that every formula of INEX[k] can be expressed with a formula of kary existential second order logic, ESO[k]. Conversely, every formula of ESO[k] with at most k-ary free relation variables can be expressed with a formula of INEX[k]. From this it follows that, on the level of sentences, INEX[k] captures the expressive power of ESO[k]. We also introduce several useful operators that can be expressed in INEX[k]. In particular, we define inclusion and exclusion quantifiers and so-called term value preserving disjunction which is essential for the proofs of the main results in this paper. Furthermore, we present a novel method of relativization for team semantics and analyze the duality of inclusion and exclusion atoms. Keywords: Inclusion logic, exclusion logic, dependence logic, team semantics, existential second order logic, expressive power 2010 MSC: 03B60, 03C80, 03C85 1. Introduction The origin of inclusion and exclusion logics lies in the notion of dependence and imperfect information in logic. First approaches in this area were partially ordered quantifiers by Henkin [10] and IF-logic (independence friendly logic) by Hintikka and Sandu [11]. The truth for IF-logic was originally defined by using semantic games of imperfect information ([12]), but an equivalent compositional semantics was presented later by Hodges [13]. However, in the compositional approach it is not sufficient to consider single assignments, but instead sets of assignments which are called teams. Email address: [email protected] (Raine Rönnholm) Preprint submitted to Annals of Pure and Applied Logic April 11, 2018 This is the post print version of the article, which has been published in Annals of Pure and Applied Logic 2018, 169(3), 177-215. The final publication is available at https://doi.org/10.1016/j.apal.2017.10.005 Teams can be seen as parallel positions in a semantic game, or can be interpreted as information sets or as databases ([18]). By using similar team semantics as Hodges, Väänänen [18] introduced dependence logic which extends first order logic with new atomic formulas called dependence atoms. Later Grädel and Väänänen [7] presented independence logic by analogously adding independence atoms to first order logic. The truth conditions for these atoms are defined by dependencies/independencies of the values of terms in a team. These logics have been recently studied actively with an attempt to formalize the dependency phenomena in different fields of science. There has been research in several areas such as database dependency theory ([15]), belief presentation ([3]) and quantum mechanics ([14]). Inclusion and exclusion logics were first presented by Galliani [4]. They extend first order logic with inclusion and exclusion atoms as dependence atoms in dependence logic. Suppose that ~ t1,~ t2are k-tuples of terms and Xis a team. The k-ary inclusion atom ~ t1⊆~ t2says that the values of ~ t1are included in the values of~ t2in the team X. The k-ary exclusion atom~ t1|~ t2analogously says that ~ t1and ~ t2get distinct values in X. These are simple and natural dependencies in database theory ([4]), and thus it is reasonable to consider such atoms in a team semantical setting. Inclusion and exclusion atoms have some natural complementary properties. Exclusion logic is known to be closed downwards ([4]), i.e. if a team satisfies some formula, then also all of its subteams satisfy it. Inclusion logic, on the other hand, is known to be closed under unions ([4]), i.e. if each team in a set of teams satisfies a formula, then also their union satisfies it. However, neither of these logics is both closed downwards and under unions. Therefore the combination of these logics, inclusion-exclusion logic, has neither of these properties. Exclusion logic is equivalent with dependence logic ([4]) which captures existential second order logic, ESO, on the level of sentences ([18]). Inclusion logic is not comparable with dependence logic in general ([4]), but captures positive greatest fixed point logic on the level of sentences, as shown by Galliani and Hella [6]. Hence exclusion logic captures NP, and inclusion logic captures PTIME over finite structures with linear order. Inclusion-exclusion logic has been shown to be equivalent with independence logic by Galliani [4]. Galliani has also shown in [4] that with inclusion-exclusion logic it is possible to define exactly those properties of teams which are definable in ESO. Thus we can say that inclusion-exclusion logic captures ESO on the level of formulas. By these earlier results, we see that the expressive power of inclusionexclusion logic is rather strong. Instead of studying this whole logic, we will consider its weaker fragments. One of the most canonical approaches is to restrict the arities of inclusion and exclusion atoms. In particular, unary atoms 2 are much simpler than inclusion and exclusion atoms in general. Hannula [8] has shown that inclusion logic has a strict arity hierarchy over graphs, but it is still open what is the exact fragment of ESO that corresponds to k-ary inclusion logic, INC[k]. Before our work similar research has not been done for exclusionnor for inclusion-exclusion logic. Our main research question for this paper was to examine whether there is some natural fragment of ESO that corresponds to unary inclusion-exclusion logic, INEX[1]. Similar research has been done on the related logics: Durand and Kontinen [2] have shown that, on the level of sentences, k-ary dependence logic captures the fragment of ESO in which at most (k−1)-ary functions can be quantified. Galliani, Hannula and Kontinen [5] have shown that the same result holds also for k-ary independence logic. The arity hierarchy of ESO (over arbitrary vocabulary) is known to be strict, as shown by Ajtai [1] in 1983. Consequently dependence and independence logics have a strict arity hierarchy over sentences. These earlier results, however, do not tell much about the expressive power of k-ary exclusion logic, EXC[k], and k-ary inclusion-exclusion logic, INEX[k], since the known translations from them to dependence and independence logics do not respect the arities of atoms. Also, since these results are proven on the level of sentences, we do not know much how does the arity affect the expressive power of these logics on the level of formulas. We will show in Subsection 4.1 that every formula of EXC[k] can be expressed with a formula of k-ary ESO, ESO[k]. The idea of this compositional translation is that for each occurrence of an exclusion atom ~ t1|~ t2we quantify a separate k-ary relation variable that gives limits to the values that the tuple ~ t1can get and~ t2cannot. We can formulate a similar, yet more complex, translation for INC[k] and then merge these two translations to create a translation from INEX[k] to ESO[k]. In Subsection 4.2 we will show that all ESO[k]-formulas that contain at most k-ary free relation variables can be expressed with a formula of INEX[k]. The translation we use here is compositional, very natural and uses inclusion and exclusion atoms in a dualistic way: The quantified k-ary relation variables Piare just replaced with k-tuples ~wiof quantified first order variables. Then we simply replace atomic formulas of the form Pi ~ twith inclusion atoms ~ t⊆~wi and formulas of the form ¬Pi ~ twith exclusion atoms ~ t|~wi. In order to get make this last translation compositional, we also need a new operator called term value preserving disjunction which is introduced in Subsection 3.4. We will show that this operator can be expressed with inclusion and exclusion atoms, and furthermore when preserving values of k-tuples, it can be defined in INEX[k]. We will also explain in Subsection 3.4 why this is a useful operator for the framework of team semantics in general. From our results it follows that, on the level of sentences, INEX[k] captures 3 the expressive power of ESO[k]. In particular, by using only unary inclusion and exclusion atoms we get the expressive power of existential monadic second order logic, EMSO. This special case should be noted for the following reason: As a consequence of the results mentioned above ([2, 5]), if we extend FO with 1-ary dependence (or independence) atoms, the expressive power stays inside FO. But if we extend FO with 2-ary dependence (or independence) atoms, the expressive power becomes already stronger than EMSO. Thus INEX[1] deserves extra recognition by capturing this important fragment of ESO that has not yet been characterized in the framework of team semantics. In addition to our main results, we also analyze the nature of inclusion and exclusion logics and their relationship more deeply. Even though inclusion and exclusion atoms are not contradictory negations of each other, we claim that they can be seen as duals of each other and thus they make a natural pair. This is one more reason why inclusion-exclusion logic can be seen as a quite canonical logic for the framework of team semantics. We also analyze inclusion and exclusion relations from an another perspective by introducing inclusion and exclusion quantifiers. This can be seen as a step back to the origin of these logics, since dependence logic was inspired by IF-logic, in which dependencies were handled with quantification. In Subsection 3.2 we first define natural semantics for inclusion and exclusion quantifiers and then show that we can express them in inclusion-exclusion logic. We also show reversely that, by extending first order logic with these quantifiers, we obtain an equivalent logic with inclusion-exclusion logic. However, there are still some small, yet intriguing, differences between these two approaches. By using several of our new operators – term value preserving disjunction and both existential and universal inclusion quantifiers – we can introduce a novel method of relativization for team semantics. This technique is introduced in Subsection 3.5 and later, in Section 5, we present further examples on how it can be applied. In Section 5 we also present some other concrete examples where we show how to use our translations and new operators to express some classical properties of models and teams in a rather straightforward way. The structure of this paper is as follows: In Section 2 we review team semantics for FO and define inclusion and exclusion logics. In Section 3 we define several useful operators for inclusion-exclusion logic – such as inclusion and exclusion quantifiers and term value preserving disjunction. In Section 4 we present our translations between INEX[k]and ESO[k], and in Section 5 we present some further examples. After the conclusion in Section 6, there is an appendix where we present a single long and technical proof that has been omitted from the main text. For some further technical details, see an extended version of this paper [17]. 4 2. Preliminaries In this section we first define team semantics for first order logic. Then we present inclusion and exclusion logics, define team semantics for them and review some of their know properties. For some further details, see [17]. 2.1. Syntax and team semantics for first order logic Let Lbe a vocabulary. We denote the set of L-terms by TL. If ~ t=t1. . . tk and ti∈TLfor each i≤k, we write ~ t∈TL. The set of variables occurring in a term tis denoted by Vr(t). For a tuple ~ t=t1. . . tkof L-terms we write Vr(~ t) := Vr(t1)∪ · · · ∪ Vr(tk). The set of first order logic formulas with respect to vocabulary L, denoted by FOL, is defined in the standard way – except that we require all formulas to be in negation normal form.FOL-formulas of the form t1=t2,¬t1=t2,R~ tand ¬R~ tare called literals. We denote the set of subformulas of an FOL-formula ϕby Sf(ϕ), the set of variables occurring in ϕ by Vr(ϕ)and the set of free variables of ϕby Fr(ϕ). Let M= (M, I)be an L-model. An assignment sfor Mis a function that is defined in some set of variables, dom(s), and ranges over M. A team X for Mis any set of assignments for Mwith a common domain, denoted by dom(X). In the literature usually only teams with finite domains have been considered, but for this paper there is no need to assume the domains of teams to be finite. Note that we also allow the empty assignment s=∅and the empty team X=∅. For the empty team we allow any of set variables to be interpreted as its domain (this is practical for certain technical reasons). The empty team is not to be confused with the team X={∅} which has a special role with FOL-sentences. Let sbe an assignment, ~a := (a1, . . . , ak)∈Mkand ~x := x1. . . xka tuple of variables. The assignment s[~a/~x ]is defined in dom(s)∪Vr(~x ), and it maps a variable xito ai(i≤k), and all other variables as the assignment s. For a team X, a set A⊆Mkand a function F:X→ P(Mk)we write X[A/~x ] := {s[~a/~x ]|s∈X, ~a ∈A} X[F/~x ] := {s[~a/~x ]|s∈X, ~a ∈ F(s)}. Let Mbe an L-model, san assignment and t∈TLs.t. Vr(t)⊆dom(s). The interpretation of twith respect to Mand s,tMhsi, is denoted simply by s(t). Let ~ t:= t1. . . tk∈TLand let Xbe a team s.t. Vr(~ t)⊆dom(X). We write s(~ t) := (s(t1), . . . , s(tk)) and X(~ t) := {s(~ t)|s∈X}. Note that s(~ t)is a vector in Mand X(~ t)is a k-ary relation in M. We write P∗(A) := P(A)\ {∅}. We are now ready to define team semantics for FO. 5 Definition 2.1. Let Mbe an L-model, ϕ∈FOLand Xa team such that Fr(ϕ)⊆dom(X). We define the truth of ϕin Mand X, denoted by MXϕ: • M Xt1=t2iff s(t1) = s(t2)for all s∈X. • M X¬t1=t2iff s(t1)6=s(t2)for all s∈X. • M XR~ tiff s(~ t)∈RMfor all s∈X. • M X¬R~ tiff s(~ t)/∈RMfor all s∈X. • M Xψ∧θiff MXψand MXθ. • M Xψ∨θiff there are Y, Y 0⊆Xs.t. Y∪Y0=X,MYψand MY0θ. • M X∃x ψ iff there is F:X→ P∗(M)such that MX[F/x]ψ. • M X∀x ψ iff MX[M/x]ψ. Remark. In the truth definition above we introduced so-called lax semantics for existential quantifier. In this definition the quantified variable can be given several witnesses. From the perspective of game-theoretic semantics this can be interpreted as the verifying player having a non-deterministic strategy when choosing a value for the quantified variable ([3]). An alternative semantics, so-called strict semantics, is to allow only a single witness for each assignment. In first the order case these two truth definitions are equivalent1([4]), but this does not hold when we extend FO with inclusion atoms. For ϕ∈FOLand ~x := x1. . . xk, we write ∃~x ϕ := ∃x1. . . ∃xkϕand ∀~x ϕ := ∀x1. . . ∀xkϕ. By Definition 2.1, consecutive quantifications modify the team after the evaluation of each quantifier. Nevertheless, as shown by the following easy proposition, it is equivalent to quantify several elements in Mone after another and to quantify a single vector in M. Proposition 2.1. For any k-tuple ~x and ϕ∈FOLwe have a) MX∃~x ϕ iff there exists F:X→ P∗(Mk)such that MX[F/~x ]ϕ. b) MX∀~x ϕ iff MX[Mk/~x ]ϕ. Note that with lax semantics for existential quantifier, when we quantify a k-tuple of variables, we can actually quantify a k-ary relation in M. First order logic with team semantics has so-called flatness-property: Proposition 2.2 ([18], Flatness).Let Xbe a team and ϕ∈FOL. Then MXϕiff M{s}ϕfor all s∈X. 1Also note that, in the general case, the lax version is not stronger since we can always turn a strict quantifier into the corresponding lax quantifier by adding a “dummy” universal quantifier before it in the formula. That is, if zis a fresh variable, then the formula ∃x ϕ has same truth condition with lax semantics as the formula ∀z∃x ϕ with strict semantics. 6 We write T sand Tfor truth with the standard Tarski semantics. The following proposition shows how team semantics is related to Tarski semantics. Proposition 2.3 ([18]).Let ϕ∈FOLand let sbe an assignment. Then for all FOL-formulas we have MT sϕiff M{s}ϕ. In particular, for all FOLsentences, we have MTϕiff M{∅} ϕ. Note that, by flatness, MXϕiff MT sϕfor all s∈X. In this sense we can say that team semantics for FO is a generalization of Tarski semantics. By Proposition 2.3 it is natural to write Mϕwhen we mean M{∅} ϕ. Note that M∅ϕholds trivially for all FOL-formulas ϕby Definition 2.1. In general we say that any logic Lwith team semantics has empty team property if M∅ϕholds for all L-formulas ϕ. We say that a logic Lis local if the truth of formulas is determined only by the values of the free variables in a team, i.e. the following holds for all L-formulas ϕ. MXϕiff MXFr(ϕ)ϕ, where XFr(ϕ) := {sFr(ϕ)|s∈X}and sFr(ϕ)is an assignment such that dom(sFr(ϕ)) = Fr(ϕ)and (sFr(ϕ))(x) = s(x)for each x∈Fr(ϕ). FO is clearly local by Propositions 2.2 and 2.3. We define two more important properties for any logic Lwith team semantics. Definition 2.2. Let Lbe a logic with team semantics. We say that • L is closed downwards if the following implication holds: If MXϕand Y⊆X, then MYϕ. • L is closed under unions if the following implication holds: If MXiϕfor every i∈I, then M∪i∈IXiϕ. By flatness, FO is both closed both downwards and under unions. 2.2. Inclusion and exclusion logics Inclusion and exclusion logics are obtained by adding inclusion and exclusion atoms, respectively, to FO with team semantics. By allowing the use of the both of these atoms we get inclusion-exclusion logic which is our main topic of interest in this paper. We first present the syntax and semantics for inclusion logic (INC). Definition 2.3. If ~ t1,~ t2are k-tuples of L-terms, ~ t1⊆~ t2is a k-ary inclusion atom. The language INCLis defined as FOL, except that (non-negated) inclusion atoms – of any arity – may be used as literals. 7 Let Mbe a model and Xa team s.t. Vr(~ t1 ~ t2)⊆dom(X). We define the truth of ~ t1⊆~ t2in the model Mand the team X: MX~ t1⊆~ t2iff for all s∈Xthere exists s0∈Xs.t. s(~ t1) = s0(~ t2). This truth condition can be written equivalently as follows: MX~ t1⊆~ t2iff X(~ t1)⊆X(~ t2). Example 2.1. Let ~ t1,...,~ tmbe k-tuples of L-terms and ~x ak-tuple of fresh variables. Now the following holds for all nonempty teams X: MX∀~x _ i≤m ~x ⊆~ tiiff [ i≤m X(~ ti) = Mk. In particular, for t∈TLand X6=∅we have MX∀x(x⊆t)iff X(t) = M. Note that this property is not closed downwards and thus it cannot be expressed in dependence logic (which is closed downwards as shown in [18]). Next we present the syntax and semantics for exclusion logic (EXC). Definition 2.4. If ~ t1,~ t2∈TLare k-tuples, ~ t1|~ t2is a k-ary exclusion atom. The language EXCLis defined using by exclusion atoms as literals in FOL. Let Mbe a model and Xa team s.t. Vr(~ t1 ~ t2)⊆dom(X). We define the truth of ~ t1|~ t2in the model Mand the team X: MX~ t1|~ t2iff for all s, s0∈X:s(~ t1)6=s0(~ t2). This truth condition can be written equivalently as follows: MX~ t1|~ t2iff X(~ t1)∩X(~ t2) = ∅. In inclusion-exclusion logic (INEX) we may use both inclusion and exclusion atoms, and the corresponding language is denoted by INEXL. INC and EXC have both been shown local2. By the truth definitions of inclusion and exclusion atoms, it is easy to see that INC and EXC both satisfy empty team property. Hence also INEX satisfies these properties. Neither inclusion nor exclusion logic has flatness-property. Galliani [4] has shown that INC is closed under unions, 2Exclusion logic has been shown equivalent with dependence logic ([4]) which is known to be local ([18]). Inclusion logic has been shown local by Galliani [4], but for this proof the lax semantics is required. With strict semantics the locality of INC is lost, which is one of the reasons why the lax semantics is considered to be a more natural choice to be used in team semantics. Inclusion logic with strict semantics has also been studied (see for example [9]). 8 but not downwards. On the other hand, EXC is closed downwards but not under unions ([18]). Hence INEX is not closed downwards nor under unions. Definition 2.5. If ϕ∈INEXLcontains at most k-ary inclusion and exclusion atoms, we say that ϕis an INEXL[k]-formula. By allowing only the use of these formulas, we obtain k-ary inclusion-exclusion logic, denoted by INEX[k]. Furthermore, k-ary inclusion logic (INC[k]) and k-ary exclusion logic (EXC[k]) are defined analogously. Note that the exclusion atom ~ t1|~ t2is not the contradictory negation of the inclusion atom ~ t1⊆~ t2, and that the former is symmetric while the latter is not (that is, ~ t1|~ t2≡~ t2|~ t1but ~ t1⊆~ t26≡ ~ t2⊆~ t1). The contradictory negations of k-ary inclusion and exclusion atoms can be defined in INEX[k]for nonempty teams, as shown by the following example. Example 2.2. Let Mbe a model, Xa nonempty team, ~ t1,~ t2∈TLk-tuples and ~x ak-tuple of variables. It is easy to see that we have M2X~ t1|~ t2iff MX∃~x (~x ⊆~ t1∧~x ⊆~ t2) M2X~ t1⊆~ t2iff MX∃~x (~x ⊆~ t1∧~x |~ t2). If we would use negated inclusion/exclusion atoms with the semantics of the contradictory negation in INEX, we would lose empty team property since the contradictory negations of these atoms are false in the empty team. But for nonempty teams, this extension would not give us any more expressive power. Observation 2.1. In team semantics contradictory negation is not equivalent with the negation ¬that is used with literals. This is because, if ϕis of the form ~ t1=~ t2or R~ t, the claims M2Xϕand MX¬ϕare not necessarily equivalent when |X|>1. Since inclusion and exclusion atoms are atomic formulas as (non-negated) literals, their negations should behave similarly as the negations of literals. Therefore, if we would define negated inclusion or exclusion atoms, the semantics of contradictory negation would not be a natural choice for it. We will discuss further the issue of sensible semantics for negated atoms in the end of of Section 4. 3. Defining new operators for inclusion-exclusion logic In this section we will define several useful operators for INEX[k]. First we will define constancy atoms and intuitionistic disjunction. Then we will introduce inclusion and exclusion quantifiers which present a new approach to inclusion and exclusion dependencies. Then we define a new operator called term value preserving disjunction which will be essential for our translation from ESO[k]to INEX[k]in the next section. Finally we will introduce a method 9 Let Y:= {s∈X3|s(~x)∈X3(~ t)}and Y0:= {s∈X3|s(~x)∈X3(~ t)}. Now clearly Y∪Y0=X3,MY~x =~y and MY0~x =~z. Also it is quite easy to see that X[X(~ t)/~x ] = Ydom(X1)and X[X(~ t)/~x ] = Y0dom(X1), whence by locality MYψand MY0θ. Hence MX3(~x =~y ∧ψ)∨(~x =~z ∧θ), and furthermore we have MXξ. For a more detailed proof, see [17]. By using Claim 1, we can easily prove the truth conditions for universal inclusion and exclusion quantifiers (Proposition 3.5). We only need to consider the use of storing operator and the special case when X(~ t) = Mk. When using the storing operator, we may drop the extra assumption that Vr(~x)∩Vr(~ t) = ∅. When X(~ t) = Mkthe universal inclusion quantifier (∀~x ⊆~ t)becomes the normal universal quantifier ∀~x and the universal exclusion quantifier (∀~x |~ t) becomes trivially true. For the rest of the proof we apply Claim 1 with ψ:= ϕ and θ:= (~x =~x)for (∀~x ⊆~ t)ϕ, and ψ:= (~x =~x)and θ:= ϕfor (∀~x |~ t)ϕ. For all technical details, see [17]. A natural idea for the truth definition for universal inclusion quantification (∀~x ⊆~y )is “∀~x ∈Mk: (~x ⊆~y ⇒ϕ)”. This intuition would give us the following definition: (∀~x ⊆~y )ϕ:= ∀~x (~x |~y ∨ϕ). However, this simple idea does not work for two reasons. Firstly, there might be too many values chosen for ~x on the right side of the disjunction, which can be a problem since INEX is not closed downwards. Secondly, the exclusion atom is evaluated after splitting the team and thus some of the original values for ~y might be lost. This general problem regarding the “loss of information” when evaluating disjunctions will be discussed more in the Subsection 3.4, where we define term value preserving disjunction. 3.3. Analyzing the properties of inclusion and exclusion quantifiers In the previous subsections we showed that inclusion and exclusion quantifiers can be expressed with inclusion and exclusion atoms, and thus we were able to define them as abbreviations in INEX. In this subsection we take a reverse perspective by considering them as basic operations to be added to FO and examining the expressive power of the resulting logics. The following observation shows that we can define inclusion and exclusion atoms with existential inclusion and exclusion quantifiers (∃~x ⊆~ t)and (∃~x |~ t). Observation 3.1. Let ~ t1,~ t2be k-tuples of L-terms and let ~x be a k-tuple of fresh variables. Now it holds that: MX~ t1⊆~ t2iff MX(∃~x ⊆~ t2)(~x =~ t1). MX~ t1|~ t2iff MX(∃~x |~ t2)(~x =~ t1), 16 We explain briefly why these equivalences hold. We first notice that for any function F:X→ P∗(Mk)the following holds: MX[F/~x ]~x =~ t1iff F(s) = {s(~ t1)}for each s∈X. (?) It is easy to see that if Fis a function which satisfies the (both) sides of (?), then we have: ran(F)⊆ P∗(X(~ t2)) if and only if MX~ t1⊆~ t2. The first equivalence follows from this. The second one is also clear since ran(F)⊆ P∗(X(~ t2)) iff MX~ t1|~ t2, for any Fwhich satisfies the both sides of (?). Recall that, in Definition 3.4, we were able to define the quantifier (∃~x ⊆~ t) with inclusion atom and the quantifier (∃~x |~ t)with exclusion atom. Hence, by the previous observation, if we extend FO with quantifiers (∃~x ⊆~ t)or (∃~x |~ t), we obtain equivalent logics with INC and EXC, respectively. We call these logics inclusion and exclusion friendly logics due their similarity with IF-logic. By using the both of these quantifiers, we obtain inclusion-exclusion friendly logic that is equivalent with INEX. Also note that the arities of these operations match, since the use of existential inclusion (exclusion) quantifiers for k-tuples corresponds to the use of k-ary inclusion (exclusion) atoms. Hence the use of existential inclusion and exclusion quantifiers for single first order variables corresponds to the use of unary inclusion and exclusion atoms, and thus, by extending FO with either/both of them, we obtain logics equivalent to INC[1],EXC[1] and INEX[1]. After the Observation 3.1 it is natural to ask whether we can define inclusion and exclusion atoms alternatively by using universal inclusion and exclusion quantifiers (∀~x ⊆~ t)and (∀~x |~ t). This can also be done, however, this time inclusion atom is defined with universal exclusion quantifier and exclusion atom is defined with universal inclusion quantifier. Observation 3.2. Let ~ t1,~ t2be k-tuples of L-terms and let ~x be a k-tuple of fresh variables. Now the following equivalences hold: MX~ t1⊆~ t2iff MX(∀~x |~ t2)(~x 6=~ t1) MX~ t1|~ t2iff MX(∀~x ⊆~ t2)(~x 6=~ t1), We prove the first equivalence by contraposition: Suppose that M2X~ t1⊆~ t2, i.e. there is s∈Xsuch that s(~ t1)/∈X(~ t2). Let r:= s[s(~ t1)/~x ], whence r∈X[X(~ t2)/~x ]. Now r(~x) = s(~ t1) = r(~ t1)and thus M2X(∀~x |~ t2)(~x 6=~ t1). For the other direction suppose that M2X(∀~x |~ t2)(~x 6=~ t1), whence there is r∈X[X(~ t2)/~x ]such that r(~x) = r(~ t1). Now there is s∈Xand ~a ∈X(~ t2) such that r=s[~a/~x ]. But since s(~ t1) = r(~ t1) = r(~x) = ~a /∈X(~ t2), we have M2X~ t1⊆~ t2. The second equivalence can be proven by a similar reasoning. 17 When we combine the equivalences above with the respective equivalences in Observation 3.1, we obtain the following correspondence. (∃~x ⊆~ t2)(~x =~ t1)≡(∀~x |~ t2)(~x 6=~ t1) (∃~x |~ t2)(~x =~ t1)≡(∀~x ⊆~ t2)(~x 6=~ t1). Here we have an interesting duality between the inclusion and exclusion quantifiers. This leads to a natural question whether existential inclusion quantifier (∃~x ⊆~ t)has the same expressive power as universal exclusion quantifier (∀~x |~ t), and the whether the same holds for the quantifiers (∃~x |~ t) and (∀~x ⊆~ t). We approach this question by first comparing universal inclusion/exclusion quantifiers with INC and EXC. In Definition 3.5 we defined universal inclusion and exclusion quantifiers in INEX by using both inclusion and exclusion atoms. We examine next whether either of them could be defined by using only one type of these atoms. For the next observation, recall that EXC is closed downwards and INC under unions. Observation 3.3. Let M= (I, M)be an L-model s.t. M={0,1,2}, and let X1={s01}and X2={s10}, where s01(x) = 0 = s10(y)and s01(y) = 1 = s10(x). (A) We first show that universal inclusion quantifier is not closed under unions. For this, let ϕ:= (∀z⊆x)(y6=z). We consider the following teams Y1:= X1[X1(x)/z] = X1[{0}/z] = {s01[0/z]} Y2:= X2[X2(x)/z] = X2[{1}/z] = {s10[1/z]} Y3:= (X1∪X2)h(X1∪X2)(x)/zi= (X1∪X2)[{0,1}/z] ={s01[0/z], s01[1/z], s10[0/z], s10[1/z]}. Now we have MY1y6=zand MY2y6=z, but M2Y3y6=z. Hence MX1ϕ and MX2ϕ, but M2X1∪X2ϕ. (B) Next, we show that universal exclusion quantifier is not closed under unions. Let ψ:= (∀z|x)(y⊆z). Note that, by Observation 3.2, y⊆zcan be expressed with universal exclusion quantifier (ψ≡(∀z|x)(∀w|z)(w6=y)). Let Z1:= X1hX1(x)/zi=X1h{0}/zi=X1[{1,2}/z] = {s01[1/z], s01[2/z]} Z2:= X2hX2(x)/zi=X2h{1}/zi=X2[{0,2}/x] = {s10[0/z], s10[2/z]} Z3:= (X1∪X2)h(X1∪X2)(x)/zi= (X1∪X2)h{0,1}/zi = (X1∪X2)[{2}/z] = {s01[2/z], s10[2/z]}. Since Z1(y) = {1}⊆{1,2}=Z1(z)and Z2(y) = {0} ⊆ {0,2}=Z2(z), we have MZ1y⊆zand MZ2y⊆z. But because Z3(y) = {0,1} 6⊆ {2}=Z3(z), 18 we have M2Z3y⊆z. Hence MX1ψand MX2ψ, but M2X1∪X2ψ. (C) Finally, we show that universal exclusion quantifier is not closed downwards either. Let θ:= (∀z|x)(y6=z)and let Z1, Z3be as above. Now MZ3y6=z, but M2Z1y6=z. Hence MX1∪X2θ, but M2X1θ; even though X1⊆X1∪X2. By this observation, universal exclusion quantifier cannot be defined in EXC and neither universal inclusion nor exclusion quantifier can be defined in INC. But there is still a possibility that universal inclusion quantifier could be defined in EXC. It turns out that this can indeed be done, but we must give its definition in a form that would not work properly in INEX. To make distinction with the earlier definition, we denote this quantifier (∀~x ⊆e~ t), where “e” stands for “exclusion”, as this operator is defined for exclusion logic only. Definition 3.6. Let ϕ∈EXCL,~ t∈TLak-tuple, ~x ak-tuple of variables and ~u, ~y k-tuples of fresh variables. We use the following notation: (∀~x ⊆e~ t)ϕ:= ∀~x ϕ t[~ t . ~u ]∀~x (∃~y |~u)(~y=~x ∨ϕ). Since intuitionistic disjunction can be defined with unary exclusion atoms we have (∀~x ⊆e~ t)ϕ∈EXCL[k]when ϕ∈EXCL[k](for any k≥1). Proposition 3.6. With the same assumptions as in Definition 3.6, we obtain the following truth condition: MX(∀~x ⊆e~ t)ϕiff MX[X( ~ t)/~x ]ϕ. The proof for this truth condition can be done using a similar reasoning as for the standard inclusion quantifier (∀~x ⊆~ t). Note that since EXC is closed downwards, the truth of ∀~x ϕ in Ximplies that MX[X( ~ t)/~x ]ϕ. Also, again by downwards closure, when the team X[Mk/~x ]is split into two subteams, if MYϕfor some team Yfor which X[X(~ t)/~x ]⊆Y, then also MX[X( ~ t)/~x ]ϕ. For a full proof with all technical details, see [17]. For proving the truth condition for (∀~x ⊆e~ t)we had to use the assumption of downwards closure which does not hold for INEX. Moreover, the claim of Proposition 3.6 is not necessarily true when ϕ∈INEXLsince, for example, if ϕ:= ∀x(x⊆y)and X(z)6=M, then MX(∀y⊆ez)ϕ, but M2X(∀y⊆z)ϕ. By the observation above, we see that definability of these quantifiers, as well as many other operators for team semantics, is “case sensitive”. That is, if a certain operator Ois definable in a logic Land L0is an extension of L, then the operator Omay have to be defined differently in L0. Note that atoms in team semantics are more regular in this sense, since if a certain atom Ais definable in a logic L, then Acan be defined in all of the extensions of Lidentically as it is defined in L. Since we were able to define universal inclusion quantifier (∀~x ⊆~ t)in EXC, it would have been natural to predict that universal exclusion quantifier (∀~x |~ t) 19 is dually definable in INC. However, this is impossible since this operator is not closed under unions as shown in Observation 3.3. Here we have an interesting piece of asymmetry between the inclusion and exclusion operators. In this subsection we were able to show that existential inclusion and exclusion quantifiers are very closely related to inclusion and exclusion atoms. However, perhaps a bit surprisingly, with universal inclusion and exclusion quantifiers, this relationship becomes more complicated. One interesting question, that is still open, is the exact expressive power of universal exclusion quantifier. For now, we only know that when ~x and ~ tare k-ary, then (∀~x |~ t) is (strictly) stronger than k-ary inclusion atom. However, it is possible that this difference would disappear on the level of sentences – that is, FO extended with (∀~x |~ t)(where ~x,~ tare k-ary) would become equivalent with INC[k] when we only consider sentences. We leave this question open for further research. 3.4. Term value preserving disjunction When evaluating disjunctions, the team is split and usually some information is lost about the values of terms in the original team. Often this is desirable, since we want to shrink or distribute the values of certain variables by giving conditions on the disjuncts. However, sometimes we want that the values of certain terms (or tuples of terms) are preserved on both sides after the evaluation of the disjunction. This is desirable especially when we are using variables to carry information about sets (or tuples of variables to carry information about relations). This method will be crucial in the proof of Theorem 4.5 later in this paper. For this purpose we introduce term value preserving disjunction. It can be defined by using constancy atoms, intuitionistic disjunctions and inclusion atoms of the same arity as the lengths of the tuples whose values we want to preserve. Thus, with this operator, the values of single terms can be preserved in INEX[1] and the values of k-tuples of terms can be preserved in INEX[k]. Definition 3.7. Let ~ t1,...,~ tnbe k-tuples of L-terms, ϕ, ψ ∈INEXLand cl, cr, y fresh variables. We define ϕ∨ ~ t1,..., ~ tn ψ:= (ϕtψ)t ∃ cl∃cr=(cl)∧=(cr)∧cl6=cr ∧ ∃ y((y=cl∧ϕ)∨(y=cr∧ψ)) ∧^ i≤n (θi∧θ0 i), θi:= ∃~z1∃~z2((y=cl∧~z1=~ ti∧~z2=~c1) ∨(y=cr∧~z1=~c1∧~z2=~ ti)) ∧~ ti⊆~z1∧~ ti⊆~z2 θ0 i:= ∃~z1∃~z2((y=cl∧~z1=~ ti∧~z2=~c2) ∨(y=cr∧~z1=~c2∧~z2=~ ti)) ∧~ ti⊆~z1∧~ ti⊆~z2, 20 where ~z1, ~z2,~c1,~c2are k-tuples of variables such that the tuples ~z1, ~z2consist of fresh variables, and ~c1,~c2are defined as ~c1:= cl. . . cland ~c2:= cr. . . cr. The next proposition gives the truth condition for this operator. Note that this truth condition is the same as for the normal disjunction with an extra condition that the values for the tuples ~ t1,...,~ tnmust be preserved on both sides after splitting the team (supposing that the split is nontrivial). Proposition 3.7. With the same assumptions as in Definition 3.7, we obtain the following truth condition: MXϕ∨ ~ t1,..., ~ tn ψiff there are Y, Y 0⊆Xs.t. Y∪Y0=X, MYϕ, MY0ψ and if Y, Y 06=∅,then Y(~ ti)=X(~ ti)=Y0(~ ti)for all i≤n. Before presenting a proof for this proposition, we explain its idea here briefly: We first check if the splitting can be done so that one of the sides is the empty team. In this case we don’t set any requirements since all INEXLformulas are true in the empty team and on the other side values are trivially preserved since it has to be the whole team X. Otherwise we fix two constants cl, crwhich correspond to the left hand and right hand sides of the disjunction. Then we attach a “label” yto each assignment in the team. This label can be either cl,cror both depending on if the assignment in question will be placed on the left, on the right or both. Since these labels are attached before doing the actual splitting, we can check beforehand that the information will be preserved. The truth of formula θiguarantees that values of term tiwill be preserved on both sides for all values, expect possibly for the value of ~c1which is a constant. The formula θ0 idoes the same, but it cannot make sure that the value for the constant ~c2is preserved. But the truth of both θiand θ0 iguarantees that the values for ~ tiare indeed preserved on both sides. Proof. (Proposition 3.7) In this proof we use the abbreviation ϕYψ:= ϕ∨ ~ t1,..., ~ tn ψ. If Xwould be an empty team, the claim would hold trivially, and thus we may assume that X6=∅. By locality we may also assume that cl, cr, y /∈dom(X). Suppose first that MXϕYψ. Now either MXϕtψor MX∃cl∃cr=(cl)∧=(cr)∧cl6=cr ∧ ∃ y((y=cl∧ϕ)∨(y=cr∧ψ)) ∧^ i≤n (θi∧θ0 i).(?) Suppose first that MXϕtψ, i.e. MXϕor MXψ. If MXϕ, then we can choose Y:= Xand Y0:= ∅, when the claim holds trivially. Analogously 21 if MXψ, we can choose Y:= ∅and Y0:= X. Suppose then that (?) holds. Now there exist F1:X→ P∗(M)and F2:X[F1/cl]→ P∗(M)such that MX1=(cl)∧=(cr)∧cl6=cr ∧ ∃ y((y=cl∧ϕ)∨(y=cr∧ψ)) ∧^ i≤n (θi∧θ0 i), where X1:= X[F1/cl, F2/cr]. Since MX1=(cl),MX1=(cr),MX1cl6=cr and X6=∅, there exist a, b ∈Msuch that X1(cl) = {a},X1(cr) = {b}and a6=b. There also exists a function F3:X1→ P∗(M)such that MX2((y=cl∧ϕ)∨(y=cr∧ψ)) ∧^ i≤n (θi∧θ0 i),where X2:= X1[F3/y]. Now there exist Z1, Z0 1⊆X2, such that Z1∪Z0 1=X2,MZ1y=cl∧ϕand MZ0 1y=cr∧ψ. Since X2(cl) = {a},X2(cr) = {b}and a6=b, it is easy to see that the following holds for each s∈X2: s∈Z1iff s(y) = aand s∈Z0 1iff s(y) = b. Let Y:= Z1dom(X)and Y0:= Z0 1dom(X). Since MZ1ϕand MZ0 1ψ, we have MYϕand MY0ψby locality. Because Z1∪Z0 1=X2, we must also have Y∪Y0=X(recall that we assumed that cl, cr, y /∈dom(X)). We still need to show that the values of ~ ti(i≤n) are preserved when Xis split into Yand Y0. For the sake of showing this, let i≤n, whence MX2θi∧θ0 i. In particular MX2θiand thus there are F1:X2→ P∗(Mk) and F2:X2[F1/~z1]→ P∗(Mk)such that MX3(y=cl∧~z1=~ ti∧~z2=~c1) ∨(y=cr∧~z1=~c1∧~z2=~ ti)∧~ ti⊆~z1∧~ ti⊆~z2, where X3=X2[F1/~z1,F2/~z2]. Now there are Z2, Z0 2⊆X3s.t. Z2∪Z0 2=X3 and    MZ2y=cl∧~z1=~ ti∧~z2=~c1 MZ0 2y=cr∧~z1=~c1∧~z2=~ ti. Let ~a := (a, . . . , a)and ~ b:= (b, . . . , b). For the sake of showing that X(~ ti)⊆ Y(~ ti)∪{~a}, let ~c ∈X(~ ti). Now there is s∈Xsuch that s(~ ti) = ~c, whence there is r∈X3such that r(~ ti) = s(~ ti). Since MX3~ ti⊆~z1, there exists r0∈X3 such that r0(~z1) = r(~ ti). Now we have ~c =s(~ ti) = r(~ ti) = r0(~z1). Suppose first r0∈Z2. Then r0(~z1) = r0(~ ti)and r0(y) = r0(cl) = a. Hence there is s0∈Ys.t. s0(~ ti) = r0(~ ti). Now ~c =r0(~z1) = r0(~ ti) = s0(~ ti)∈Y(~ ti). If r0/∈Z2, then r0∈Z0 2, whence we have ~c =r0(~z1) = r0(~c1) = r0(cl. . . cl) = ~a. Hence in either case ~c ∈Y(~ ti)∪ {~a}and thus X(~ ti)⊆Y(~ ti)∪ {~a}. 22 By using the fact that MX2θ0 i, we can analogously deduce the inclusion X(~ ti)⊆Y(~ ti)∪ {~ b}. Since ~a 6=~ b, it thus has to be that X(~ ti)⊆Y(~ ti). Clearly Y(~ ti)⊆X(~ ti), and therefore we have Y(~ ti) = X(~ ti). By using a symmetric argumentation we can also show that Y0(~ ti) = X(~ ti). Suppose then that there exist Y, Y 0⊆Xsuch that Y∪Y0=X,MYϕand MY0ψ, and if Y, Y 06=∅, then we have Y(~ ti)=Y0(~ ti)=X(~ ti)for each i≤n. If Y=∅, then Y0=Xand thus MXψ. Therefore MXϕtψand thus MϕYψ. And if Y0=∅, we obtain MϕYψby a similar argumentation. Hence we may assume Y, Y 06=∅, whence Y(~ ti) = Y0(~ ti) = X(~ ti)for each i≤n. We first examine the special case when |M|= 1. Because X6=∅, the team Xhas to be a singleton {s}for some s. Since Y, Y 06=∅, we have Y=Xand Y0=X. Therefore MXϕtψand thus we have MXϕYψ. Hence we may assume that |M| ≥ 2, whence there are a, b ∈Msuch that a6=b. Let F1:X→ P∗(M)s.t. s7→ {a}and let F2:X[F1/cl]→ P∗(M)s.t. s7→ {b}. We write X1:= X[F1/cl, F2/cr]. By the definitions of F1and F2, we clearly have MX1=(cl),MX1=(cr)and MX1cl6=cr. Let F3:X1→ P∗(M)s.t.        s7→ {a}if sdom(X)∈Y\Y0 s7→ {b}if sdom(X)∈Y0\Y s7→ {a, b}if sdom(X)∈Y∩Y0. We define the following teams X2:= X1[F3/y],Z1:= {s∈X3|s(y) = a} and Z0 1:= {s∈X3|s(y) = b}. Now it clearly holds that Z1∪Z0 1=X2, MZ1y=cland MZ0 1y=cr. By locality and the definition of F3, we have MZ1ϕand MZ0 1ψ. Therefore MX2(y=cl∧ϕ)∨(y=cr∧ψ). Let i≤n. We define ~a := (a, . . . , a)and                F1:X2→ P∗(Mk)s.t.    s7→ {s(~ ti)}if s(y) = a s7→ {~a}if s(y) = b F2:X2[F1/~z1]→ P∗(Mk)s.t.    s7→ {~a}if s(y) = a s7→ {s(~ ti)}if s(y) = b. Let X3:= X2[F1/~z1,F2/~z2],Z2:= {s∈X3|s(y) = a}and Z0 2:= {s∈X3| s(y) = b}. Now Z2∪Z0 2=X3and by the definitions of F1and F2we have MZ2y=cl∧~z1=~ ti∧~z2=~c1and MZ0 2y=cr∧~z1=~c1∧~z2=~ ti. For the sake of showing that MX3~ ti⊆~z1, let r∈X3. Now there is s∈X, s.t. r(~ ti) = s(~ ti). Since s(~ ti)∈X(~ ti) = Y(~ ti), there is s0∈Y, such that s0(~ ti) = s(~ ti). Let r0:= s0[a/cl, b/cr, a/y, s0(~ ti)/~z1,~a/~z2]. Now r0∈X3and r(~ ti) = s(~ ti) = s0(~ ti) = r0(~z1). Hence MX3~ ti⊆~z1. Analogously we can show 23 that MX3~ ti⊆~z2and thus MX2θi. By a similar argumentation MX2θ0 i and thus MX2Vi≤n(θi∧θ0 i). Hence (?) holds, and therefore MXϕYψ. Term value preserving disjunction has several natural variants. The version we defined requires that the values of given tuples of terms are preserved both on the left and right side of the disjunction. We could weaken this condition by requiring these values to be preserved only on the left, only on the right or only on either of the sides without specifying which. Or we could modify this condition by requiring different tuples of terms to be preserved on the left and different tuples to be preserved on the right. Now we allow the splitting to be done in such a way that either of the sides becomes empty, which is natural for our needs since INEX has empty team property. But strictly speaking, the values of the given terms are not necessarily preserved in this case, since there are no values in the empty team. If we require values to be preserved in then as well, we can additionally require that splitting must be done in a way that neither of the sides becomes empty. If we only require this condition – ignoring the values of any terms – we obtain a disjunction that can be seen as a dual operator for intuitionistic disjunction4. We will not go into details here, but all of the variants described above can be defined in INEX. We just need to do some simple modifications on the formula that defines term value preserving disjunction in Definition 3.7. In this paper we use term value preserving disjunction only as a useful tool in INEX, but it would be interesting to study the properties and the expressive power of this operator (or some of its variants) independently. 3.5. Relativization method for team semantics In this subsection we introduce an application which uses several of the new operators that we have defined in this section. Suppose that ϕis an INEXLsentence and y /∈Vr(ϕ)is a variable in the domain of a team X. If we replace all quantifiers ∃x, ∀xin ϕwith the corresponding inclusion quantifiers (∃x⊆y), (∀x⊆y), the evaluation of the resulting formula is identical to evaluation of ϕ, except that the quantifiers in ϕmay only choose values within the values of y. If we further replace disjunctions in ϕwith the ones that preserve the value of y, then the quantifications may only choose values within the set X(y)(the initial values of yin X). Since the resulting formula only “sees” the part of model that is restricted to the set X(y), we call this method relativization. Definition 3.8. Let ϕbe an INEXL-sentence and let y /∈Vr(ϕ)be a variable. 4Intutionistic disjunction states that the splitting must be done in a way that either of the sides becomes empty – a dual condition is that neither of the sides can be left empty. 24 The relativization of ϕon y, denoted by ϕy, is defined recursively: ψy=ψif ψis a literal or inclusion/exclusion atom (ψ∧θ)y=ψy∧θy (ψ∨θ)y=ψyYθy, where Y:= ∨ y (∃x ψ)y= (∃x⊆y)(ψy) (∀x ψ)y= (∀x⊆y)(ψy). Note that since ϕis a sentence, we have Fr(ϕy) = {y}. Let Xbe a team and y∈dom(X)\Vr(ϕ). If ϕdefines some property of the domain of a model, then the formula ϕydefines the same property of the set values for yin the team X. This is proven in Proposition 3.8 below. This proposition could be proven also for many other logics Lwith team semantics. If the following assumptions hold for L, the proof can be done identically as it is done here: Lis an extension of FO with new atomic formulas, it is local, has empty team property, and inclusion quantifiers (for single variables) and term value preserving disjunction (for single terms) can expressed in L. Note that in order to express these operators, it would suffice that we could use unary inclusion and exclusion atoms in L. If M= (I, M)is an L-model and A⊆M, the notation MAdenotes the submodel of Mthat is relativized on A. That is, the universe of MAis the set Aand the symbols in Lare interpreted as: RMA=RMAnfor n-ary relation symbols R∈L,fMA=fMAnfor n-ary function symbols f∈L and cMA=cMfor constant symbols c∈L. Note that if Lcontains function or constant symbols, then MAcan be an L-model only if fMAn:An→A for all each n-ary f∈Land cM∈Afor each c∈L. But if Lis relational, then MAis an L-model for any A⊆M. Proposition 3.8. Let ϕbe an INEXL-sentence and ybe a variable such that y /∈Vr(ϕ). Now MXϕyiff MX(y)ϕ for all L-models Mand teams Xsuch that MX(y)is an L-model. Proof. We first show that If MXµy, then MX(y)Xµ, (R1) for all µ∈Sf(ϕ)and teams Xfor which the following condition holds: X(z)⊆X(y)for all z∈dom(X).(?) 25 Note that since µ0and µ0 ido not contain the relation variable R, we can replace the model M[~ A/~ P]with the model M[~ A/~ P, X(~y )/R]in Claim 3. The existence of s∈Xfor each tuple ~a ∈Aisuch that s[~a/~u ]satisfies ϕ0 i, guarantees that the values in Aiare included in the values~ t2in the team when the inclusion atom (~ t1⊆~ t2)iis evaluated. With this result we can prove the claim of this theorem; that is MXϕiff M[X(~y )/R]Φ. Suppose first that MXϕ. Now by Claim 3 there are A1, . . . , An⊆Mk s.t. M0Xϕ0, and for all i≤nand ~a ∈Aithere exists s∈Xsuch that M0{s[~a/~u ]}ϕ0 i, where M0=M[~ A/~ P, X(~y )/R]. Let j≤nand let Y:= {r∈ {∅}[Mk/~u ]|r(~u)/∈Aj}and Y0:= {r∈ {∅}[Mk/~u ]|r(~u)∈Aj}. Now Y∪Y0={∅}[Mk/~u ]and because Aj=PM0 j, clearly M0Y¬Pj~u. By the definition of Y0, we have r(~u)∈Ajfor each r∈Y0. Hence, by applying the result of Claim 3 for the values r(~u), the following holds: for each r∈Y0there exists sr∈Xs.t. M0{sr[r(~u)/~u ]}ϕ0 j. Let F:Y0→ P∗(Mm)s.t. r7→ {sr(~y)}. Now r[sr(~y)/~y ] = sr[r(~u)/~u ]for each r∈Y0and thus M0{r[sr(~y)/~y ]}ϕ0 jfor each r∈Y0. Hence by locality and flatness M0Y0[F/~y ]ϕ0 j. Because sr(~y)∈X(~y ) = RM0for each r∈Y0, by flatness we also have M0Y0[F/~y ]R~y and thus M0Y0∃~y (R~y ∧ϕ0 j). Therefore M0{∅}[Mk/~u ]¬Pj~u∨∃ ~y (R~y∧ϕ0 j)and thus M0Vi≤n∀~u (¬Pi~u ∨∃ ~y (R~y∧ϕ0 i)). Because M0Xϕ0and X(~y ) = RM0, by locality M0∀~y (¬R~y ∨(R~y∧ϕ0)). Therefore we can conclude that M[X(~y )/R]Φ. Suppose then that M[X(~y )/R]Φ. Thus there exist A1, . . . , An⊆Mksuch that the first order part of Φholds in M0:= M[~ A/~ P, X(~y )/R]. In particular, M0∀~y (¬R~y ∨(R~y ∧ϕ0)) and thus by locality M0Xϕ0. For the sake of proving the right side of the equivalence of Claim 3, let j≤nand ~a ∈Aj. Now M0∀~u (¬Pj~u ∨ ∃ ~y (R~y ∧ϕ0 j)), and thus there are Y, Y 0⊆ {∅}[Mk/~u ]such that Y∪Y0={∅}[Mk/~u ],M0Y¬Pj~u and M0Y0∃~y (R~y ∧ϕ0 j). Hence there is a function F:Y0→ P∗(Mm)such that M0Y0[F/~y ]R~y ∧ϕ0 j. Let r:= ∅[~a/~u ], whence r∈ {∅}[Mk/~u ]. Since r(~u) = ~a ∈Aj=PM0 j and M0Y¬Pj~u, we have r /∈Yand thus r∈Y0. Let ~ b∈ F(r)and let s:= r[~ b/~y ]. By flatness, M0{s}R~y and thus s(~y)∈RM0=X(~y ). Hence there exists s0∈Xsuch that s0(~y) = s(~y). Since M0{s}ϕ0 j, by locality also M0{s0[s(~u)/~u ]}ϕ0 j. Because s(~u) = r(~u) = ~a, by Claim 3 we have MXϕ. Forming a translation from INEX[k]to ESO[k] The next theorem shows that there is also a translation from INEX[k] to ESO[k]. This translation can be formulated by first eliminating exclusion atoms as in Theorem 4.1 and then inclusion atoms as in Theorem 4.2. 32 Theorem 4.3. Let ϕ(~y )∈INEXL[k]. Now there is an ESOL[k]-formula Φ(R), for which we have MXϕiff M[X(~y )/R]Φ. Proof. Without loss of generality we may assume that each exclusion and inclusion atom in the formula ϕis k-ary. We index the exclusion atoms by (~ t1|~ t2)1,...,(~ t1|~ t2)n. Let P1,...Pnbe k-ary relation variables. Let ψ∈Sf(ϕ). We define the formula ψ0recursively as follows. ψ0=ψif ψis a literal ((~ t1|~ t2)i)0=Pi ~ t1∧ ¬Pi ~ t2for each i≤n (~ t1⊆~ t2)0=~ t1⊆~ t2 (ψ∧θ)0=ψ0∧θ0,(ψ∨θ)0=ψ0∨θ0 (∃x ψ)0=∃x ψ0,(∀x ψ)0=∀x ψ0. We can prove the equivalence of Claim 2 for any µ∈Sf(ϕ)by structural induction on µ: Since inclusion atoms are left as they are, their step in the induction is trivial. Other steps can be proven identically as in the proof of Claim 2 within the proof of Theorem 4.1. Thus we have MXϕiff there exist A1, . . . , An⊆Mks.t. M[~ A/~ P]Xϕ0. Since ϕ0contains only inclusion atoms and Fr(ϕ) = Fr(ϕ0) = Vr(~y), we can apply Theorem 4.2 for ϕ0to get an ESOL-formula Ψ(R)for which we have MXϕ0iff M[X(~y)/R]Ψ. We can now define Φ := ∃P1. . . ∃PnΨ, whence Φis an ESOL-formula with the free relation variable R. Then we have MXϕiff there exist A1,...An⊆Mks.t. M[~ A/~ P]Xϕ0 iff there exist A1,...An⊆Mks.t. M[~ A/~ P, X(~y)/R]Ψ iff M[X(~y)/R]Φ. The result of Theorem 4.3 can be formulated equivalently as follows: All INEX[k]-definable properties of teams are ESO[k]-definable. 4.2. Translation from ESO[k]to INEX[k] When translating from ESO to INEX, our technique is to simulate second order quantification by replacing the quantifications of k-ary relation variables Psimply with quantifications of k-tuples of first order variables ~w. The idea is then to choose such values for ~w that in the resulting team X, the relation 33 X(~w)is the same as the relation that is quantified for the value of P. However, we cannot simulate the quantification of the empty set this way, since the first order variables must be given at least one value. But this problem can be avoided, since any ESO-formula Φcan be written in an equivalent form Φ0 which is satisfied if and only if it is satisfied with nonempty interpretations for the quantified relation variables. This is stated in the following easy lemma (for a proof, see [17]). Lemma 4.4. Let Φ := ∃P1. . . ∃Pnγbe an ESOL[k]-formula, where γis the first order part of Φ. Then there exists δ∈ESOL[0] with the same free relation variables as γsuch that the following holds: MΦiff there exist nonempty A1, . . . , An⊆Mks.t. M[~ A/~ P]δ. Now we are ready to formulate our translation from ESO[k] to INEX[k]. For this translation we must require the given teams to be nonempty and assume that the free relation variables in ESOL[k]-formulas are at most k-ary. But here we can allow the ESOL[k]-formula Φto have any number of free relation variables instead of just one. Suppose that Φdefines some properties p1,...,pmfor relations R1, . . . , Rmrespectively. Then it is natural to say that ϕ(~y1. . . ~ym)∈INEXLis equivalent with Φif the relations X(~y1), . . . , X(~ym) have the properties p1,...,pmin all teams Xin which ϕtrue. Theorem 4.5. Let Φ(R1. . . Rm)∈ESOL[k], where the free relation variables Riare at most k-ary. Let ~y, . . . , ~ymbe k-tuples of fresh variables. Then there exists an INEXL[k]-formula ϕ(~y1. . . ~ym), such that MXϕiff M[X(~y1)/R1, . . . , X(~ym)/Rm]Φ, for all suitable L-models Mand nonempty teams X. Proof. Since Φ∈ESOL[k], it is of the form Φ = ∃P1. . . ∃Pnγ, where P1, . . . , Pn are relation variables and γis the first order part of Φ. Without loss of generality, we may assume that P1, . . . , Pn, R1, . . . , Rmare all distinct and k-ary. Let δbe the formula given by Lemma 4.4 for the formula γ. Now we have MΦiff there exist nonempty A1, . . . , An⊆Mks.t. M[~ A/~ P]δ, (4) for all models Mthat have interpretations for the relation variables R1, . . . , Rm. Let ~w1, . . . , ~wnbe k-tuples of fresh variables. The formula ψ0is defined recur34 sively for each ψ∈Sf(δ): ψ0=ψif ψis a literal and neither Pinor Rj occurs in ψfor any ior j. (Pi~ t)0=~ t⊆~wi,(¬Pi~ t)0=~ t|~wifor all i≤n (Ri~ t)0=~ t⊆~yi,(¬Ri~ t)0=~ t|~yifor all i≤m (ψ∧θ)0=ψ0∧θ0 (ψ∨θ)0=ψ0Yθ0,where Y:= ∨ ~w1,..., ~wn,~y1,...,~ym (∃x ψ)0=∃x ψ0,(∀x ψ)0=∀x ψ0. Now we can define the formula ϕsimply as: ϕ:= ∃~w1. . . ∃~wnδ0. Clearly ϕis an INEXL[k]-formula and Fr(ϕ) = Vr(~y1. . . ~ym)7. Before proving the claim of this theorem need to prove Claims 4 and 5. Claim 4. Let µ∈Sf(δ)and let Xbe a team such that the variables ~w1, . . . , ~wn, ~y1, . . . , ~ymare in dom(X). Let M0:= M[X(~w1)/P1, . . . , X(~wn)/Pn, X(~y1)/R1, . . . , X(~ym)/Rm]. Now we have: If MXµ0,then M0Xµ. We prove this claim by structural induction on µ: •If µis a literal such that neither Pinor Rjoccurs in µfor any i≤nor j≤m, the claim holds trivially since µ0=µ. •Let µ=Pj~ tfor some j(the case µ=Rj~ tis analogous). Suppose that MX(Pj~ t)0, i.e. MX~ t⊆~wj, and let s∈X. Because MX~ t⊆~wj, there exists s0∈Xsuch that s0(~wj) = s(~ t). Now we have s(~ t)∈X(~wj) = PM0 j, and thus M0XPj~ t. •Let µ=¬Pj~ tfor some j(the case µ=¬Rj~ tis analogous). Suppose that MX(¬Pj~ t)0, i.e. MX~ t|~wjand let s∈X. Since MX~ t|~wj, we have s(~ t)6=s0(~wj)for each s0∈X. Therefore s(~ t)/∈X(~wj) = PM0 j, and thus M0X¬Pj~ t. •The case µ=ψ∧θis straightforward to prove. •Let µ=ψ∨θ. Suppose that MX(ψ∨θ)0, i.e. MXψ0Yθ0. Thus there are Y1, Y2⊆Xs.t. Y1∪Y2=X,MY1ψ0and MY2θ0, and if Y1, Y26=∅, 7Also, note that if Φis an ESOL-sentence, then ϕis an INEXL-sentence. 35 then the tuples ~wiand ~yjhave the same set of values in Y1and Y2as they have in X(for each i≤nand j≤m). If Y1=∅, then Y2=Xand thus MXθ0. By the inductive hypothesis M0Xθand thus M0Xψ∨θ. Analogously if Y2=∅, then M0Xψ∨θ. Suppose then that Y1, Y26=∅. Now by the inductive hypothesis we have    M[Y1(~wi)i≤n/~ P, Y1(~yj)j≤m/~ R]Y1ψ M[Y2(~wi)i≤n/~ P, Y2(~yj)j≤m/~ R]Y2θ. Because ~wiand ~yjhave the same set of values in Y1and Y2as in X(for any i≤n,j≤m), we have M0Y1ψand M0Y2θ. Therefore M0Xψ∨θ. •The cases µ=∃x ψ and µ=∀x ψ are straightforward to prove. Claim 5. Let µ∈Sf(δ)and assume that A1, . . . , An, B1, . . . , Bm⊆Mkare nonempty sets. Let X6=∅be a team such that Vr(~y1. . . ~ym)⊆dom(X)and for each i≤mand r∈XFr(µ)the following assumption holds: Xr(~yi) = Bi,where Xr:= {s∈X|sFr(µ) = r}.(?) This condition can be written equivalently as: For each r∈XFr(µ),i≤m and ~ b∈Bithere exists s∈Xsuch that s(Fr(µ)∪Vr(~yi)) = r[~ b/~yi]. That is, each assignment in XFr(ϕ)can be extended to Xwith all of the values in Bi. Now the following implication holds: If M0XFr(µ)µ, then MX0µ0, where M0:= M[~ A/~ P, ~ B/~ R]and X0:= X[A1/~w1, . . . , An/~wn]. We prove this claim by structural induction on µ: •If µis a literal such that neither Pinor Rjoccurs in µ, then the claim holds by locality since µ0=µ. •Let µ=Pj~ tfor some j≤n. Suppose that M0XFr(µ)Pj~ t. Let s∈X0 and let r∈XFr(µ)be an assignment for which r=sFr(µ). Since M0XFr(µ)Pj~ t, we have r(~ t)∈PM0 j=Aj=X0(~wj). Thus there exists s0∈X0 s.t. s0(~wj) = r(~ t). Now s(~ t) = r(~ t) = s0(~wj). Therefore MX0~ t⊆~wj, i.e. MX0(Pj~ t)0. •Let µ=¬Pj~ tfor some j≤n. Suppose that M0XFr(µ)¬Pj~ t. Let s, s0∈ X0and let r∈XFr(µ)be an assignment s.t. r=sFr(µ). Because M0XFr(µ)¬Pj~ t, we have r(~ t)/∈PM0 j=Aj=X0(~wj). Hence it has to be that r(~ t)6=s0(~wj), and thus s(~ t) = r(~ t)6=s0(~wj). Therefore MX0~ t|~wj, i.e. MX0(¬Pj~ t)0. 36 •Let µ=Rj~ tor µ=¬Rj~ tfor some j≤m. Note that because the condition (?) holds for X(with respect to Fr(µ)), we have X(~yj) = Bj. Hence RM0 j= Bj=X(~yj)=X0(~yj), and thus the cases µ=Rj~ tand µ=¬Rj~ tcan be proved analogously as we proved the two previous cases. •The case µ=ψ∧θis straightforward to prove. •Let µ=ψ∨θ. Suppose that M0XFr(µ)ψ∨θ, i.e. there are Y∗ 1, Y ∗ 2⊆X Fr(µ)such that Y∗ 1∪Y∗ 2=XFr(µ),M0Y∗ 1ψand M0Y∗ 2θ. Let Y1:= {s∈X|sFr(µ)∈Y∗ 1}and Y2:= {s∈X|sFr(µ)∈Y∗ 2}. Now Y1Fr(µ) = Y∗ 1,Y2Fr(µ) = Y∗ 2and Y1∪Y2=X. Let Y0 1:= Y1[A1/~w1, . . . , An/~wn]and Y0 2:= Y2[A1/~w1, . . . , An/~wn]. Now X0=Y0 1∪Y0 2. If Y0 1=∅, then Y0 2=X0and thus clearly MX0ψ0Yθ0, i.e MX0(ψ∨θ)0. Analogously if Y0 2=∅, then MX0(ψ∨θ)0. Suppose then that Y0 1, Y 0 26=∅. Since the condition (?) holds for Xwith respect to Fr(µ), by the definition of Y1it is easy to see that (?) holds also for Y1with respect to Fr(µ). Since Fr(ψ)⊆Fr(µ),(?)holds for Y1also with respect to Fr(ψ). Analogously (?)holds for Y2with respect to Fr(θ). Therefore, by the inductive hypothesis, MY0 1ψ0and MY0 2θ0. We also have Y0 1(~wi)=Y0 2(~wi)=Ai=X0(wi)for each i≤n. Furthermore, by the condition (?), Y0 1(~yi) = Y0 2(~yi) = Bi=X0(yi)for each i≤m. Therefore MX0ψ0Yθ0, i.e MX0(ψ∨θ)0. •Let µ=∃x ψ (the case µ=∀x ψ can be proven similarly). Suppose that M0XFr(µ)∃x ψ. Hence there is F:XFr(µ)→ P∗(M)such that M0(XFr(µ))[F/x]ψ. Let G:X→ P∗(M), s 7→ F(sFr(µ)) G0:X0→ P∗(M), s 7→ F(sFr(µ)). Now X[G/x]Fr(ψ)=(XFr(µ))[F/x]and therefore M0X[G/x]Fr(ψ)ψ. Since (?) holds for Xwith respect to Fr(µ), by the definition of G(?) holds for X[G/x]with respect to Fr(ψ). Let X00 := (X[G/x])[A1/~w1, . . . , An/~wn], whence by the inductive hypothesis we have MX00 ψ0. By the definition of G0, we have X00 =X0[G0/x], and thus MX0[G0/x]ψ0. Hence MX0∃x ψ0, i.e. MX0(∃x ψ)0. We are now are finally ready prove the claim of this theorem: MXϕiff M[X(~y1)/R1, . . . , X(~ym)/Rm]Φ. 37 Suppose first that MXϕ, i.e. MX∃~w1. . . ∃~wnδ0. Thus there exist F1:X→ P∗(Mk) F2:X[F1/~w1]→ P∗(Mk) . . . Fn:X[F1/~w1,...,Fn−1/~wn−1]→ P∗(Mk) s.t. MX0δ0,where X0:= X[F1/~w1,...,Fn/~wn]. Let M0:= M[X0(~w1)/P1, . . . , X0(~wn)/Pn, X0(~y1)/R1, . . . , X0(~ym)/Rm]. Now by Claim 4, we have M0X0δ. Because X0Fr(δ) = {∅}, by locality M0δ. Since X0(~yi)=X(~yi)for each i≤m, we have M[X(~y1)/R1, . . . , X(~ym)/Rm]Φ. Suppose then that M[X(~y1)/R1, . . . , X(~ym)/Rm]Φ. Thus, by the equation (4), there are nonempty sets A1, . . . , An⊆Mksuch that M0δ, where M0:= M[A1/P1, . . . , An/Pn, X(~y1)/R1, . . . , X(~ym)/Rm]. Since, by the assumptions, X6=∅and Vr(~y1. . . ~ym)⊆dom(X), we have X(~yi)6=∅for each i≤m. We define the function Fifor each i≤nby Fi:X[F1/~w1,...,Fi−1/~wi−1]→ P∗(Mk), s 7→ Ai. Let X0:= X[F1/~w1,...,Fn/~wn], whence X0=X[A1/~w1, . . . , An/~wn]. Since XFr(δ) = {∅}, the condition (?) in Claim 5 holds for the team Xwith respect to Fr(δ). We also have M0XFr(δ)δand thus by Claim 5 we obtain MX0δ0. Hence MX∃~w1. . . ∃~wnδ0, i.e. MXϕ. Remark. By Theorem 4.5, for each ESOL[k]-formula Φ(R), for which Ris at most k-ary, there exists an INEXL[k]-formula ϕ(~y )such that for all X6=∅: MXϕiff M[X(~y )/R]Φ. Without the requirement of non-empty teams and the arity restriction on R, this would be the converse of Theorem 4.3. But due empty team property of INEX, the left side of the equivalence is always true for the empty team and any formula of INEX. Thus, when defining classes of relations with INEX, we can only define such classes that include the empty relation. The arity restriction is also necessary since it can be shown that for any kthere are ESO[k]-definable properties of (k+1)-ary relations X(~y )that cannot be defined in INEX[k]. A proof for this claim will be presented in a future work by the author. Since Theorem 4.3 and Theorem 4.5 can also be proven for INEXL[k]- and ESOL[k]-sentences, we obtain the following corollary. 38 Corollary 4.6. On the level of sentences INEX[k]captures the expressive power of ESO[k]. In particular, INEX[1] captures EMSO. As a direct corollary we also obtain a strict arity hierarchy for INEX, since the arity hierarchy for ESO (with arbitrary vocabulary) is strict, as shown by Ajtai [1] in 1983. As mentioned in the introduction, k-ary dependence and independence logics capture the fragment of ESO where at most (k−1)-ary functions can be quantified. This fragment differs from ESO[k] at least when kis one or two – and presumably for any k. Hence it appears that INEX[k] does not correspond to l-ary independence logic for any kand l, even though without arity bounds these two logics are equivalent. On the duality of inclusion and exclusion atoms For the last topic in this section, we will discuss the relationship of inclusion and exclusion atoms. We will also consider natural candidates for the semantics of negated inclusion and exclusion atoms. In our translation in Theorem 4.5 we used inclusion and exclusion atoms in a dualistic way by replacing atomic formulas P~ twith inclusion atoms and negated atomic formulas ¬P~ t with exclusion atoms. This correspondence becomes more obvious when we reformulate the truth conditions for P~ tand ¬P~ t(compare with Definition 2.1) as follows: MXP~ tiff X(~ t)⊆PMand MX¬P~ tiff X(~ t)⊆PM. The truth conditions for inclusion and exclusion atoms can be written in a form that is very similar to the equivalences above: MX~ t1⊆~ t2iff X(~ t1)⊆X(~ t2)and MX~ t1|~ t2iff X(~ t1)⊆X(~ t2). As we argued earlier (Observation 2.1), the semantics of a contradictory negation (MX¬ϕiff M2Xϕ) is not a very natural choice of semantics for the negated atoms. Instead, it would be more natural to have such a semantics that is similar to the semantics of literals. From this viewpoint, a natural candidate for a semantics of a negated inclusion atom would be the following: MX¬(~ t1⊆~ t2)iff X(~ t1)⊆X(~ t2).(¬ ⊆) Then we would have ¬(~ t1⊆~ t2)≡~ t1|~ t2. Therefore, if we allow the use of negated atoms in INC[k]with our semantics, the resulting logic is equivalent with INEX[k]. Note that since the exclusion relation is symmetric, our choice of semantics leads to the following equivalence: ¬(~ t1⊆~ t2)≡~ t1|~ t2≡~ t2|~ t1≡ ¬(~ t2⊆~ t1). 39 Hence, by this definition, ¬(~ t1⊆~ t2)≡ ¬(~ t2⊆~ t1)even though ~ t1⊆~ t26≡ ~ t2⊆~ t1. This kind of property of a negated atom might be a bit exotic, but not unthinkable, since our negation is not a contradictory negation. Let us then consider semantics for the negated exclusion atom ¬(~ t1|~ t2). Semantics of the inclusion atom ~ t1⊆~ t2is not a possible choice here, since by the symmetry of the exclusion relation, we must have ¬(~ t1|~ t2)≡ ¬(~ t2|~ t1). The truth condition MX~ t1|~ t2iff X(~ t1)∩X(~ t2) = ∅, naturally gives us the following candidate for a semantics. MX¬(~ t1|~ t2)iff X(~ t1) = X(~ t2)(¬ | ) Now we have ¬(~ t1|~ t2)≡ ¬(~ t2|~ t1), as required, and ¬(~ t1|~ t2)≡~ t1⊆~ t2∧~ t2⊆~ t1. This choice of semantics is actually equivalent with the semantics of equiextension atom ~ t1./ ~ t2that was introduced by Galliani in [4]. This atom has been shown equivalent with the inclusion atom ~ t1⊆~ t2of the same arity ([4]). Hence if we allow the use of negated atoms in EXC[k]with our semantics, the resulting logic turns out be equivalent with INEX[k]. With our choices for semantics of negated inclusion and exclusion atoms, (¬ ⊆) and (¬ | ), we have ¬(~ t1⊆~ t2)≡~ t1|~ t2and ¬(~ t1|~ t2)≡~ t1./ ~ t2. Now the exclusion atom is equivalent with the negated inclusion atom, but not vice versa. However, the negated exclusion atom is equally expressive as the inclusion atom of the corresponding arity. Hence even though inclusion and exclusion atoms are not exactly negations of each other, they nevertheless have a dualistic relationship. We could extend FO with either of these atoms and allow the use of its negation to obtain a logic equivalent to INEX. In team semantics we must require all formulas to be in negation normal form. This can be seen as one of the weaknesses of this framework since the free use of negation is natural for a logic. Dependence logic and other related logics have also been criticized for not having sensible semantics for negated atoms8. However, there has not been much research on these issues. In order to solve these problems, Kuusisto [16] has presented an alternative framework called double team semantics. In this approach there are always two teams – a “verifying team” and a “falsifying team”. This allows to use negations freely, whence it just swaps the roles of these two teams. This approach has received relatively little attention, but we believe that it should be studied further in order to understand the role of negation in team semantics more deeply. 8Originally, in [18], negations were allowed to appear in front of dependence atoms. But the semantics for negated dependence atom was defined such that it was true only in the empty team. This way both empty team property and downwards closure were preserved. 40 5. Examples of some INEX-definable properties In this section we present several examples on the expressibility of inclusionexclusion logic. Within these examples we also utilize several of the new operators we introduced in Section 3. Although all of the properties expressed here are known to be expressible in INEX by the results of the previous section, we believe that these examples are valuable for demonstrating the nature of inclusion-exclusion logic and team semantics in general. By Corollary 4.6 we know that, in particular, all EMSO-definable properties of models can be expressed by using only unary inclusion and exclusion atoms. In the next example we show how two classical EMSO-definable properties of graphs can be defined in INEX[1]. Example 5.1. Let G= (V, E)be an undirected graph. Then we have (a) Gis disconnected if and only if G∃x1∃x2x1|x2∧ ∀ z(z⊆x1∨z⊆x2)∧(∀y1⊆x1)(∀y2⊆x2)¬Ey1y2. (b) Gis k-colorable if and only if Gγ≤k∨ ∃ x1. . . ∃xk^ i6=j xi|xj∧ ∀ z_ i≤k z⊆xi ∧^ i≤k (∀y1⊆xi)(∀y2⊆xi)¬Ey1y2, where γ≤k:= ∃x1. . . ∃xk∀y(Wi≤ky=xi). We explain briefly why these equivalences hold: In (a) we first quantify two nonempty sets for the values of x1and x2. We use exclusion atom to guarantee that these sets are disjoint. The formula ∀z(z⊆x1∨z⊆x2)checks that the union of these sets covers the whole set of vertices (recall Example 2.1). Finally we use universal inclusion quantifiers to confirm that for any pair of elements chosen within these sets, there is no edge between them. In (b) we first check if |V| ≤ k, in which case the graph would be trivially kcolorable. If that is not the case, we can quantify knonempty disjoint sets which represent the coloring of the graph. Confirming that these sets are disjoint and cover all the vertices can be done similarly as in (a). Finally we confirm that the coloring is correct by choosing any pair of vertices within an unicolored set and checking that there is no edge between them. The properties in Example 5.1 could also be expressed in EMSO and then we could directly use our translation in Theorem 4.5 to express these properties in INEX[1]. This method would give us sentences that are only slightly longer 41 F:X1∪X∗ 2→ P∗(M),       s7→ F1(s)if s∈X1\X∗ 2 s7→ F∗ 2(s)if s∈X∗ 2\X1 s7→ F1(s)∪F∗ 2(s)if s∈X1∩X∗ 2. By the definitions of F∗ 2and F, we have X1[F1/x]∪(X2[F2/x])∗=X1[F1/x]∪X∗ 2[F∗ 2/x]=(X1∪X∗ 2)[F/x]. Hence MX1∪X∗ 2∃x ψ0, i.e. MX1∪X∗ 2(∃x ψ)0. •Let µ=∀x ψ. Suppose MX1(∀x ψ)0and MX2(∀x ψ)0 i. Thus MX1∀x ψ0 and MX2∃x ψ0 i∧∀ x ψ0. Since MX2∀x ψ0, by locality MX∗ 2∀x ψ0. Thus by flatness MX1∪X∗ 2∀x ψ0, i.e. MX1∪X∗ 2(∀x ψ)0. Now we are finally ready to prove Claim 3: MXµiff there exist A1, . . . , An⊆Mks.t. M0Xµ0, and for any i≤nand ~a ∈Aithere is s∈Xs.t. M0{s[~a/~u ]}µ0 i, where M0:= M[~ A/~ P]. Proof. We first examine the special case when X=∅: For the other direction of the equivalence, suppose that MXµ. Let Ai:= ∅for each i≤nand let M0:= M[~ A/~ P]. Because X=∅, we have M0Xµ0, and since Ai=∅for each i≤n, the rest of the right side of the equivalence holds trivially. The other direction is clear since M∅µholds always. We may thus assume that X6=∅. •If µis a literal, the claim holds trivially (we can choose Ai:= ∅for each i≤nwhen proving the other direction of the equivalence). •Let µ= (~ t1⊆~ t2)jfor some j≤n. Suppose first that MX~ t1⊆~ t2. Let M0:= M[~ A/~ P],where Ai:=    X(~ t1)if i=j ∅else. Since X(~ t1) = Aj=PM0 j, we have M0XPj~ t1, i.e. M0X(~ t1⊆~ t2)0. Let i∈ {1, . . . , n} \ {j}and let ~a ∈Ai. Since M0XPj~ t1we can choose any s∈X(6=∅), and then by flatness M0{s}Pj~ t1. By locality we have M0{s[~a/~u ]}Pj~ t1, i.e. M0{s[~a/~u ]}(~ t1⊆~ t2)0 i. Let then i=jand ~a ∈A0 j. Because ~a ∈X(~ t1), there is s∈Xs.t. s(~ t1) = ~a. Since MX~ t1⊆~ t2, there is s0∈Xs.t. s0(~ t2) = s(~ t1). Now s0(~ t2) = ~a, and thus s0[~a/~u ](~u) = s0[~a/~u ](~ t2), i.e. M0{s0[~a/~u ]}~u =~ t2. Since M0XPj~ t1, by locality and flatness M0{s0[~a/~u ]}Pj~ t1. Thus M0{s0[~a/~u ]}~u =~ t2∧Pj~ t1, i.e. M0{s0[~a/~u ]}(~ t1⊆~ t2)0 i. 48 Suppose then that there exist A1, . . . , An⊆Mks.t. M0X(~ t1⊆~ t2)0, and for each i≤nand ~a ∈Aithere exists s∈Xs.t. M0{s[~a/~u ]}(~ t1⊆~ t2)0 i. For the sake of proving that MX~ t1⊆~ t2, let s∈X. Since M0XPj~ t1, by flatness we have M0{s}Pj~ t1. Now s(~ t1)∈PM0 j=Ajand thus there is s0∈X such that M0{s0[s( ~ t1)/~u ]}~u =~ t2∧Pj~ t1. In particular, M0{s0[s( ~ t1)/~u ]}~u =~ t2, and thus we have s(~ t1) = s0[s(~ t1)/~u ](~u) = s0[s(~ t1)/~u ](~ t2) = s0(~ t2). •Let µ=ψ∧θ. Suppose first that MXψ∧θ. Hence MXψand MXθ. By the inductive hypothesis there are B1, . . . , Bn⊆Mks.t. M[~ B/ ~ P]Xψ0 and there are B0 1, . . . , B0 n⊆Mks.t. M[~ B0/~ P]Xθ0. Moreover, for all i≤n and tuples ~a ∈Biand ~a0∈B0 ithere are s, s0∈Xs.t. M[~ B/ ~ P]{s[~a/~u ]}ψ0 i and M[~ B0/~ P]{s0[~a0/~u ]}θ0 i. Let M0:= M[~ A/~ P],where Ai:=    Biif Pioccurs in ψ0 B0 iif Pidoes not occur in ψ0. Because none of Pican occur in both ψ0and θ0, we clearly have M0Xψ0 and M0Xθ0. Hence M0Xψ0∧θ0, i.e. M0X(ψ∧θ)0. Let i≤nand let ~a ∈Ai. Suppose first that Pioccurs in ψ0. Now ~a ∈Bi, and thus there is s∈Xs.t. M[~ B/ ~ P]{s[~a/~u ]}ψ0 i. Relation variables not occurring in ψ0do not occur in ψ0 ieither, and thus M0{s[~a/~u ]}ψ0 i. Because (~ t1⊆~ t2)i does not occur in θand M0Xθ0, by Claim I we have M0{s[~a/~u ]}θ0 i. Thus M0{s[~a/~u ]}ψ0 i∧θ0 i, i.e. M0{s[~a/~u ]}(ψ∧θ)0 i. The case when Pioccurs in θ0 is analogous. Finally suppose that Pidoes not occur in ψ0nor θ0, whence (~ t1⊆~ t2)idoes not occur in ψ∧θ. Since M0X(ψ∧θ)0, we can choose any s∈X(6=∅), and then by Claim I we have M0{s[~a/~u ]}(ψ∧θ)0 i. Suppose then that there are A1, . . . , An⊆Mks.t. M0X(ψ∧θ)0, and for every i≤nand ~a ∈Aithere exists s∈Xs.t. M0{s[~a/~u ]}(ψ∧θ)0 i. Now we have M0Xψ0∧θ0, i.e. M0Xψ0and M0Xθ0. Because (ψ∧θ)0 i=ψ0 i∧θ0 i, for every i≤nand ~a ∈Aithere exists s∈Xsuch that M0{s[~a/~u ]}ψ0 i. Since also M0Xψ0, by the inductive hypothesis MXψ. Analogously we have MXθ, and thus MXψ∧θ. •Let µ=ψ∨θ. Suppose first that MXψ∨θ. Thus there are Y, Y 0⊆X s.t. Y∪Y0=X,MYψand MY0θ. By the inductive hypothesis there are B1, . . . , Bn, B0 1, . . . , B0 n⊆Mks.t. M[~ B/ ~ P]Yψ0and M[~ B0/~ P]Y0θ0. In addition, for every i≤n,~a ∈Biand ~a0∈B0 ithere exist s∈Yand s0∈Y0 s.t. M[~ B/ ~ P]{s[~a/~u ]}ψ0 iand M[~ B0/~ P]{s0[~a0/~u ]}θ0 i. Let M0:= M[~ A/~ P],where Ai:=    Biif Pioccurs in ψ0 B0 iif Pidoes not occur in ψ0. 49 Because none of Pican occur in both ψ0and θ0, we clearly have M0Yψ0 and M0Y0θ0. Therefore M0Xψ0∨θ0, i.e. M0X(ψ∨θ)0. Let i≤nand ~a ∈Ai. Suppose first that Pioccurs in ψ0. Now Ai=Bi, and thus, by the inductive hypothesis, there is s∈Y(⊆X)such that M[~ B/ ~ P]{s[~a/~u ]}ψ0 i. Relation variables not occurring in ψ0do not occur in ψ0 ieither, and thus M0{s[~a/~u ]}ψ0 i, i.e. M0{s[~a/~u ]}(ψ∨θ)0 i. The case when Pioccurs in θ0is analogous. Suppose then that Pidoes not occur in ψ0nor θ0, whence (~ t1⊆~ t2)idoes not occur in ψ∨θ. Since M0X(ψ∨θ)0, we can choose any s∈X(6=∅), and then by Claim I we have M0{s[~a/~u ]}(ψ∨θ)0 i. Suppose then that there are A1, . . . , An⊆Mks.t. M0X(ψ∨θ)0, and for all i≤nand ~a ∈Aithere is si,~a ∈Xs.t. M0{si,~a[~a/~u ]}(ψ∨θ)0 i. Since M0Xψ0∨θ0, there are Y, Y 0⊆Xs.t. Y∪Y0=X,M0Yψ0and M0Y0θ0. We define the teams Yiand Y0 i, for every i≤n, and the teams Z, Z0⊆X: Yi:= {si,~a[~a/~u ]|~a ∈Ai}if (~ t1⊆~ t2)ioccurs in ψ, and else Yi:= ∅. Y0 i:= {si,~a[~a/~u ]|~a ∈Ai}if (~ t1⊆~ t2)ioccurs in θ, and else Y0 i:= ∅. Z:= Y∪([ i≤n Yidom(X)), Z0:= Y0∪([ i≤n Y0 idom(X)). We then show that for every i≤nit holds that M0Yiψ0 i. Let i≤n. If (~ t1⊆~ t2)idoes not occur in ψ, then Yi=∅whence trivially M0Yiψ0 i. Suppose then that (~ t1⊆~ t2)ioccurs in ψ. Now (ψ∨θ)0 i=ψ0 iand thus M0{r}ψ0 ifor every r∈Yi. By flatness we thus have M0Yiψ0 i. Since M0Yψ0and M0Yiψ0 ifor every i≤n, we can apply Claim II for each i≤nto obtain M0Zψ0. By a symmetric argumentation M0Z0θ0. We then show that MZψ. We may suppose that Z6=∅, since else trivially MZψ. Let i≤nand let ~a ∈Ai. Suppose first that (~ t1⊆~ t2)ioccurs in ψ. Now (ψ∨θ)0 i=ψ0 iand thus there is si,~a ∈Xs.t. M0{si,~a[~a/~u ]}ψ0 i. By the definition of Yiwe must have si,~a[~a/~u ]∈Yiand moreover si,~a ∈Z. Suppose then that (~ t1⊆~ t2)idoes not occur in ψ. Then we can choose any assignment s∈Z(6=∅), whence by Claim I we have M0{s[~a/~u ]}ψ0 i. Hence, by the inductive hypothesis, MZψ. We can analogously deduce MZ0θ. Since Z∪Z0=X, we have MXψ∨θ. •Let µ=∃x ψ. Suppose first that MX∃x ψ, i.e. there is F:X→ P∗(M), s.t. MX[F/x]ψ. By the inductive hypothesis there are A1, . . . , An⊆Mks.t. M0X[F/x]ψ0, where M0:=M[~ A/~ P]. Moreover, for all i≤nand ~a∈Aithere is r∈X[F/x]s.t. M0{r[~a/~u ]}ψ0 i. Since M0X[F/x]ψ0, we have M0X∃x ψ0, i.e. M0X(∃x ψ)0. Let i≤nand let ~a ∈Ai. Now there is r∈X[F/x]s.t. M0{r[~a/~u ]}ψ0 i. Since r∈X[F/x], there is s∈Xand b∈F(s)s.t. r=s[b/x]. Let F0: 50 {s[~a/~u ]} → P∗(M)s.t. s[~a/~u ]7→ {b}. Since {s[~a/~u ]}[F0/x] = {r[~a/~u ]}, we have M0{s[~a/~u ]}∃x ψ0 i, i.e. M0{s[~a/~u ]}(∃x ψ)0 i. Suppose then that there are A1, . . . , An⊆Mks.t. M0X(∃x ψ)0, and for every i≤nand ~a ∈Aithere is si,~a ∈Xs.t. M0{si,~a[~a/~u ]}(∃x ψ)0 i. Now there is F:X→ P∗(M)s.t. MX[F/x]ψ0. Furthermore, for each i≤nand ~a ∈Aithere is Fi,~a :{si,~a[~a/~u ]} → P∗(M)s.t. M0{si,~a[~a/~u ]}[Fi,~a/x]ψ0 i. For each i≤nlet X0 i:= [ ~a∈Ai {si,~a[~a/~u ]}[Fi,~a/x]. By flatness M0X0 iψ0 ifor each i≤n. Let F0:X→ P∗(M)s.t. s7→ F(s)∪ {b∈Fi,~a(si,~a[~a/~u ]) |i≤n, ~a ∈Ais.t. s=si,~a}. By the definitions of F0and X0 i(i≤n) we have X[F/x]∪[ i≤n X0 idom(X[F/x])=X[F0/x]. Thus by applying Claim II for each i≤n, we obtain M0X[F0/x]ψ0. Moreover, now for each i≤nand ~a ∈Aithere is r∈X[F0/x]s.t. M0{r[~a/~u ]}ψ0 i. Thus, by the inductive hypothesis, MX[F0/x]ψ, i.e. MX∃x ψ. •Let µ=∀x ψ. Suppose first that MX∀x ψ, i.e. MX[M/x]ψ. By the inductive hypothesis there are A1, . . . , An⊆Mks.t. M0X[M/x]ψ0. Moreover, for each i≤nand ~a ∈Aithere exists r∈X[M/x]s.t. M0{r[~a/~u ]}ψ0 i. Now M0X∀x ψ0, i.e. M0X(∀x ψ)0. Let i≤nand let ~a ∈Ai. Now there is r∈X[M/x]s.t. M0{r[~a/~u ]}ψ0 i. Since r∈X[M/x], there is s∈Xand b∈Ms.t. r=s[b/x]. Let F:{s[~a/~u ]} → P∗(M)s.t. s[~a/~u ]7→ {b}. Now {s[~a/~u ]}[F/x] = {r[~a/~u ]}, and therefore M0{s[~a/~u ]}∃x ψ0 i. Since M0X∀x ψ0, by flatness and locality we have M0{s[~a/~u ]}∀x ψ0. Hence M0{s[~a/~u ]}∃x ψ0 i∧ ∀ x ψ0, i.e. M0{s[~a/~u ]}(∀x ψ)0 i. Suppose then that there are A1, . . . , An⊆Mks.t. M0X(∀x ψ)0, and that for each i≤nand ~a ∈Aithere is s∈Xs.t. M0{s[~a/~u ]}(∀x ψ)0 i. Now we have M0X∀x ψ0, i.e. M0X[M/x]ψ0. Let i≤nand let ~a ∈Ai. Now there is s∈Xs.t. M0{s[~a/~u ]}∃x ψ0 i∧ ∀x ψ0and thus there is F:{s[~a/~u ]}→P∗(M)s.t. M0{s[~a/~u ]}[F/x]ψ0 i. Let b∈F(s[~a/~u]) and let r:= s[b/x], whence r∈X[M/x]and r[~a/~u]∈ {s[~a/~u ]}[F/x]. Now by flatness M0{r[~a/~u]}ψ0 i. Therefore, by the inductive hypothesis, MX[M/x]ψ, i.e. MX∀x ψ. 51