May 30, 2026
We define a new Ehrenfeucht–Fraïssé game for dependence logic. The previously known rendition of such a game was based on moves that are teams. Since teams can be massive, making team moves may be quite complicated. To remedy this, our new Ehrenfeucht–Fraïssé game for dependence logic has only moves that consist of single elements, as in the classical Ehrenfeucht–Fraïssé game of first order logic. A new feature of the game is that a player can declare that their move is made on the basis of certain previous moves only and thereby in a sense independent of other moves. We show that our game characterizes elementary equivalence in dependence logic.
The Ehrenfeucht–Fraïssé game [1] is a fundamental tool of first order logic. We define the corresponding game for dependence logic [2]—an extension of first order logic by dependence atoms \(\mathop{=}(x,y)\), with the intuitive meaning “\(y\) is completely determined by \(x\)"—and show that the game characterizes elementary equivalence in this logic.
Previously, versions of the Ehrenfeucht–Fraïssé game have been defined for a variety of extensions and fragments of first order logic, in particular infinitary logics ([3], [4], [5]), second order logic ([6]), logics with generalized quantifiers ([7], [8], [9], [10], [11]) and logics with a fixed finite number of variables ([12], [13], [14]). Moreover, one version of the Ehrenfeucht–Fraïssé game for the very dependence logic that is our subject in this paper was already defined in [2]. However, that game was “second order" in the sense that moves were sets of assignments, or teams, as they are called. Similarly, there is a”second-order" game for inclusion logic [15], as well as one for inquisitive logic [16]. Our new game is “first order" in the sense that moves are elements as in the original Ehrenfeucht–Fraïssé game of [1]. We show that our game captures dependence logic in the same way as the original Ehrenfeucht–Fraïssé game captures first order logic.
The ordinary Ehrenfeucht–Fraïssé game is a tool for comparing two models. The game is a perfect-information zero-sum game with two players, \(\mathrm{\mathbf{I}}\) and \(\mathrm{\mathbf{II}}\). Winning strategies of player \(\mathrm{\mathbf{II}}\) are witnesses to levels of similarity (or isomorphism) of the models, manifested by elementary equivalence up to a quantifier rank. Winning strategies of player \(\mathrm{\mathbf{I}}\) are witnesses to a difference between the models, manifested by a first-order sentence which is true in one model but not in the other. It is possible to think of the game as a syntax-free approach to comparing the models. We can use the game to express inability to separate the models with a first-order sentence of a certain size. Equivalently, we can use the game to say that one of the models has a first-order property that the other model does not have. In this analysis, the concept of “first order” can be varied by modifying the game.
In using the Ehrenfeucht–Fraïssé game approach for the logical analysis of dependence, something we aim to do in this paper, we have two models and we want to analyze whether they have the same dependence-type properties. For example, there may be a definable binary relation which in one model contains a one-one function but in the other model perhaps not. Or there may be two definable unary relations \(P\) and \(Q\) such that in one model \(|P|\le |Q|\) and in the other model perhaps \(|P|>|Q|\). Or there may be a definable linear order which is a well-order in one model but perhaps not in the other. Or there may be a definable graph relation which is 3-colourable in one model but perhaps not in the other. How does the Ehrenfeucht–Fraïssé game capture such differences?
A possible solution is to use a second order Ehrenfeucht–Fraïssé game in which the players play relations rather than elements, or teams as in [2]. An interesting case is the game for the Henkin (i.e. partially ordered) quantifier, where moves involve choosing a function which is then thrown away [8]. So positions in that game are first order even if moves are second order. This is relevant from the point of view of dependence logic because sentences of the latter have the same expressive power as sentences which start with a partially ordered quantifier prefix followed by a first order formula. However, in this paper we want to stay on the first-order level and focus on an Ehrenfeucht–Fraïssé game in which the moves are elements of the models, not teams or functions. Admittedly, it is not absolutely clear that there is a real difference, as we impose second order conditions on winning strategies.
One important feature of dependence logic that comes to play a role is the lack of negation, except in front of first-order atomic formulas. Therefore, we aim at defining a variant of the Ehrenfeucht–Fraïssé game for \(\mathfrak{A}\) and \(\mathfrak{B}\) such that if player \(\mathrm{\mathbf{II}}\) has a winning strategy, then \(\mathfrak{A}\models\phi\) implies \(\mathfrak{B}\models\phi\) for all dependence logic sentences \(\phi\). By stating the same also in converse order, i.e. existence of a winning strategy for \(\mathrm{\mathbf{II}}\) in the game for \(\mathfrak{B}\) and \(\mathfrak{A}\), we obtain a criterion for elementary equivalence in the usual sense.
Let us consider, as an example, two graphs \(\mathfrak{A}\) and \(\mathfrak{B}\). Let us assume that \(\mathfrak{A}\) is 2-colourable but \(\mathfrak{B}\) is not. We assume the possibility to refer to two colours in both graphs and the question is whether the vertices can be coloured with these colours in a way that is required by the concept of 2-colouring.3 Thus \(\mathfrak{A}\) has the dependence-type property that we can assign one of two colours to each vertex in such a way that neighboring vertices get different colour. How would player \(\mathrm{\mathbf{I}}\) take advantage of this colouring \(f\) in \(\mathfrak{A}\) and the lack of any 2-colouring in \(\mathfrak{B}\)? An obvious idea is the following:
\(\mathrm{\mathbf{I}}\) picks \(x_0\) in \(\mathfrak{B}\) asking \(\mathrm{\mathbf{II}}\) to give its colour.
\(\mathrm{\mathbf{II}}\) retaliates by picking \(y_0\) in \(\mathfrak{A}\) and asking \(\mathrm{\mathbf{I}}\) to give first its colour.
\(\mathrm{\mathbf{I}}\) gives a colour \(x_1\) for \(y_0\), making the commitment that he chose the colour on the basis of knowing \(y_0\) only.
Now \(\mathrm{\mathbf{II}}\) gives some colour \(y_1\) for \(x_0\), making the commitment that she chose the colour on the basis of knowing \(x_0\) only.
\(\mathrm{\mathbf{I}}\) picks again some \(x_2\) in \(\mathfrak{B}\) asking again \(\mathrm{\mathbf{II}}\) to give its colour.
\(\mathrm{\mathbf{II}}\) again retaliates by picking \(y_2\) in \(\mathfrak{A}\) and asking \(\mathrm{\mathbf{I}}\) to give its colour.
\(\mathrm{\mathbf{I}}\) gives a colour \(x_3\) for \(y_2\), claiming that he chose the colour on the basis of knowing \(y_2\) only.
\(\mathrm{\mathbf{II}}\) gives some colour \(y_3\) for \(x_2\), claiming that she chose the colour on the basis of knowing \(x_2\) only.
Now \(\mathrm{\mathbf{II}}\) has won if
\(x_0=x_2\implies y_0=y_2\),
\(x_0Ex_2\implies y_0Ey_2\), and
\(x_1\ne x_3 \implies y_1\ne y_3\).
A pair \(\{s_0,s_1\}\) of plays of the above game is said to be \(\mathrm{\mathbf{I}}\)-good if it satisfies \(\mathop{=}(y_0,x_1)\wedge\mathop{=}(y_2,x_3)\) and \(\mathrm{\mathbf{II}}\)-good if it satisfies \(\mathop{=}(x_0,y_1)\wedge\mathop{=}(x_2,y_3)\). A strategy \(\tau\) of \(\mathrm{\mathbf{II}}\) is called a uniform winning strategy if every \(\mathrm{\mathbf{I}}\)-good pair of plays in which \(\mathrm{\mathbf{II}}\) has used the strategy \(\tau\) is \(\mathrm{\mathbf{II}}\)-good and satisfies condition [item:32winning32condition] above.
We show that \(\mathrm{\mathbf{II}}\) cannot have a uniform winning strategy in this game, assuming the players honour their commitments. Suppose she has and let us call it \(\tau\). Let us play so that \(\mathrm{\mathbf{I}}\) plays \(x_0=x_2\) but otherwise \(x_0\) is arbitrarily. Then she plays some \(y_1\). Let us denote this \(y_1=g(x_0)\). The function \(g\) cannot be a 2-colouring of \(\mathfrak{B}\) because \(\mathfrak{B}\) is not 2-colourable. Thus there are \(b_0\) and \(b_1\) in \(\mathfrak{B}\) such that \(b_0E^\mathfrak{B}b_1\) but \(g(b_0)=g(b_1)\). Let us consider two plays \(s_0\) and \(s_1\) (see Table 1):
| \(s_0\) | \(s_1\) | ||
|---|---|---|---|
| \(\mathrm{\mathbf{I}}\) | \(x_0\) | \(b_0\) | \(b_1\) |
| \(\mathrm{\mathbf{II}}\) | \(y_0=\tau(x_0)\) | \(a_0\) | \(a_0'\) |
| \(\mathrm{\mathbf{I}}\) | \(x_1\) | \(f(a_0)\) | \(f(a_0')\) |
| \(\mathrm{\mathbf{II}}\) | \(y_1\) | \(g(b_0)\) | \(g(b_1)\) |
| \(\mathrm{\mathbf{I}}\) | \(x_2\) | \(b_0\) | \(b_0\) |
| \(\mathrm{\mathbf{II}}\) | \(y_2\) | \(a_1\) | \(a_1'\) |
| \(\mathrm{\mathbf{I}}\) | \(x_3\) | \(f(a_1)\) | \(f(a_1')\) |
| \(\mathrm{\mathbf{II}}\) | \(y_3\) | \(d_1\) | \(d_1'\) |
The pair \(s_0,s_1\) is \(\mathrm{\mathbf{I}}\)-good since \(\mathrm{\mathbf{I}}\) is using the 2-colouring \(f\) in \(A\). Since \(\mathrm{\mathbf{II}}\) is using \(\tau\), the pair is also \(\mathrm{\mathbf{II}}\)-good. Hence \(d_1=d'_1\). By condition [item:32winning32condition] applied to \(s_0\), we have \(g(b_0)=d_1\). Condition [item:32winning32condition] applied to \(s_1\) yields \(a_0'E^\mathfrak{B}a_1'\), whence \(f(a_0')\ne f(a_1')\), and by condition [item:32winning32condition] again, still applied to \(s_1\), \(g(b_1)\ne d_1'\). But \[g(b_1)=g(b_0)=d_1=d_1'.\] This contradiction shows that \(\mathrm{\mathbf{II}}\) cannot have a uniform winning strategy.
The above game is a prototype of the new Ehrenfeucht–Fraïssé game \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) we propose in Section 3, after some preliminaries in Section 2. We also introduce the crucially important concept of a uniform winning strategy of \(\mathrm{\mathbf{II}}\) in \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\). In Section 4, an auxiliary game, a slight modification \(\mathop{\mathrm{EF}}^\mathcal{D}_n((\mathfrak{A},X),(\mathfrak{B},Y))\) of the Ehrenfeucht–Fraïssé game presented in [2], is introduced. It is then shown, in Section 5, that if \(\mathrm{\mathbf{II}}\) has a winning strategy in the auxiliary game \(\mathop{\mathrm{EF}}^\mathcal{D}_n((\mathfrak{A},X),(\mathfrak{B},Y))\), she has a uniform winning strategy in \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\). Section 6 is devoted to the main results of this paper: an equivalence of having a uniform winning strategy in \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) and preservation of truth from \(\mathfrak{A}\) to \(\mathfrak{B}\).
Let \(L\) be a vocabulary. Given an \(L\)-structure \(\mathfrak{A}\) and a set \(D\) of variables, an assignment of \(\mathfrak{A}\) with domain \(D\) is a function \(D\to A\). Given an element \(a\in A\) and an assignment \(s\in A^D\) and a variable \(x\) (not necessarily in \(D\)), we we denote by \(s[a/x]\) the assignment \(s'\) of \(\mathfrak{A}\) with domain \(D\cup\{x\}\), defined by \[s'(y) = \begin{cases} a & \text{if y = x,} \\ s(y) & \text{for y\in D\setminus\{x\}.} \end{cases}\] Given an assignment \(s\) and a tuple \(\vec{x} = (x_0,\dots,x_{n-1})\in\mathop{\mathrm{dom}}(s)^n\) of variables, we write \(s(\vec{x})\) as a shorthand for the tuple \((s(x_0),\dots,s(x_{n-1}))\).
A structure \(\mathfrak{A}\) and an assignment \(s\) of \(\mathfrak{A}\) satisfying a first-order formula \(\phi\), in symbols \(\mathfrak{A}\models_s\phi\), is defined as usual: \(\mathfrak{A}\models_s R(\vec{x})\) if \(s(\vec{x})\in R^\mathfrak{A}\); \(\mathfrak{A}\models_s x = y\) if \(s(x) = s(y)\); \(\mathfrak{A}\models_s\neg\phi\) if \(\mathfrak{A}\not\models_s\phi\); \(\mathfrak{A}\models_s \phi\land\psi\) if \(\mathfrak{A}\models_s\phi\) and \(\mathfrak{A}\models_s\psi\); and \(\mathfrak{A}\models_s\exists x\phi\) if there is \(a\in A\) such that \(\mathfrak{A}\models_{s[a/x]}\phi\). It is obviously required that the free variables of the formula are included in the domain of the assignment.
Next we define what teams are, as well as some operations on them that are used to define the semantics of dependence logic.
Definition 1. Let \(L\) be a vocabulary.
Given an \(L\)-structure \(\mathfrak{A}\) and a set \(D\) of variables, a team of \(\mathfrak{A}\) with domain \(D\) is a set of assignments of \(\mathfrak{A}\) with domain \(D\), i.e. a subset of \(A^D\). The domain of a team \(X\) is denoted by \(\mathop{\mathrm{dom}}(X)\).
Given a structure \(\mathfrak{A}\) and a team \(X\) of \(\mathfrak{A}\), a supplement function for \(X\) and \(\mathfrak{A}\) is a function \(X\to\mathop{\mathrm{\mathcal{P}}}(A)\setminus\{\emptyset\}\). Given a supplement function \(F\) for \(X\) and \(\mathfrak{A}\) and a variable \(x\), we denote by \(X[F/x]\) the team \(Y\) of \(\mathfrak{A}\) with domain \(\mathop{\mathrm{dom}}(X)\cup\{x\}\) defined by \[Y = \{ s[a/x] \mid s\in X, a\in F(s) \}.\] We say that the team has been supplemented by \(F\).
We denote by \(X[A/x]\) the team \(Y\) of \(\mathfrak{A}\) with domain \(\mathop{\mathrm{dom}}(X)\cup\{x\}\) defined by \[Y = \{ s[a/x] \mid a\in A \}.\] We say that the team has been duplicated.
Next we define the syntax and semantics of dependence logic as it is usually presented in the literature. Another (equivalent) variant is introduced in Section 4 and then used for the rest of the paper.
Definition 2. Let \(L\) be a vocabulary.
The syntax of \(L\)-formulas of dependence logic is \[\phi \Coloneqq \alpha \mid \neg\alpha \mid \mathop{=}(\vec{x},y) \mid (\phi\land\phi) \mid (\phi\lor\phi) \mid \exists x\phi \mid \forall x\phi,\] where \(\alpha\) is a first-order atomic \(L\)-formula. We denote dependence logic by \(\mathcal{D}\).
Given an \(L\)-formula \(\phi\in\mathcal{D}\), an \(L\)-structure \(\mathfrak{A}\) and a team \(X\) of \(\mathfrak{A}\) whose domain contains the free variables of \(\phi\), we define \(\mathfrak{A}\models_X\phi\) recursively as follows.
If \(\phi\) is a first-order atomic or negated atomic formula, then \(\mathfrak{A}\models_X\phi\) if \(\mathfrak{A}\models_s\phi\) for all \(s\in X\).4
If \(\phi\) is \(\mathop{=}(x_0,\dots,x_{n-1},y)\), then \(\mathfrak{A}\models_X\phi\) if for all \(s,s'\in X\) such that \(s(x_i) = s'(x_i)\) for all \(i<n\), we have \(s(y) = s'(y)\).
If \(\phi = \psi\land\theta\), then \(\mathfrak{A}\models_X\phi\) if \(\mathfrak{A}\models_X\psi\) and \(\mathfrak{A}\models_X\theta\).
If \(\phi = \psi\lor\theta\), then \(\mathfrak{A}\models_X\phi\) if there are \(Y,Z\subseteq X\) such that \(X = Y\cup Z\), \(\mathfrak{A}\models_Y\psi\) and \(\mathfrak{A}\models_Z\theta\).
If \(\phi = \exists x\psi\), then \(\mathfrak{A}\models_X\phi\) if there is a supplement function \(F\) for \(X\) and \(\mathfrak{A}\) such that \(\mathfrak{A}\models_{X[F/x]}\psi\).
If \(\phi = \forall x\psi\), then \(\mathfrak{A}\models_X\phi\) if \(\mathfrak{A}\models_{X[A/x]}\psi\).
This is the standard team semantics of dependence logic.
The quantifier rank \(\mathop{\mathrm{qr}}(\phi)\) of a formula \(\phi\) is defined recursively by setting \(\mathop{\mathrm{qr}}(\phi) = 0\) for atomic formulas \(\phi\), \(\mathop{\mathrm{qr}}(\phi\land\psi) = \mathop{\mathrm{qr}}(\phi\lor\psi) = \max\{\mathop{\mathrm{qr}}(\phi), \mathop{\mathrm{qr}}(\psi)\}\) and \(\mathop{\mathrm{qr}}(\exists x\phi) = \mathop{\mathrm{qr}}(\forall x\phi) = \mathop{\mathrm{qr}}(\phi)+1\). Note that in [2], the definition is slightly different, as also disjunction increases quantifier rank.
We write \((\mathfrak{A},X)\mathbin{\Rrightarrow}^\mathcal{D}_n(\mathfrak{B},Y)\) if \(\mathop{\mathrm{dom}}(X) = \mathop{\mathrm{dom}}(Y)\) and for all formulas \(\phi\) of dependence logic, with free variables in the domain of \(X\) and \(Y\), and quantifier rank \(\leq n\), we have \[\mathfrak{A}\models_X\phi \implies \mathfrak{B}\models_Y\phi.\] We write \(\mathfrak{A}\mathbin{\Rrightarrow}^\mathcal{D}_n\mathfrak{B}\) if \(\mathfrak{B}\) satisfies all the sentences of quantifier rank \(\leq n\) that \(\mathfrak{A}\) satisfies. If \(\mathfrak{A}\mathbin{\Rrightarrow}^\mathcal{D}_n\mathfrak{B}\) for all \(n<\omega\), we write \(\mathfrak{A}\mathbin{\Rrightarrow}^\mathcal{D}\mathfrak{B}\). Note that \(\mathfrak{A}\mathbin{\Rrightarrow}^\mathcal{D}_n\mathfrak{B}\) if and only if \((\mathfrak{A},X)\mathbin{\Rrightarrow}^\mathcal{D}_n(\mathfrak{B},Y)\), where \(X = Y = \{\emptyset\}\).
Fact 3. Dependence logic is downward closed, meaning that for any \(L\)-formula \(\phi\) of dependence logic, an \(L\)-structure \(\mathfrak{A}\) and a team \(X\) of \(\mathfrak{A}\) whose domain contains the free variables of \(\phi\), if \(\mathfrak{A}\models_X\phi\), then \(\mathfrak{A}\models_Y\phi\) for any \(Y\subseteq X\).
The existential and universal quantifiers do not, at first glance, seem like the semantic duals of each other. However, due to downward closedness, they are, as demonstrated by the following lemma.
Lemma 1. Given a formula \(\phi\) of dependence logic, \(\mathfrak{A}\models_X\forall x\phi\) if and only if \(\mathfrak{A}\models_{X[F/x]}\phi\) for all supplement functions \(F\) of \(X\) and \(\mathfrak{A}\).
Proof. As duplication is a particular kind of supplementation, the direction from right to left is clear. For the other direction, suppose that \(\mathfrak{A}\models_X\forall x\phi\). Then \(\mathfrak{A}\models_{X[A/x]}\phi\). Let \(F\) be any supplement function of \(X\). Note that \(X[F/x]\subseteq X[A/x]\). As dependence logic is downward closed, this means that \(\mathfrak{A}\models_{X[F/x]}\phi\). ◻
We conclude the section with an important normal form for \(\mathcal{D}\).
Theorem 1 ([2]). Every sentence of \(\mathcal{D}\) is equivalent to one of the form \[\forall x_0\dots\forall x_{m-1}\exists y_0\dots\exists y_{n-1}(\psi\land\theta),\] where
\(\theta\) is a quantifier-free first-order formula,
\(\psi = \bigwedge_{i<n}\mathop{=}(\vec{z}_i, y_i)\), and
\(\vec{z}_i \in\{x_j \mid j<m\}^{<\omega}\) for all \(i<n\).
We now give an exact definition of the new EF game that we described in the introduction and which we denote by \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\).
Definition 4. Let \(\mathfrak{A}\) and \(\mathfrak{B}\) be \(L\)-structures with disjoint domains.
We denote the (ordinary) Ehrenfeucht–Fraïssé game of length \(n\) between \(\mathfrak{A}\) and \(\mathfrak{B}\) by \(\mathop{\mathrm{EF}}_n(\mathfrak{A},\mathfrak{B})\). The game has two players, \(\mathrm{\mathbf{I}}\) and \(\mathrm{\mathbf{II}}\), and they take turns picking elements of \(A\cup B\). On round \(i<n\), either
\(\mathrm{\mathbf{I}}\) chooses some \(x_i\in A\) and \(\mathrm{\mathbf{II}}\) responds with \(y_i\in B\), or
\(\mathrm{\mathbf{I}}\) choose some \(x_i\in B\) and \(\mathrm{\mathbf{II}}\) responds with \(y_i\in A\).
Then, let \[a_i = \begin{cases} x_i & \text{if x_i\in A,} \\ y_i & \text{otherwise,} \end{cases} \quad\text{and}\quad b_i = \begin{cases} x_i & \text{if x_i\in B,} \\ y_i & \text{otherwise.} \end{cases}\] \(\mathrm{\mathbf{II}}\) wins a play \[(x_0,y_0,\dots,x_{n-1},y_{n-1})\] if the function \(\{(a_i,b_i) \mid i<n\}\) is a partial isomorphism.
If a player \(P\) has a winning strategy in the game, we write \[P\mathbin{\raisebox{0.8\depth}{\uparrow}}\mathop{\mathrm{EF}}_n(\mathfrak{A},\mathfrak{B}).\]
The game \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) of length \(n\) between \(\mathfrak{A}\) and \(\mathfrak{B}\) is played exactly the same way as \(\mathop{\mathrm{EF}}_n(\mathfrak{A},\mathfrak{B})\), with the following addition: on each round \(k<n\), in addition to playing an element \(x_k\in A\cup B\), \(\mathrm{\mathbf{I}}\) also plays a collection \(\mathcal{W}_k\subseteq\mathop{\mathrm{\mathcal{P}}}(n)\) of sets of indices, as well as two sets \[\mathcal{U}^+_k,\mathcal{U}^-_k \subseteq \{ R(\vec{x}) \mid R\in L\cup\{=\}, \vec{x}\in\{v_0,\dots,v_{n-1}\}^{\mathop{\mathrm{ar}}(R)}, v_k\in\vec{x} \},\] of atomic first-order formulas such that \(\mathcal{U}^+_k\cap\mathcal{U}^-_k = \emptyset\). Player \(\mathrm{\mathbf{II}}\) wins a play \[((x_0,\mathcal{W}_0,\mathcal{U}^+_0,\mathcal{U}^-_k),y_0,\dots,(x_{n-1},\mathcal{W}_{n-1},\mathcal{U}^+_{n-1},\mathcal{U}^-_k),y_{n-1})\] if the relation \(\{ (a_k, b_k) \mid k<n \}\) preserves the atomic formulas of \(\bigcup_{k<n}\mathcal{U}^+_k\) and the negations of the atomic formulas of \(\bigcup_{k<n}\mathcal{U}^-_k\), i.e. for any \(k<n\) and \(\phi(v_0,\dots,v_{n-1})\in\mathcal{U}^+_k\), \[\mathfrak{A}\models\phi(a_0,\dots,a_{n-1}) \implies \mathfrak{B}\models\phi(b_0,\dots,b_{n-1}),\] and for any \(\phi(v_0,\dots,v_{n-1})\in\mathcal{U}^-_k\), \[\mathfrak{A}\models\neg\phi(a_0,\dots,a_{n-1}) \implies \mathfrak{B}\models\neg\phi(b_0,\dots,b_{n-1}).\]
In the above definition, the set \(\mathcal{W}_k\) is the set of dependence commitments made by \(\mathrm{\mathbf{I}}\) on round \(k\). If \(\{i_0,\dots,i_{k-1}\}\in\mathcal{W}_k\), then \(\mathrm{\mathbf{I}}\) has declared that the move \(x_k\) is determined by the moves that were made on rounds \(i_0,\dots,i_{k-1}\) in the same model as \(x_k\), i.e. by \(a_{i_0},\dots,a_{i_{k-1}}\) in the case \(x_k\in A\) and by \(b_{i_0},\dots,b_{i_{k-1}}\) in the case \(x_k\in B\). However, a careful reader may notice that the winning condition for \(\mathrm{\mathbf{II}}\) does not mention these commitments at all. This is by design: in a single play, a declaration of dependence has no meaning5. Only when examining multiple plays at once can we determine whether a dependence occurs. This is done below in Definition 5.
Note that also first-order atomic formulas are treated as commitments of \(\mathrm{\mathbf{I}}\), as illustrated by the sets \(\mathcal{U}^+_k\) (atoms to be preserved) and \(\mathcal{U}^-_k\) (atoms whose negations are to be preserved). This is due to the fact that in the team semantics of first-order logic, a team satisfies an atomic formula if and only if every assignment separately does. Now, if we think of (the element moves of) a single play of the game as a pair \((s,s')\) of assignments—the moves played in \(\mathfrak{A}\) making up \(s\) and the moves played in \(\mathfrak{B}\) making up \(s'\)—then a collection of plays gives rise to a pair of teams. It might be that neither team satisfies, say, \(P(v_0)\), but for different reasons: perhaps one assignment \(s_0\) in \(\mathfrak{A}\) does not satisfy \(P(v_0)\) while its pair \(s'_0\) in \(\mathfrak{B}\) does, and another assignment \(s_1\) satisfies \(P(v_0)\) while its pair \(s'_1\) does not. Therefore, any atomic formulas \(\mathrm{\mathbf{I}}\) has no intention of satisfying in a uniform manner, should not contribute to \(\mathrm{\mathbf{II}}\) losing a play in the sense of dependence logic.
Note also that as equations and their negations only need to be preserved when declared so by \(\mathrm{\mathbf{I}}\), the relation \(\{ (a_k, b_k) \mid k<n \}\) generally need not be a function, let alone an injection, unlike in the classical game \(\mathop{\mathrm{EF}}_n(\mathfrak{A},\mathfrak{B})\).
Next we give an exact definition of what it means for a winning strategy of \(\mathrm{\mathbf{II}}\) to be uniform.
Definition 5.
Let \[p = ((x_0,\mathcal{W}_0,\mathcal{U}^+_0,\mathcal{U}^-_0),y_0,\dots,(x_{n-1},\mathcal{W}_{n-1},\mathcal{U}^+_{n-1},\mathcal{U}^-_{n-1}),y_{n-1})\] and \[p' = ((x'_0,\mathcal{W}'_0,(\mathcal{U}^+_0)',(\mathcal{U}^-_0)'),y'_0,\dots,(x'_{n-1},\mathcal{W}'_{n-1},(\mathcal{U}^+_{n-1})',(\mathcal{U}^-_{n-1})'),y'_{n-1})\] be two plays of \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\). We say that \(\mathrm{\mathbf{I}}\) has played \(p\) and \(p'\) consistently if for all \(k<n\),
\(\mathcal{W}_k = \mathcal{W}'_k\), \(\mathcal{U}^+_k = (\mathcal{U}^+_k)'\) and \(\mathcal{U}^-_k = (\mathcal{U}^-_k)'\),
\(x_k\in A\) if and only if \(x'_k\in A\),
for all atoms \(\phi(v_0,\dots,v_{n-1})\in\bigcup_{k<n}\mathcal{U}^+_k\), \[\mathfrak{A}\models\phi(a_0,\dots,a_{n-1}) \quad\text{and}\quad \mathfrak{A}\models\phi(a'_0,\dots,a'_{n-1}),\]
for all atoms \(\phi(v_0,\dots,v_{n-1})\in\bigcup_{k<n}\mathcal{U}^-_k\), \[\mathfrak{A}\models\neg\phi(a_0,\dots,a_{n-1}) \quad\text{and}\quad \mathfrak{A}\models\neg\phi(a'_0,\dots,a'_{n-1}),\] and
for all \(W\in\mathcal{W}_k\), whenever \(a_i = a'_i\) for all \(i\in W\), also \(a_k = a'_k\).
We say that a strategy \(\tau\) of \(\mathrm{\mathbf{II}}\) in \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) is uniformly winning if it is winning and the following holds: for any two plays \[((x_0,\mathcal{W}_0,\mathcal{U}^+_0,\mathcal{U}^-_0),y_0,\dots,(x_{n-1},\mathcal{W}_{n-1},\mathcal{U}^+_{n-1},\mathcal{U}^-_{n-1}),y_{n-1})\] and \[((x'_0,\mathcal{W}'_0,(\mathcal{U}^+_0)',(\mathcal{U}^-_0)'),y'_0,\dots,(x'_{n-1},\mathcal{W}'_{n-1},(\mathcal{U}^+_{n-1})',(\mathcal{U}^-_{n-1})'),y'_{n-1}),\] where \(\mathrm{\mathbf{II}}\) has used \(\tau\) and \(\mathrm{\mathbf{I}}\) has played consistently, for any \(k<n\) and \(W\in\mathcal{W}_k\), we have \[\text{b_i = b'_i for all i\in W} \implies b_k = b'_k.\] When \(\mathrm{\mathbf{II}}\) has a uniformly winning strategy, we write \[\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}_{\!\textrm u}\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B}).\]
In the above definition, it is enough to consider only pairs of plays instead of larger sets. This reflects the fact that if a dependence atom is not satisfied by a team, then a subteam of two assignments will already falsify the atom. In Section 5, we show that one can also consider larger sets when convenient.
Let us, for a moment, forget the commitments of \(\mathrm{\mathbf{I}}\) in \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) and only consider the element moves. Then, as previously mentioned, a single play \[(x_0,y_0,\dots,x_{n-1},y_{n-1})\] can be thought of as a pair of assignments \[(s,s')\in A^D\times B^D,\] where \(D = \{v_0,\dots,v_{n-1}\}\), such that \(a_i = s(v_i)\) and \(b_i = s'(v_i)\) for all \(i<n\). Furthermore, a set of plays can be seen as a pair of teams \((X,Y)\), where \(X\) consists of the assingments \(s\) and \(Y\) of the assignments \(s'\). In such a pair \((X,Y)\), every assignment \(s\in X\) clearly corresponds to exactly one \(s'\in Y\) and vice versa, so it makes sense to tag each assignment in each team by some index to keep track of the pairings. We now define a notion of a team indexed by a given set to make this formal—and to help us in bookkeeping in later proofs. Giving a team an indexing makes it a multiteam, but team semantics of \(\mathcal{D}\) for indexed teams will have nothing to do with multiteam semantics of [17] but instead collapses back to ordinary team semantics: the truth of “\(\mathfrak{A}\models_X\phi\)” remain the same if one forgets about the indexing of \(X\) altogether.
Finally, we define an auxiliary game \(\mathop{\mathrm{EF}}^\mathcal{D}_n((\mathfrak{A},X),(\mathfrak{B},Y))\) based on indexed teams and show that \((\mathfrak{A},X)\mathbin{\Rrightarrow}^\mathcal{D}_n(\mathfrak{B},Y)\) implies the existence of a winning strategy for \(\mathrm{\mathbf{II}}\).
Definition 6. Let \(L\) be a vocabulary, \(\mathfrak{A}\) an \(L\)-structure, \(D\) a set of variables and \(I\) a set.
An \(I\)-indexed team of \(\mathfrak{A}\) with domain \(D\) is a function \(I\to A^D\).
Let \(\eta\) be a function whose domain is \(I\) and whose values are non-empty sets. A supplement function of type \(\eta\) for \(\mathfrak{A}\) is any function \(F\) such that \(\mathop{\mathrm{dom}}(F) = I\) and \(F(i)\in A^{\eta(i)}\) for all \(i\in I\).
Let \(F\) be a supplement function of type \(\eta\) for \(\mathfrak{A}\). Denote by \(I[\eta]\) the set \[\{ (i,j) \mid i\in I, j\in\eta(i) \}.\] For a variable \(x\) and an \(I\)-indexed team \(X\) of \(\mathfrak{A}\), we define the supplementation \(X[F/x]\) of \(X\) by \(F\) to be the \(I[\eta]\)-indexed team \(Y\) of \(\mathfrak{A}\) defined as \[Y(i,j)(y) = \begin{cases} F(i)(j) & \text{if y = x}, \\ X(i)(y) & \text{otherwise}. \end{cases}\] In other words, \(X[F/x](i,j) = X(i)[F(i)(j)/x]\) for all \((i,j)\in I[\eta]\).
If \(X\) is an \(I\)-indexed team, \(J\subseteq I\) and \(Y\) is a \(J\)-indexed team, then we say that \(Y\) is a subteam of \(X\) if \(X\restriction J = Y\).
Definition 7. Given an \(L\)-structure \(\mathfrak{A}\), an \(I\)-indexed team \(X\) of \(\mathfrak{A}\) and a formula \(\phi\) of dependence logic whose free variables are included in \(\mathop{\mathrm{dom}}(X)\), we define \(\mathfrak{A}\models_X\phi\) recursively as follows.
If \(\phi\) is first-order atomic or negated atomic, then \(\mathfrak{A}\models_X\phi\) if for all \(i\in I\), \(\mathfrak{A}\models_{X(i)}\phi\).
If \(\phi\) is \(\mathop{=}(\vec{x},y)\), then \(\mathfrak{A}\models_X\phi\) if for all \(i,j\in I\), \[X(i)(\vec{x}) = X(j)(\vec{x}) \implies X(i)(y) = X(j)(y).\]
If \(\phi = \psi\land\theta\), then \(\mathfrak{A}\models_X\phi\) if \(\mathfrak{A}\models_X\psi\) and \(\mathfrak{A}\models_X\theta\).
If \(\phi = \psi\lor\theta\), then \(\mathfrak{A}\models_X\phi\) if there are \(J,K\subseteq I\) such that \(J\cup K = I\) and \(\mathfrak{A}\models_{X\restriction J}\psi\) and \(\mathfrak{A}\models_{X\restriction K}\theta\).
If \(\phi = \exists x \psi\), then \(\mathfrak{A}\models_X\phi\) if there is a supplement function \(F\) for \(\mathfrak{A}\) such that \(\mathfrak{A}\models_{X[F/x]}\psi\).
If \(\phi = \forall x\psi\), then \(\mathfrak{A}\models_X\phi\) if \(\mathfrak{A}\models_{X[F/x]}\psi\) for all supplement functions \(F\) for \(\mathfrak{A}\).
Next we prove that the indexing of a team by some set \(I\), possibly making the team a multiset of assignments, does not in any way affect the semantics as we have defined it.
Lemma 2. Given an \(I\)-indexed team \(X\), denote by \(X^*\) the (ordinary) team \[\{ X(i) \mid i\in I \}.\] Then for any formula \(\phi\) of dependence logic, \[\mathfrak{A}\models_X\phi \iff \mathfrak{A}\models_{X^*}\phi.\]
Proof. We proceed by induction on \(\phi\). The case for atomic formulas and connectives is clear, so we only consider the quantifiers. The universal quantifier case is the dual of the existential quantifier case, by Lemma 1. Suppose that \(\phi = \exists x\psi\) and \(\mathfrak{A}\models_X\phi\). Then there is a supplement function \(F\) such that \(\mathfrak{A}\models_{X[F/x]}\psi\). Let \(\eta\) be the type of \(F\). We define an (ordinary) supplement function \(G\) on \(X^*\) by setting \[G(X(i)) = \{ F(i)(j) \mid j\in\eta(i) \}.\] By the induction hypothesis, we have \(\mathfrak{A}\models_{X[F/x]^*}\psi\), so it is enought to show that \(X[F/x]^* = X^*[G/x]\).
First suppose that \(s\in X[F/x]^*\). Then \(s = X[F/x](i,j)\) for some \((i,j)\in I[\eta]\). This means that \(i\in I\) and \(j\in\eta(i)\). Now \(s = X(i)[F(i)(j)/x]\). As \(j\in\eta(i)\), we have \(F(i)(j)\in G(X(i))\), and by definition, \(X(i)\in X^*\), so it follows that \(s\in X^*[G/x]\).
Then suppose that \(s\in X^*[G/x]\). Then \(s = s'[a/x]\) for some \(s'\in X^*\) and \(a\in G(s')\). Now there is some \(i\in I\) such that \(s' = X(i)\). As \(a\in G(X(i))\), there is \(j\in\eta(i)\) such that \(a = F(i)(j)\). Thus \(s = X(i)[F(i)(j)/x] = X[F/x](i,j)\), whence \(s\in X[F/x]^*\).
Conversely, suppose that \(\mathfrak{A}\models_{X^*}\phi\). Then there is a(n ordinary) supplement function \(G\) on \(X^*\) such that \(\mathfrak{A}\models_{X^*[G/x]}\psi\). Let \(\eta\) be the function \[i\mapsto G(X(i)), i\in I.\] Define a supplement function \(F\) of type \(\eta\) by setting \[F(i)(a) = a.\] Again, it is sufficient to show that \(X[F/x]^* = X^*[G/x]\).
First suppose that \(s\in X[F/x]^*\). Then \(s = X[F/x](i,a)\) for some \((i,a)\in I[\eta]\). Now \(s = X(i)[F(i)(a)/x]\). By definition, \(F(i)(a) = a\in G(X(i))\) and \(X(i)\in X^*\), so \(s\in X^*[G/x]\).
Then suppose that \(s\in X^*[G/x]\). Then \(s = s'[a/x]\) for some \(s'\in X^*\) and \(a\in G(s')\). Again, \(s' = X(i)\) and \(a\in G(X(i))\) for some \(i\in I\). As \(a = F(i)(a)\), we have \(s = X(i)[F(i)(a)/x] = X[F/x](i,a)\), and hence \(s\in X[F/x]^*\). ◻
Lemma 3. For any \(I\)-indexed team \(X\) of \(\mathfrak{A}\) and formula \(\phi\) of \(\mathcal{D}\), we have \(\mathfrak{A}\models_X\forall x\phi\) if and only if \(\mathfrak{A}\models_{X[F/x]}\phi\), where \(F\) is any duplicating supplement function, i.e. for each \(i\in I[\eta]\), where \(\eta\) is the type of \(F\), \(F(i)\) lists all elements of \(A\) (possibly with repetition).
Next we define an auxiliary game that we use to prove that \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) captures equivalence in \(\mathcal{D}\). It is an indexed variant of the EF game introduced in [2] for \(\mathcal{D}\), without the disjunction moves. Additionally, positions in the game of [2] are teams, but in the game \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\), moves are supplement functions. This way, moves of the game are the same kind of objects as the ones used to define the semantics of quantifiers, making the game more analogous to the classic EF game.
Definition 8. Let \(\mathfrak{A}\) and \(\mathfrak{B}\) be \(L\)-structures, \(I\) a set, \(D = \{v_k \mid k<\alpha\}\) for some ordinal \(\alpha\), and \(X\) and \(Y\) \(I\)-indexed teams of \(\mathfrak{A}\) and \(\mathfrak{B}\), respectively, with domain \(D\). The game \(\mathop{\mathrm{EF}}^\mathcal{D}_n((\mathfrak{A},X),(\mathfrak{B},Y))\) has two players, \(\mathrm{\mathbf{I}}\) and \(\mathrm{\mathbf{II}}\), and \(n\) rounds. Denote \(I_0 = I\), \(X_0 = X\) and \(Y_0 = Y\). On round \(k\), \(\mathrm{\mathbf{I}}\) chooses a supplement function \(F_k\) for either \(\mathfrak{A}\) or \(\mathfrak{B}\), of some type \(\eta_k\) such that \(\mathop{\mathrm{dom}}(\eta_k) = I_k\). Then \(\mathrm{\mathbf{II}}\) chooses a supplement function \(G_k\) for \(\mathfrak{B}\) if \(F_k\) was for \(\mathfrak{A}\) and for \(\mathfrak{B}\) otherwise, so that the type of \(G_k\) is also \(\eta_k\). Then \(I_{k+1} \mathrel{\vcenter{:}}= I_k[\eta_k]\), \(X_{k+1} = X_k[F_k/v_{\alpha+k}]\) and \(Y_{k+1} = Y_k[G_k/v_{\alpha+k}]\). Denote by \(H_k^\mathfrak{A}\) the move that was for \(\mathfrak{A}\) and by \(H_k^\mathfrak{B}\) the one that was for \(\mathfrak{B}\). After all \(n\) rounds have been played, look at the \(I_n\)-indexed teams \[\begin{align} X_n &= X[H^\mathfrak{A}_0/v_\alpha]\dots[H^\mathfrak{A}_{n-1}/v_{\alpha+n-1}] \quad\text{and} \\ Y_n &= Y[H^\mathfrak{B}_0/v_\alpha]\dots[H^\mathfrak{B}_{n-1}/v_{\alpha+n-1}]. \end{align}\] Then \(\mathrm{\mathbf{II}}\) wins if for all atomic and negated atomic formulas \(\phi\) (including dependence atoms), with free variables in \(\{v_k \mid k<\alpha+n\}\), we have \[\mathfrak{A}\models_{X_n}\phi \implies \mathfrak{B}\models_{Y_n}\phi.\]
Lemma 4. For all \(I\) and \(I\)-indexed teams \(X\) and \(Y\) of \(\mathfrak{A}\) and \(\mathfrak{B}\), respectively, with domain \(D_\alpha\) for some \(\alpha\), if \((\mathfrak{A},X)\mathbin{\Rrightarrow}^\mathcal{D}_n(\mathfrak{B},Y)\), then \[\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}\mathop{\mathrm{EF}}^\mathcal{D}_n((\mathfrak{A},X),(\mathfrak{B},Y)).\]
Proof. We prove the claim by induction on \(n\). First, fix \(X\) and \(Y\) and suppose that \((\mathfrak{A},X)\mathbin{\Rrightarrow}^\mathcal{D}_0(\mathfrak{B},Y)\). This means that for all atomic and negated atomic formulas \(\phi\), \[\mathfrak{A}\models_X\phi \implies \mathfrak{B}\models_Y\phi.\] As this is the winning condition of \(\mathrm{\mathbf{II}}\) in \(\mathop{\mathrm{EF}}^\mathcal{D}_0((\mathfrak{A},X),(\mathfrak{B},Y))\), the only strategy of \(\mathrm{\mathbf{II}}\) in this \(0\)-round game is winning.
Then assume, as the induction hypothesis, that for any \(X\) and \(Y\), if \((\mathfrak{A},X)\mathbin{\Rrightarrow}^\mathcal{D}_n(\mathfrak{B},Y)\), then \[\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}\mathop{\mathrm{EF}}^\mathcal{D}_n((\mathfrak{A},X),(\mathfrak{B},Y)).\] Now fix \(X\) and \(Y\) and suppose that \((\mathfrak{A},X)\mathbin{\Rrightarrow}^\mathcal{D}_{n+1}(\mathfrak{B},Y)\). Let us play \(\mathop{\mathrm{EF}}^\mathcal{D}_{n+1}((\mathfrak{A},X),(\mathfrak{B},Y))\). On the first round, \(\mathrm{\mathbf{I}}\) plays a supplement function \(F_0\). Suppose that \(F_0 = H^\mathfrak{A}_0\) (the case \(F_0 = H^\mathfrak{B}_0\) is symmetric). Now, let \[\Phi = \bigwedge\{\phi(\vec{x}) \mid \vec{x}\in D_{\alpha+1}^{<\omega}, \mathop{\mathrm{qr}}(\phi)\leq n, \mathfrak{A}\models_{X[F_0/v_\alpha]}\phi \}.\] Clearly \(\mathfrak{A}\models_X\exists v_\alpha\Phi\) and \(\mathop{\mathrm{qr}}(\exists v_\alpha\Phi) \leq n+1\). Thus, \(\mathfrak{B}\models_Y\exists v_\alpha\Phi\), whence there is some \(G_0\) such that \(\mathfrak{B}\models_{Y[G_0/v_\alpha]}\Phi\). By downward closedness, we may assume that the type of \(G_0\) is the same as the type of \(F_0\). By the definition of \(\Phi\), we have \(\mathfrak{B}\models_{Y[G_0/v_\alpha]}\phi\) for all \(\phi\) of quantifier rank \(\leq n\) such that \(\mathfrak{A}\models_{X[F_0/v_\alpha]}\phi\). Hence \[(A,X[F_0/v_\alpha]) \mathbin{\Rrightarrow}^\mathcal{D}_n (\mathfrak{B},Y[G_0/v_\alpha]),\] which, by the induction hypothesis, means that \[\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}\mathop{\mathrm{EF}}^\mathcal{D}_n((A,X[F_0/v_\alpha]),(\mathfrak{B},Y[G_0/v_\alpha])).\] Hence, in \(\mathop{\mathrm{EF}}^\mathcal{D}_{n+1}((\mathfrak{A},X),(\mathfrak{B},Y))\), if \(\mathrm{\mathbf{II}}\) plays \(G_0\) as a response to \(\mathrm{\mathbf{I}}\) playing \(F_0\) on the first round, she has a winning strategy from that round onwards. Hence she wins the play. ◻
We could also prove a converse for the previous result, but that is not without complications, as we have dropped the disjunction move that was included in the game of [2]. If we redefine quantifier rank to increase with disjunction and add the disjunction move to the game, then we obviously recover the results of [2].
In this section, we connect the auxiliary game defined in Section 4 to our new game of Section 3. We will then leverage this connection in Section 6 to prove our main result.
The following lemma formulates the consistency and uniformity conditions of \(\mathop{\mathrm{EF}}^{\mathrm{dep}}\) in terms of indexed teams.
Lemma 5.
Suppose that \(I\) is a set and \[P = \{ ((x_0^i,\mathcal{W}_0,\mathcal{U}^+_0,\mathcal{U}^-_0),y_0^i,\dots,(x_{n-1}^i,\mathcal{W}_{n-1},\mathcal{U}^+_{n-1},\mathcal{U}^-_{n-1}),y_{n-1}^i) \mid i\in I \}\] is a set of plays of \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\). Denote \[a_k^i = \begin{cases} x_k^i & \text{if x_k\in A}, \\ y_k^i & \text{otherwise}, \end{cases}\] and let \(X\) be the \(I\)-indexed team \[i\mapsto\{(v_k,a^i_k) \mid k<n\}, \quad i\in I\] of \(\mathfrak{A}\). Then \(\mathrm{\mathbf{I}}\) has played the plays of \(P\) (pairwise) consistently if and only if
for all \(i,j\in I\) and \(k<n\), \(x_k^i\in A\) if and only if \(x_k^j\in A\),
for all \(k<n\) and \(\phi\in\mathcal{U}^+_k\), \(\mathfrak{A}\models_X\phi\),
for all \(k<n\) and \(\phi\in\mathcal{U}^-_k\), \(\mathfrak{A}\models_X\neg\phi\), and
for all \(k<n\) and \(W\in\mathcal{W}_k\), \[\mathfrak{A}\models_X\mathop{=}(\vec{x}, v_k),\] where \(\vec{x}\) enumerates \(\{v_l \mid l\in W\}\).
A strategy \(\tau\) of \(\mathrm{\mathbf{II}}\) in \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) is uniformly winning if and only if the following holds. Suppose that \(I\) is a set and \[\{ ((x_0^i,\mathcal{W}_0,\mathcal{U}^+_0,\mathcal{U}^-_0),y_0^i,\dots,(x_{n-1}^i,\mathcal{W}_{n-1},\mathcal{U}^+_{n-1},\mathcal{U}^-_{n-1}),y_{n-1}^i) \mid i\in I \}\] is a set of plays of \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) such that \(\mathrm{\mathbf{II}}\) has used \(\tau\) and \(\mathrm{\mathbf{I}}\) has played consistently. Denote \[a_k^i = \begin{cases} x_k^i & \text{if x_k\in A}, \\ y_k^i & \text{otherwise}, \end{cases} \quad\text{and}\quad b_k^i = \begin{cases} x_k^i & \text{if x_k\in B}, \\ y_k^i & \text{otherwise}. \end{cases}\] Let \(X\) be the \(I\)-indexed team \[i\mapsto\{(v_k,a^i_k) \mid k<n\}, \quad i\in I,\] of \(\mathfrak{A}\) and \(Y\) the \(I\)-indexed team \[i\mapsto\{(v_k,b^i_k) \mid k<n\}, \quad i\in I,\] of \(\mathfrak{B}\). Then,
for all \(k<n\) and \(\phi\in\mathcal{U}^+_k\), \(\mathfrak{B}\models_Y\phi\),
for all \(k<n\) and \(\phi\in\mathcal{U}^-_k\), \(\mathfrak{B}\models_Y\neg\phi\), and
for all \(k<n\) and \(W\in\mathcal{W}_k\), \[\mathfrak{B}\models_Y\mathop{=}(\vec{x},v_k),\] where \(\vec{x}\) enumerates \(\{v_l \mid l\in W\}\).
Proof.
We show that \(\mathrm{\mathbf{I}}\) has played \(P\) pairwise consistently if and only if the conditions of the statement of the lemma hold.
This is the same condition as in the definition of \(\mathrm{\mathbf{I}}\) playing consistently.
Fix \(k<n\). By flatness and the fact that \(a^i_l = X(i)(v_l)\) for all \(l<n\), for any \(\phi(v_0,\dots,v_{n-1})\in\mathcal{U}^+_k\), we have \[\text{\mathfrak{A}\models\phi(a_0^i,\dots,a_{n-1}^i) for all i\in I} \iff \mathfrak{A}\models_X\phi.\]
The case for \(\mathcal{U}^-_k\) is similar to the previous item.
Fix \(k<n\) and \(W\in\mathcal{W}_k\) and let \(\vec{x}\) enumerate \(\{v_l \mid l\in W\}\). As \(X(i)(v_l) = a^i_l\) for all \(l<n\), we have \[\begin{align} &\forall i,j\in I \bigg[ \forall l\in W (a^i_l = a^j_l) \implies a^i_k = a^j_k \bigg] \\ &\iff \forall i,j\in I \bigg[ \forall l\in W (X(i)(v_l) = X(j)(v_l)) \\ &\implies X(i)(v_k) = X(j)(v_k) \bigg] \\ &\iff \mathfrak{A}\models_X\mathop{=}(\vec{x}, v_k). \end{align}\]
Let \(\tau\) be uniformly winning. Let \(I\), \(x^i_l\), \(\mathcal{W}_l\), \(\mathcal{U}^+_l\), \(\mathcal{U}^-_l\), \(y^i_l\), \(X\) and \(Y\) be as in the statement of the lemma and that \(\mathrm{\mathbf{I}}\) has played consistently. Thus, as \(\tau\) wins uniformly, we have \[\text{b^i_l = b^j_l for all l\in W} \implies b^i_k = b^j_k\] for all \(i,j\in I\), \(k<n\) and \(W\in\mathcal{W}_k\). As we have \(b^i_j = Y(i)(v_j)\) for all \(i\in I\) and \(j<n\), we immediately obtain \(\mathfrak{B}\models_Y\mathop{=}(\vec{x}_W,v_k)\) for each \(W\in\mathcal{W}_k\). Fix \(\phi\in\mathcal{U}^+_k\). As \(\tau\) is winning, we have \[\mathfrak{A}\models\phi(a^i_0,\dots,a^i_{n-1}) \implies \mathfrak{B}\models\phi(b^i_0,\dots,b^i_{n-1})\] for all \(i\in I\). As \(\mathrm{\mathbf{I}}\) has played consistently, we have \(\mathfrak{A}\models\phi(a^i_0,\dots,a^i_{n-1})\). Thus we obtain \(\mathfrak{B}\models\phi(b^i_0,\dots,b^i_{n-1})\). By flatness, \(\mathfrak{B}\models_Y\phi\). The case for \(\phi\in\mathcal{U}^-_k\) is similar.
For the converse, suppose that for any \(I\), \(x^i_l\), \(\mathcal{W}_l\), \(\mathcal{U}^+_l\), \(\mathcal{U}^-_l\), \(y^i_l\), \(X\) and \(Y\) that are as above, the conditions of the statement of the lemma hold. We show that \(\tau\) is uniformly winning. To first show that \(\tau\) is winning, let \[((x^0_0,\mathcal{W}_0,\mathcal{U}^+_0,\mathcal{U}^-_0),y^0_0,\dots,(x^0_{n-1},\mathcal{W}_{n-1},\mathcal{U}^+_{n-1},\mathcal{U}^-_{n-1}),y^0_{n-1})\] be a play where \(\mathrm{\mathbf{II}}\) has used \(\tau\). Now, fix \(k<n\) and \(\phi(v_0,\dots,v_{n-1})\in\mathcal{U}^+_k\) and suppose that \(\mathfrak{A}\models\phi(a_0,\dots,a_{n-1})\). Let \(I = \{0\}\) and define \(x^0_l = x_l\) and \(y^0_l = y_l\) and let \(X\) and \(Y\) be the \(I\)-indexed teams made from the singleton set \[\{ ((x^0_0,\mathcal{W}_0,\mathcal{U}^+_0,\mathcal{U}^-_0),y^0_0,\dots,(x^0_{n-1},\mathcal{W}_{n-1},\mathcal{U}^+_{n-1},\mathcal{U}^-_{n-1}),y^0_{n-1}) \}\] of plays. Clearly \(\mathrm{\mathbf{I}}\) has played the set of plays pairwise consistently. By applying the statement of the lemma, we obtain \(\mathfrak{B}\models_Y\phi\), which by flatness means \(\mathfrak{B}\models\phi(b_0,\dots,b_{n-1})\). The treatment of any \(\phi\in\mathcal{U}^-_k\) is similar.
In order to show that \(\tau\) wins uniformly, let \[((x_0,\mathcal{W}_0,\mathcal{U}^+_0,\mathcal{U}^-_0),y_0,\dots,(x_{n-1},\mathcal{W}_{n-1},\mathcal{U}^+_{n-1},\mathcal{U}^-_{n-1}),y_{n-1})\] and \[((\hat{x}_0,\hat{\mathcal{W}}_0,\hat{\mathcal{U}}^+_0,\hat{\mathcal{U}}^-_0),\hat{y}_0,\dots,(\hat{x}_{n-1},\hat{\mathcal{W}}_{n-1},\hat{\mathcal{U}}^+_{n-1},\hat{\mathcal{U}}^-_{n-1}),\hat{y}_{n-1})\] be two plays where \(\mathrm{\mathbf{II}}\) has used \(\tau\) and \(\mathrm{\mathbf{I}}\) has played consistently. It follows that \(\mathcal{W}_l = \hat{\mathcal{W}}_l\), \(\mathcal{U}^+_l = \hat{\mathcal{U}}^+_l\) and \(\mathcal{U}^-_l = \hat{\mathcal{U}}^-_l\) for all \(l<n\). Fix \(k<n\) and \(W\in\mathcal{W}_k\), and suppose that \(b_l = \hat{b}_j\) for all \(l\in W\). Now, let \(I = \{0,1\}\) and define \(x^0_l = x_l\), \(y^0_l = y_l\), \(x^1_l = \hat{x}_l\) and \(y^1_l = \hat{y}_j\). Let \(X\) and \(Y\) consist of the move sequences of the two players as before. As \(\mathrm{\mathbf{I}}\) has played consistently, we have \(\mathfrak{A}\models_X\mathop{=}(\vec{x}_W,v_k)\) for all \(W\in\mathcal{W}_k\). We may apply our initial assumption to obtain \(\mathfrak{B}\models_Y\mathop{=}(\vec{x}_W,v_k)\) for all \(W\in\mathcal{W}_k\). This means that for all \(W\in\mathcal{W}_k\), \[\text{Y(0)(v_l) = Y(1)(v_l) for all l\in W} \implies Y(0)(v_k) = Y(1)(v_k).\] As \(Y(0)(v_l) = b^0_l = b_l = \hat{b}_l = b^1_l = Y(1)(v_l)\) for all \(l\in W\), we must also have \(b_k = b^0_k = Y(0)(v_k) = Y(1)(v_k) = b^1_k = \hat{b}_k\). This concludes the proof.
◻
Lemma 6. Denote by \(N\) the \(1\)-indexed team \(0\mapsto\emptyset\), and let \(n<\omega\). If \[\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}\mathop{\mathrm{EF}}_n^\mathcal{D}((\mathfrak{A},N),(\mathfrak{B},N)),\] then \[\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}_{\!\textrm u}\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B}).\]
Proof. Let \(\tau\) be a strategy of \(\mathrm{\mathbf{II}}\) in \(\mathop{\mathrm{EF}}_n^\mathcal{D}((\mathfrak{A},N),(\mathfrak{B},N))\). We define a uniform strategy of \(\mathrm{\mathbf{II}}\) in \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) in pieces for each way that \(\mathrm{\mathbf{I}}\) can play consistently. For this, fix \((i_0,\dots,i_{n-1})\in 2^n\) and, for each \(k<n\), \(\mathcal{W}_k\subseteq\mathop{\mathrm{\mathcal{P}}}(n)\) and \(\mathcal{U}^+_k,\mathcal{U}^-_k\subseteq\{ R(\vec{x}) \mid R\in L, \vec{x}\in\{v_0,\dots,v_{n-1}\}^{<\omega}, v_k\in\vec{x}\}\). Let \(P\) be the set of all plays of \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) where \(\mathrm{\mathbf{I}}\) has played consistently and, on each round \(k<n\), \(\mathrm{\mathbf{I}}\) has played the commitments \(\mathcal{W}_k\), \(\mathcal{U}^+_k\) and \(\mathcal{U}^-_k\), and the element \(x_k\) is in \(\mathfrak{A}\) if and only if \(i_k = 0\). Now, consider the set of all possible moves \(x_0^i\), \(i<\alpha_0\), such that the move can lead to a play in \(P\). Let \(X_0 = Y_0 = N\) and \(I_0 = 1\). Denote by \(\eta_0\) the function with domain \(1\) and \(\eta_0(0) = \alpha_0\). We then define a supplement function \(F_0\) of type \(\eta_0\) such that \(\mathop{\mathrm{dom}}(F_0) = 1\), \(F_0(0) = (x_0^i)_{i<\alpha_0}\). Now, \(\tau\) produces a supplement function \(G_0\) of type \(\eta_0\) such that \(\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}\mathop{\mathrm{EF}}_{n-1}^\mathcal{D}((\mathfrak{A},X_1),(\mathfrak{B},Y_1))\), where \(I_1 = I_0[\eta_0]\) and \(X_1\) and \(Y_1\) are the \(I_1\)-indexed teams \(X_0[H_0^\mathfrak{A}/v_0]\) and \(Y_0[H_0^\mathfrak{B}/v_0]\), respectively.
Then, for each \(i\in I_1\), consider all the moves \(x_1^{(i,j)}\), \(j<\alpha_1\), that \(\mathrm{\mathbf{I}}\) can play so that the move sequence \((x_0^i,G_0(0)(i),x_1^{(i,j)})\) can lead to a play in \(P\). Let \(\eta_1\) have domain \(I_1\) and \(\eta_1(i) = \alpha^i_1\) for all \(i\in I_1\). We define a supplement function \(F_1\) of type \(\eta_1\) by setting \(F_1(i) = (x_1^{i,j})_{j<\alpha_1^i}\). Then \(\tau\) produces \(G_1\) of type \(\eta_1\) such that \(\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}\mathop{\mathrm{EF}}^\mathcal{D}_{n-1}((\mathfrak{A},X_2),(\mathfrak{B},Y_2))\), where \(I_2 = I_1[\eta_1]\) and \(X_2\) and \(Y_2\) are the \(I_2\)-indexed teas \(X_1[H_1^\mathfrak{A}/v_1]\) and \(Y_1[H_1^\mathfrak{B}/V_1]\).
By continuing this way, we accumulate teams \(X_n\) and \(Y_n\) that consist of all possible movesets of \(\mathrm{\mathbf{I}}\) where he has played consistently and according to the specification \((i_0,\dots,i_{n-1})\), while playing \(\mathcal{W}_k\), \(\mathcal{U}^+_k\) and \(\mathcal{U}^-_k\) on round \(k\), and the responses of \(\mathrm{\mathbf{II}}\) as described. As \(\mathrm{\mathbf{I}}\) has played consistently, it so happens that \(\mathfrak{A}\models_{X_n}R(\vec{x})\) for all \(R(\vec{x})\in\bigcup_{k<n}\mathcal{U}^+_k\) and \(\mathfrak{A}\models_{X_n}\neg R(\vec{x})\) for all \(R(\vec{x})\in\bigcup_{k<n}\mathcal{U}^-_k\) and \(\mathfrak{A}\models_{X_n}\mathop{=}(\vec{x},v_k)\) for all \(W\in\mathcal{W}_k\), where \(\vec{x}\) enumerates \(\{v_l \mid l\in W\}\). As \(\tau\) is winning in \(\mathop{\mathrm{EF}}_n^\mathcal{D}((\mathfrak{A},N),(\mathfrak{B},N))\), we have \[\mathfrak{A}\models_{X_n}\phi \implies \mathfrak{B}\models_{Y_n}\phi\] for all atomic \(\phi\). Hence, the strategy where \(\mathrm{\mathbf{II}}\) plays \(G_k(i)\) on round \(k\) of \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) as a response to \(\mathrm{\mathbf{I}}\) playing \(F_k(i)\) is uniformly winning. ◻
We could prove the converse of Lemma 6 with a few redefinitions. In \(\mathop{\mathrm{EF}}_n^\mathcal{D}((\mathfrak{A},X),(\mathfrak{B},Y))\) the obvious strategy of \(\mathrm{\mathbf{II}}\) would be to consider assignments of each index \(i\in I\) in \(X\) as moves played in \(\mathfrak{A}\) and in \(Y\) as moves played in \(\mathfrak{B}\) in a single play of \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) and build supplement functions out of possible responses in the uniform game to moves by \(\mathrm{\mathbf{I}}\) given by the supplement function. However, we would need to consider a variant of \(\mathcal{D}\) where we require that dependence atoms only occur in a form \(\mathop{=}(\vec{x}, v_k)\), where \(\vec{x} = (v_{i_0},\dots,v_{i_{m-1}})\) and \(k>i_0,\dots,i_{m-1}\). We would also need to modify \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) so that \(\mathcal{W}_i\subseteq\mathop{\mathrm{\mathcal{P}}}(i)\), i.e. \(\mathrm{\mathbf{I}}\) does not make promises that his move is determined by future moves (which is possible with our current definition).
We are ready to prove the main result of this paper:
Theorem 2. The following are equivalent.
\(\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}_{\!\textrm u}\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) for all \(n<\omega\).
\(\mathfrak{A}\mathbin{\Rrightarrow}^\mathcal{D}\mathfrak{B}\).
Proof. [item:32Dependence32logic32is32preserved]\(\implies\)[item:32II32wins32uniformly32for32all32n]: Suppose that \(\mathfrak{A}\mathbin{\Rrightarrow}^\mathcal{D}\mathfrak{B}\). By Lemma 4, \[\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}\mathop{\mathrm{EF}}^\mathcal{D}_n((\mathfrak{A},N),(\mathfrak{B},N))\] for all \(n<\omega\), whence by Lemma 6, we have \(\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}_{\!\textrm u}\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) for all \(n<\omega\).
[item:32II32wins32uniformly32for32all32n]\(\implies\)[item:32Dependence32logic32is32preserved]: Suppose that \(\mathrm{\mathbf{II}}\mathbin{\raisebox{0.8\depth}{\uparrow}}_{\!\textrm u}\mathop{\mathrm{EF}}^{\mathrm{dep}}_n(\mathfrak{A},\mathfrak{B})\) for all \(n<\omega\). Let \(\phi\) be an arbitrary sentence of dependence logic. We may assume that \(\phi\) is \[\forall v_0\dots\forall v_{m-1}\exists v_m\dots\exists v_{m+k-1}(\psi\land\theta),\] where \(\theta\) is a quantifier-free first-order formula and \(\psi\) is \[\bigwedge_{i<k}\mathop{=}(\vec{u}_i, v_{m+i})\] with \(\vec{u}_i \in\{v_j \mid j<m\}^{<\omega}\) for all \(i<k\). Furthermore, we can assume that \(\theta\) is in disjunctive normal form and let \(\theta\) be \[\bigvee_{i<l}\left( \bigwedge_{j\in U^+_i}\theta^+_j \land \bigwedge_{j\in U^-_i}\neg\theta^-_j \right).\] Then fix a uniform winning strategy \(\tau\) for \(\mathrm{\mathbf{II}}\) in the game of length \(n = m+k\). We now aim at showing that \[\mathfrak{A}\models_N\phi \implies \mathfrak{B}\models_N\phi,\] so suppose that \(\mathfrak{A}\models_N\phi\). Now, let \(X_0 = Y_0 = N\), let \(F^*_0,\dots,F^*_{m-1}\) and \(G_0,\dots,G_{m-1}\) be supplement functions such that \(F^*_i\) duplicates the team \(X^*_i\mathrel{\vcenter{:}}= N[F_0/v_0]\dots[F_{i-1}/v_{i-1}]\), \(G_i\) duplicates \(Y_i\mathrel{\vcenter{:}}= N[G_0/v_0]\dots[G_{i-1}/v_{i-1}]\), \(F^*_i\) and \(G_i\) have the same type, and for every \(b\in B\), \[\{F^*_i(j) \mid G_i(j) = b \} = A\] (i.e. every element of \(\mathfrak{A}\) occurs together with all elements of \(\mathfrak{B}\)). Now, \[\mathfrak{A}\models_{X^*_m}\exists v_m\dots\exists v_{m+k-1}(\psi\land\theta),\] so there are supplement functions \(F_m,\dots,F_{m+k-1}\) such that \[\mathfrak{A}\models_{X^*_m[F_m/v_m]\dots[F_{m+k-1}/v_{m+k-1}]}\psi\land\theta.\] Then let \[\begin{align} X^* &= X^*_m[F_m/v_m]\dots[F_{m+k-1}/v_{m+k-1}] \\ &= N[F^*_0/v_0]\dots[F^*_{m-1}/v_{m-1}][F_m/v_m]\dots[F_{m+k-1}/v_{m+k-1}] \end{align}\] and let \(I\) be its index set. Now there is \(i^*<l\) such that \[\mathfrak{A}\models_{X^*} \bigwedge_{j\in U^+_{i^*}}\theta^+_j \land \bigwedge_{j\in U^-_{i^*}}\neg\theta^-_j.\] Let \(\mathcal{U}^+_p\) consist of all the \(\theta_j^+\) such that \(j\in U^+_{i^*}\), \(\mathcal{U}^-_p\) of all the \(\theta_j^-\) such that \(j\in U^-_{i^*}\) and \(\mathcal{W}_p = \{v_j \mid v_j\in\vec{u}_p\}\) when \(m\leq p < m+k\) and \(\mathcal{W}_p = \emptyset\) otherwise.
Now, let us play \(\mathop{\mathrm{EF}}^{\mathrm{dep}}_{m+k}(\mathfrak{A},\mathfrak{B})\) \(|I|\)-many times. In the \(i^{\text{th}}\) game, on round \(j<m\), we let \(\mathrm{\mathbf{I}}\) play \((Y(i)(j),\mathcal{W}_j,\mathcal{U}^+_j,\mathcal{U}^-_j)\) and denote by \(a^i_j\) the response of \(\mathrm{\mathbf{II}}\) produced by her uniform winning strategy. Now, we define supplement functions \(F_i\) so that \(F_i(j) = a^i_j\). Then let \[X = N[F_0/v_0]\dots[F_{m+k-1}/v_{m+k-1}].\] Now, \(\{X(i) \mid i\in I\}\subseteq\{X^*(i) \mid i\in I\}\), so \(X\) also satisfies \(\psi\) and \[\bigwedge_{j\in U^+_{i^*}}\theta^+_j \land \bigwedge_{j\in U^-_{i^*}}\neg\theta^-_j\] by downward closedness and Lemma 2. On round \(j\geq m\), we let \(\mathrm{\mathbf{I}}\) play \((X(i)(j),\mathcal{W}_j,\mathcal{U}^+_j,\mathcal{U}^-_j)\) and denote by \(b^i_j\) the response of \(\mathrm{\mathbf{II}}\). Now, consider the set of all these plays. Clearly \(\mathrm{\mathbf{I}}\) has played consistently, as demonstrated by the fact that \[\mathfrak{A}\models_X\bigwedge_{i<k}\mathop{=}(\vec{u}_i,v_{m+i})\land\bigwedge_{j\in U^+_{i^*}}\theta^+_j \land \bigwedge_{j\in U^-_{i^*}}\neg\theta^-_j.\] Then denote by \(Y\) the team \(Y_m[G_m/v_m]\dots[G_{m+k-1}/v_{m+k-1}]\), where \(G_{m+j}\) are defined so that \(Y(i)(j) = b^i_j\). As \(\mathrm{\mathbf{II}}\) wins uniformly, we have \[\mathfrak{B}\models_Y\mathop{=}(\vec{u}_p,v_{m+p})\land\bigwedge_{j\in U^+_{i^*}}\theta^+_j \land \bigwedge_{j\in U^-_{i^*}}\neg\theta^-_j\] for all \(p<m+k\). Thus, \(\mathfrak{B}\models_Y\psi\land\theta\), whence \(\mathfrak{B}\models_N\phi\), as desired. ◻
Given that Ehrenfeucht–Fraïssé type games are often used to prove inexpressivity results, it would be illuminating to have more examples. For instance, could we use the game to show that finiteness is not definable in \(\mathcal{D}\)? Even more interesting would be to be able to show that a property not known to be undefinable in \(\mathcal{D}\) is not definable.
Having to settle for the use of a normal form in the proof of our main result is somewhat unsatisfying, and we also lose the connection between the length of the game and the quantifier rank of formulas that are preserved. The alternative could be to restrict both the syntax of \(\mathcal{D}\) and the commitments made in the game (and this would also reconnect quantifier rank and game length), but this also seems unsatisfactory. Is it possible to connect the length of the game to quantifier rank of the formulas in some reasonable manner?
Lemma 6 utilizes the fact that \(\mathop{\mathrm{EF}}^{\mathcal{D}}_n((\mathfrak{A},X),(\mathfrak{B},Y))\) is symmetric, which is made possible by Lemma 1—a result that does not necessarily hold if one moves from \(\mathcal{D}\) to some other logic that is not downward closed. The main result also uses some amount of downward closedness. Therefore the results of this paper cannot immediately be lifted to, say, inclusion logic. Thus, a question arises: can a similar game be found for other team logics, most notably inclusion logic and independence logic?
The first author was supported by U.K. EPSRC Research Fellowship EP/V040944/1, Resources in Computation.↩︎
The second author has received funding from the Academy of Finland (decision number 368671) and the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 101020762).↩︎
One way to do this is to add a constant symbol for each colour. Another option is to simply play two additional rounds of the game in the beginning and treat the two first moves of each player as the two colours in each graph. Then a colouring of either of the graphs will correspond to a function on the graph that maps each element to one of these two distinguished elements.↩︎
Here \(\mathfrak{A}\models_s\phi(x_0,\dots,x_{n-1})\) means \(\mathfrak{A}\models\phi(s(x_0),\dots,s(x_{n-1}))\).↩︎
Or, rather, the meaning is trivialized, for a singleton team always satisfies all dependence atoms.↩︎