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