=Paper=
{{Paper
|id=Vol-1326/132-Kuusisto
|storemode=property
|title=Team Semantics and Recursive Enumerability
|pdfUrl=https://ceur-ws.org/Vol-1326/132-Kuusisto.pdf
|volume=Vol-1326
|dblpUrl=https://dblp.org/rec/conf/sofsem/Kuusisto15
}}
==Team Semantics and Recursive Enumerability==
<pdf width="1500px">https://ceur-ws.org/Vol-1326/132-Kuusisto.pdf</pdf>
<pre>
    Team Semantics and Recursive Enumerability

                                    Antti Kuusisto

                            University of Wroclaw, Poland,
                           Technical University of Denmark
                            Stockholm University, Sweden
                              antti.j.kuusisto@uta.fi



       Abstract. It is well known that dependence logic captures the comple-
       xity class NP, and it has recently been shown that inclusion logic captures
       P on ordered models. These results demonstrate that team semantics
       offers interesting new possibilities for descriptive complexity theory. In
       order to properly understand the connection between team semantics
       and descriptive complexity, we introduce an extension D∗ of dependence
       logic that can define exactly all recursively enumerable classes of finite
       models. Thus D∗ provides an approach to computation alterative to
       Turing machines. The essential novel feature in D∗ is an operator that
       can extend the domain of the considered model by a finite number of
       fresh elements.

       Keywords: team semantics, dependence logic, descriptive complexity


1    Introduction

In this article we study logics based on team semantics. Team semantics was
originally conceived by Hodges [7] in the context of IF-logic [6]. On the intuitive
level, team semantics provides an alternative compositional approach to systems
based on game-theoretic semantics. The compositional approach simplifies the
more traditional game-theoretic approaches in several ways.
     In [13], Väänänen introduced dependence logic (D), which is a novel approach
to IF-logic based on new atomic formulae =(x1 , ..., xk , y) that can be interpreted
to mean that the choice for the value of y is functionally determined by the
choices for the values of x1 , ..., xk in a semantic game.
     After the introduction of dependence logic, research on logics based on team
semantics has been very active. Several different logics with different applica-
tions have been investigated. Currently the two most important systems stud-
ied in the field in addition to dependence logic are independence logic [4] of
Grädel and Väänänen and inclusion logic [2] of Galliani. Independence logic
is a variant of dependence logic that extends first-order logic by new atomic
formulae x1 , ..., xk ⊥ y1 , ..., yn with the intuitive meaning that the interpreta-
tions of the variables x1 , ..., xk are independent of the interpretations of the
variables y1 , ..., yn . Inclusion logic extends first-order logic by atomic formulae
x1 , ..., xk ⊆ y1 , ..., yk , whose intuitive meaning is that each tuple interpreting the
                                  Team Semantics and Recursive Enumerability              133

variables x1 , ..., xk must also be a tuple that interprets y1 , ..., yk . Exclusion logic,
also introduced in [2] by Galliani, is a natural counterpart of inclusion logic with
atoms x1 , ..., xk | y1 , ..., yk which state that the set of tuples interpreting x1 , ..., xk
must not overlap with the set of tuples interpreting y1 , ..., yk .
    It was observed in [13] and [4] that dependence logic and independence logic
are both equi-expressive with existential second-order logic, and thereby capture
NP. Curiously, it was established in [3] that inclusion logic is equi-expressive
with greatest fixed point logic and thereby captures P on finite ordered models.
These results show that team semantics offers a novel interesting perspective
on descriptive complexity theory. Especially the very close connection between
team semantics and game-theoretic concepts is interesting in this context.
    In order properly understand the perspective on descriptive complexity pro-
vided by team semantics, it makes sense to accomodate the related logics in
a unified umbrella framework that exactly characterizes the computational ca-
pacity of Turing machines. It turns out that there exists a particularly simple
extension of dependence logic that does the job. Let D∗ denote the logic ob-
tained by extending first-order logic by the atoms of dependence, independence,
inclusion, and exclusion logic, and furthermore, an operator Ix that extends
the domain of the model considered by a finite number of fresh elements. We
show below that D∗ can define exactly all recursively enumerable classes of finite
models.
    Since D∗ captures RE, it is not only a logic but also a model of computation.
The striking simplicity of D∗ and the link between team semantics and game-
theory make D∗ a particularly interesting system. There of course exist other
logical frameworks where RE can be easily captured, such as abstract state
machines [5], [1] and the recursive games of [10]. However, D∗ provides a simple
unified perspective on recent advances in descriptive complexity based on team
semantics. The framework of [10] resembles D∗ since it provides a perspective
on RE that explains computational notions via game-theoretic concepts, but the
approach in [10] is burdened by potentially infinite games and [10] also lacks
a compositional approach. The approach provided by D∗ is at least in some
reasonable sense more straighforward.


2    Preliminaries

We consider only models with a purely relational vocabulary, i.e., a vocabulary
consisting of relation symbols only. Therefore, all vocabularies are below assumed
to be purely relational without further warning. We let A, B, C, etc., denote
models; A, B and C denote the domains of the models A, B and C, respectively.
    We let VAR denote a countably infinite set of exactly all first-order variable
symbols. Let X ⊆ VAR be a finite, possibly empty set. Let A be a set. A function
s : X → A is called an assignment with domain X and codomain A. We let s[a/x]
denote the assignment with domain X ∪ {x} and codomain A ∪ {a} defined such
that s[a/x](y) = a if y = x, and s[a/x](y) = s(a) if y 6= x. Let T be a set. We
define s[ T /x ] = { s[a/x] | a ∈ T }.
134      A. Kuusisto

     Let X ⊆ VAR be a finite, possibly empty set. Let U be a set of assignments
s : X → A. Such a set U is a team with domain X and codomain A. Note that
the empty set is a team with codomain A, as is the set {∅} containing only the
empty assignment. The team ∅ does not have a unique domain; any finite subset
of VAR is a domain of ∅. The domain of the team {∅} is ∅. The domain of team
U is denoted by Dom(U ).
     Let T be a set. We define U [ T /x ] := { s[a/x] | a ∈ T, s ∈ U }. Let
f : U → P(TS  ) be a function, where P denotes the power set operator. We define
U [ f /x ] :=     s[ f (s)/x ].
             s∈U
     Let V be a team. Let k ∈ Z+ , where Z+ denotes  
      the positive integers.
                                                                              
        Let
x1 , ..., xk ∈ Dom(V ). Define Rel V, (x1 , ..., xk ) := { s(x1 ), ..., s(xk ) | s ∈ V }.
     We then define lax team semantics for formulae of first-order logic (FO). As
usual in investigations related to team semantics, formulae are assumed to be
in negation normal form, i.e., negations occur only in front of atomic formulae.
Let A be a model and U a team with codomain A. Let |=FO denote the ordinary
Tarskian satisfaction relation of first-order logic, i.e., A, s |=FO ϕ means that the
model A satisfies the first-order formula ϕ under the assignment s. We define
                                                             

       A, U |= x = y             ⇔ ∀s ∈ U A, s |=FO x = y ,

       A, U |= ¬x = y            ⇔ ∀s ∈ U A, s |=FO ¬x = y ,           

       A, U |= R(x1 , ..., xk ) ⇔ ∀s ∈ U A, s |=FO R(x1 , ..., xk ) ,

       A, U |= ¬R(x1 , ..., xk ) ⇔ ∀s ∈ U A, s |=FO ¬R(x1 , ..., xk ) ,
       A, U |= (ϕ ∧ ψ)           ⇔ A, U |= ϕ and A, U |= ψ,
       A, U |= (ϕ ∨ ψ)           ⇔ A, U0 |= ϕ and A, U1 |= ψ for some
                                   teams U0 , U1 ⊆ U such that U0 ∪ U1 = U,
       A, U |= ∀x ϕ              ⇔ A, U [ A/x ] |= ϕ,
       A, U |= ∃x ϕ              ⇔ A, [ f /x ] |= ϕ for some f : U → (P(A) \ ∅).

A sentence ϕ is true in A (A |= ϕ) if A, {∅} |= ϕ. It is well known and easy to
show that for an FO-formula ϕ, we have A, U |= ϕ iff A, s |=FO ϕ for all s ∈ U .

Proposition 1. Let ϕ be a formula of first-order logic. Let U be a team. Then
A, U |= ϕ iff ∀s ∈ U (A, s |=FO ϕ).                                         t
                                                                            u

     Dependence logic (D) is the extension of first-order logic in negation normal
form with novel atoms = (x1 , ..., xk ) for each positive integer k. These atoms
are called dependence atoms. The semantics dictates that A, U |==(x1 , ..., xk )
iff for each s, t ∈ U such that s(xi ) = t(xi ) for each i ∈ {1, ..., k − 1}, we have
s(xk ) = t(xk ). We note that dependence logic is sometimes formulated such that
negated atoms ¬=(x1 , ..., xk ) are allowed, but since the semantics then dictates
that A, U |= ¬=(x1 , ..., xk ) iff U = ∅, these negated atoms can be replaced by
∃x(x 6= x).
     Inclusion logic is obtained by extending first-order logic in negation normal
form by atoms x1 , ..., xk ⊆ y1 , ..., yk with the semantics A, U |= x1 , ..., xk ⊆
y1 , ..., yk iff Rel (U, (x1 , ..., xk )) ⊆ Rel (U, (y1 , ..., yk )). Here k can be any positive
integer. Similarly, exclusion logic extends first-order logic in negation normal
                                     Team Semantics and Recursive Enumerability                 135

form with atoms x1 , ..., xk | y1 , ..., yk such that A, U |= x1 , ..., xk | y1 , ..., yk iff
Rel (U, (x1 , ..., xk )) ∩ Rel (U, (y1 , .., yk )) = ∅. Again k can be any positive integer.
Independence logic extends first-order logic in negation normal form with atoms
x1 , ..., xk ⊥z1 ,...,zm y1 , ..., yn such that A, U |= x1 , ..., xk ⊥z1 ,...,zm y1 , ..., yn iff for
all s, s0 ∈ U there exists a t ∈ U such that
  ^                                ^                     ^                    ^
        s(zi ) = s0 (zi ) ⇒                                                      t(yi ) = s0 (yi ) .
                         
                                                                         

                                       t(xi ) = s(xi ) ∧   t(zi ) = s(zi ) ∧
 i≤m                           i≤k                    i≤m                    i≤n

Here k, m, n can be any positive integers. Independence logic also contains atoms
                                                                                         0
x1 , ..., xk ⊥ y1 , ..., yn such that V
                                      A, U |= x1 , ..., xk ⊥ y1 , ...,
                                                                   V yn iff for all0 s, s ∈ U
there exists a t ∈ U such that i≤k t(xi ) = s(xi ) and i≤n t(yi ) = s (yi ). Here
k and n can be any positive integers.
     Let A be a model and τ its vocabulary. Let S 6= ∅ be finite a set such that
S ∩ A = ∅. We let A + S denote the model B such that B = A ∪ S and RB = RA
for all R ∈ τ . The model B is called a finite bloating of A.
     We then define the logic D∗ that captures recursive enumerability. In the
spirit of team semantics, D∗ is based on the use of sets of assignments, i.e.,
teams, that involve first-order variables. Let D+ denote the logic obtained by
extending first-order logic in negation normal form by all dependence atoms,
independence atoms, inclusion atoms, and exclusion atoms. D∗ is obtained by
extending D+ by an additional formula formation rule stating that if ϕ is a
formula, then so is Ix ϕ. We define A, U |= Ix ϕ iff there exists a finite bloating
A + S of A such that A + S, U [S/x] |= ϕ. We note that there are connections
between different classes of atoms: for example, since =(x1 , ..., xk , y) is equivalent
to y⊥x1 ,...,xk y, dependence atoms can in fact be very easily eliminated from D∗ .
     Note that if desired, we can avoid reference to a proper class of possible
bloatings of A in the semantics of D∗ by letting A1 := A ∪ {A} to be the
canonical bloating of A by one element and Ak+1 := Ak ∪ {Ak } the bloating of
A by k + 1 elements.


3    D∗ Captures RE
Let τ be a vocabulary. Sentences of existential second-order logic (ESO) over τ
are formulae of the type ∃X1 ...∃Xk ϕ, where X1 , ..., Xk are relation variables and
ϕ a sentence of FO over τ ∪ {X1 , ..., Xk }. The symbols X1 , ..., Xk are not in τ .
We extend ESO by defining a logic LRE , whose τ -sentences are of the type IY ψ,
where Y 6∈ τ is a unary relation variable and ψ an ESO-sentence over τ ∪ {Y }.
Let A be a τ -model. The semantics of LRE is defined such that A |= IY ψ iff
there exists a finite set S 6= ∅ such that the following conditions hold.
 1. A ∩ S = ∅.
 2. Let A+ be the model of the vocabulary τ ∪ {Y } with domain A ∪ S such
            +           +
    that Y A = S and RA = RA for all R ∈ τ . We have A+ |= ψ.
   As we shall see, the logic LRE can define in the finite exactly all recursively
enumerable classes of finite models.
136     A. Kuusisto

    Let σ 6= ∅ be a finite set of unary relation symbols and Succ a binary relation
symbol. A word model over the vocabulary {Succ} ∪ σ is a model A defined as
follows.

 1. The domain A of A is a nonempty finite set. The predicate Succ is a successor
    relation over A, i.e., a binary relation corresponding to a linear order, but
    with maximum out-degree and in-degree equal to one.
 2. Let b ∈ A be the smallest element with respect to Succ. We have b 6∈ P A for
    all P ∈ σ. (This is because we do not allow models with the empty domain;
    the empty word corresponds to the word model with exactly one element.)
    For all a ∈ A \ {b}, there is exactly one P ∈ σ such that a ∈ P A .

    Word models canonically encode finite words. For example the word abbaa
over the alphabet {a, b} is encoded by the word model M over the vocabulary
{Succ, Pa , Pb } defined such that M = {0, ..., 5} and Succ M is the canonical
successor relation on M , and we have PaM = {1, 4, 5} and PbM = {2, 3}.
    When investigating computations on structure classes (rather than strings),
Turing machines of course operate on encodings of structures. We will use the
encoding scheme of [11]. Let τ be a finite vocabulary and A a finite τ -structure.
In order to encode the structure A by a binary string, we first need to define
a linear ordering of the domain A of A. Let <A denote such an ordering.
    Let R ∈ τ be a k-ary relation symbol. The encoding enc(RA ) of RA is the
    k
|A| -bit string defined as follows. Consider an enumeration of all k-tuples over
A in the lexicographic order defined with respect to <A . In the lexicographic
order, (a1 , ..., ak ) is smaller than (a01 , ..., a0k ) iff there exists i ∈ {1, ..., k} such
that ai < a0i and aj = a0j for all j < i. There are |A|k tuples in Ak , and the
string enc(RA ) is the word t ∈ {0, 1}∗ of the length |A|k such that the bit ti of
t = t1 ... t|A|k is 1 if and only if the i-th tuple (a1 , ..., ak ) ∈ Ak in the lexicographic
order is in the relation RA .
    The encoding enc(A) is defined as follows. We first order the relations in τ .
Let p be the number of relations in τ , and let R1 , ..., Rp enumerate the symbols
in τ according to the order. We define enc(A) := 0|A| · 1 · enc(R1A ) · ... · enc(RpA ).
Notice that the encoding of A indeed depends on the order <A and the ordering
of the relation symbols in τ , so A in general has several encodings. However, we
assume that τ is always ordered in some canonical way, so the multiplicity of
encodings results in only due to different orderings of the domain of A.
    Let τ be a finite vocabulary. A Turing machine TM defines a semi-decision
algorithm for a class C of finite τ -models iff there is an accepting run for TM on
an input w ∈ {0, 1}∗ exactly when w is some encoding of some structure A ∈ C.

Proposition 2. In the finite, LRE can define exactly all recursively enumerable
classes of models.

Proof. Let TM be a Turing machine that defines a semi-decision algorithm for
some class of models. It is routine to write a formula ϕTM := IY ∃X ψ such
that A |= ϕTM if there exists an extension B of A that consist essentially of
                                  Team Semantics and Recursive Enumerability               137

a copy of A and another part C that encodes the computation table of an ac-
cepting computation of TM on an input enc(A). We can use the predicates in
∃X in order to define word models that encode enc(A) and other strings that
correspond to the Turing machine tape at different stages of the computation.
Symbols in ∃X can also be used, inter alia, in order to define the other parts of
the computation table and an ordering of the domain of A, and also relations
that connect A to C in order to ensure A and C are correctly related. The symbol
Y is used in order to see which points belong to the original model A.
   For the converse, given a sentence IY ∃X ψ of LRE , we can define a Turing
machine that first non-deterministically provides a number k ∈ Z+ of fresh
points to be added to the domain of the model considered, and then checks if
∃X ψ holds in the obtained larger model.                                       t
                                                                               u
     Our next aim is to discuss Lemma 1, which essentially provides a way of
encoding a unary relation symbol Y by a corresponding variable symbol y with
the help of inclusion, exclusion, and independence atoms. For the purposes of the
Lemma, we first define a translation from dependence logic to D+ . Rönnholm
considers a translation with similar intuitions in [12].
     Let χ be a sentence of dependence logic over a vocabulary τ such that Y 6∈ τ .
Let y, v, u, u0 be variables that do not occur in χ. We next define a translation
TYy (χ) of χ into D+ by recursion on the structure of χ. (Strictly speaking, the
variables v, u, u0 are fixed parameters of the translation just like y and Y , so
                          0
we should write TYy,v,u,u (χ) instead of TYy (χ). The issue here is only that when
a sentence χ is translated, the auxiliary variables y, v, u, u0 should not occur in
χ.)

 1. TYy (R(x1 , ..., xk )) := R(x1 , ..., xk ) and TYy (¬R(x1 , ..., xk )) := ¬R(x1 , ..., xk )
 2. TYy (x = z) := x = z and TYy (¬x = z) := ¬x = z
 3. TYy (Y (x)) := x ⊆ y and TYy (¬Y (x)) := x|y
 4. TYy ( =(x1 , ..., xk ) ) := =(x1 , ..., xk )
 5. TYy ( (ϕ ∧ ψ) ) := ( (TYy (ϕ) ∧ TYy (ψ) )
 6. TYy ( (ϕ ∨ ψ) ) := ∃v v⊥z y ∧ (TYy (ϕ) ∧ v = u) ∨ (TYy (ψ) ∧ v = u0 ) , where
                                                                                 



    z contains exactly all variables quantified superordinate to (ϕ ∨ ψ) in χ, i.e.,
    exactly each x such that (ϕ ∨ ψ) is in the scope of ∃x or ∀x.
 7. Assume ∃x ϕ is subordinate to a disjunction in χ, meaning that there is
    a subformula (α ∨ β) of χ and ∃x ϕ           
 is a subformula of (α ∨ β). We define
    TYy (∃x ϕ) := ∃x x⊥z yv ∧ TYy (ϕ) , where z contains exactly all variables
    quantified superordinate to ∃x ϕ in χ, with the exception that z never con-
    tains x; the exception is relevant if χ contains nested quantification of x.
 8. Assume ∃x ϕ is not 
subordinate to a disjunction in χ. Then TYy (∃x ϕ) :=
    ∃x x⊥z y ∧ TYy (ϕ) , where z contains exactly all variables quantified su-
    perordinate to ∃x ϕ in χ, with the exception that z never contains x.
 9. TYy (∀x ϕ) := ∀x (TYy (ϕ))

   Let A be a model such that |A| ≥ 2. Let S ⊆ A. Let χ be a sentence of
dependence logic and ϕ a subformula of χ. Let (U, V ) a pair of be teams with
codomain A such that the following conditions hold.
138     A. Kuusisto

 1. Call Z := Dom(U ). Z contains exactly all variables quantified superordinate
    to ϕ in χ. Dom(V ) is Z ∪ {y, u, u0 } or Z ∪ {y, v, u, u0 }; we have v ∈ Dom(V )
    iff ϕ is subordinate to a disjunction in χ.
 2. We have U = V  Z, i.e., U = { s  Z | s ∈ V }, where Z = Dom(U ).
 3. There exists a team X such that V = X[S/y]. (Thus S 6= ∅ if V 6= ∅.)
 4. For all s, t ∈ V , we have s(u) = t(u) 6= t(u0 ) = s(u0 ). In other words, every
    assignment in V gives exactly the same interpretation to u and to u0 , and
    the interpretation of u is different from that of u0 .
When (U, V ) satisfies the above four conditions, we say that (U, V ) is a suitable
pair for A, S ⊆ A, (y, v, u, u0 ) and (ϕ, χ). Below A, S, and (y, v, u, u0 ) will always
be clear from the context (and in fact the same everywhere), so we may simply
talk about suitable pairs for (ϕ, χ).
    Let B be a model and T ⊆ B a set. Let τ be the vocabulary of B. Let P 6∈ τ
be a unary relation symbol. We let (B, P 7→ T ) denote the expansion of B to
the vocabulary τ ∪ {P } such that P B = T .
    Let s be an assignment with domain X. Let {x1 , ..., xk } be a finite set of
variables. We let s−{x1 ,...,xk } denote the assignment s  (X \ {x1 , ..., xk }).
Lemma 1. Let χ be a sentence of dependence logic not containing the symbols
y, v, u, u0 . Let A be a model with at least two elements. Let Y be a unary relation
symbol that occurs neither in χ nor in the vocabulary of A. Let S ⊆ A. Let
({∅}, V ) be
 a suitable pair of for A, S, (y, v, u, u0 ) and (χ, χ). Then we have
 A, Y 7→ S , {∅} |= χ iff A, V |= TYy (χ).
Proof. Prove by induction on 
the structure of χ that for any subformula ϕ of
χ, the equivalence A, Y 7→ S , U |= ϕ ⇔ A, V |= TYy (ϕ) holds for all suitable
pairs (U, V ) for A, S, (y, v, u, u0 ) and (ϕ, χ).                          t
                                                                            u
   Define TYy (ϕ) := ∃u∃u0 u 6= u0 ∧ =(u) ∧ =(u0 ) ∧ TYy (ϕ) ). The following
Lemma now follows directly.
Lemma 2. Let A be a model such that |A| ≥ 2. Let S ⊆ A be a nonempty
finite set. Let ϕ be a sentence of dependence logic. Let y be a variable that does
not occur in ϕ. Let Y be a unary symbol that occurs neither in ϕ nor in the
vocabulary of A. Then (A, Y 7→ S), {∅} |= ϕ iff A, {∅}[S/y] |= TYy (ϕ).         t
                                                                                u
Theorem 1. LRE is contained in D∗ .
Proof. It is well known that every sentence α of ESO translates to an equivalent
sentence α# of dependence logic, see [13]. We shall use this translation below.
   Let ϕ := IY ∃Xψ be a sentence of LRE , where ψ is a first-order sentence.
The following chain of equivalences, where the penultimate equivalence follows
by Lemma 2, settles the current theorem.
                          

A |= ϕ ⇔ A + S, Y 7→ S |= ∃Xψ for some finite S 6= ∅ s.t. S ∩ A = ∅
                          
              
#
       ⇔ A + S, Y 7→ S , {∅} |= ∃Xψ           for some finite S 6= ∅ s.t. S ∩ A = ∅
                                          #
       ⇔ A + S, {∅}[S/y] |= TyY ∃Xψ
                                        
   

                                              for some finite S 6= ∅ s.t. S ∩ A = ∅
                          y       
# 

       ⇔ A, {∅} |= Iy TY ∃Xψ
                                Team Semantics and Recursive Enumerability         139

                                                                                     t
                                                                                     u

Theorem 2. D∗ is contained in LRE .

Proof. Let ϕ be a sentence of D∗ . Assume ϕ contains k occurrences of the
operator I. Let TM be a Turing machine such that when given an input model A,
TM first nondeterministically constructs a tuple n ∈ (Z+ )k that gives for each
occurrence of I in ϕ a number of new points to be added to the model. Then TM
checks whether A satisfies ϕ with the given tuple n of cardinalites to be added
during the evaluation. TM is a semi-decision algorithm corresponding to ϕ. t  u

4    Conclusions
We have shown how the standard logics based on team semantics extend natu-
rally to the simple system D∗ that captures RE. The system D∗ nicely expands
the scope of team semantics from logic to computation. It will be interesting to
investigate, for example, what kind of decidable fragments D∗ has. Furthermore,
it would be interesting to investigate generalized quantifiers and generalized
atoms ([8,9]) in the context of D∗ .


References
 1. Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High- Level System
    Design and Analysis. Springer (2003)
 2. Galliani, P.: Inclusion and exclusion dependencies in team semantics - on some
    logics of imperfect information. Ann. Pure Appl. Logic, 163(1), pp. 68-84, (2012)
 3. Galliani, P., Hella, L.: Inclusion logic and Fixed point logic. In: CSL 2013,
    pp. 281-295 (2013)
 4. Grädel, E., Väänänen, J.: Dependence and independence. Studia Logica, 101(2),
    pp. 399-410 (2013)
 5. Gurevich, Y.: A new thesis. American Mathematical Soc. Abstracts, 6(4), p. 317
    (1985)
 6. Hintikka, J., Sandu, G.: Informational independence as a semantical phenomenon.
    In: Logic, Methodology and Philosophy of Science VIII, Elsevier (1989)
 7. Hodges, W.: Compositional semantics for a language of imperfect information.
    Logic Journal of the IGPL, 5, 539-563 (1997)
 8. Kuusisto, A.: Logics of incomplete information without identity. TamPub, Uni-
    versity of Tampere (2011)
 9. Kuusisto, A.: A double team semantics for generalized quantifiers. CoRR,
    abs/1310, 3032 (2013)
10. Kuusisto, A.: Some Turing-complete extensions of First-order logic. CoRR,
    abs/1405,1715 (2014)
11. Libkin, L.: Elements of Finite Model Theory. Springer (2004)
12. Rönnholm, R.: Inkluusio ja ekskluusio kvantifioinnissa. TamPub, University of
    Tampere (2014)
13. Väänänen, J.: Dependence logic: A new approach to independence friendly logic.
    Cambridge University Press (2007)

</pre>