It is well known that dependence logic captures the complexity class NP, and it has recently been shown that inclusion logic captures P on ordered models. These results demonstrate that team semantics o ers 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 de ne exactly all recursively enumerable classes of nite 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 nite number of fresh elements.
In this article we study logics based on team semantics. Team semantics was
originally conceived by Hodges [
In [
After the introduction of dependence logic, research on logics based on team
semantics has been very active. Several di erent logics with di erent
applications have been investigated. Currently the two most important systems
studied in the eld in addition to dependence logic are independence logic [
It was observed in [
In order properly understand the perspective on descriptive complexity provided by team semantics, it makes sense to accomodate the related logics in a uni ed umbrella framework that exactly characterizes the computational capacity 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 obtained by extending rst-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 nite number of fresh elements. We show below that D can de ne exactly all recursively enumerable classes of nite 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
gametheory make D a particularly interesting system. There of course exist other
logical frameworks where RE can be easily captured, such as abstract state
machines [
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 in nite set of exactly all rst-order variable symbols. Let X VAR be a nite, 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 [ fxg and codomain A [ fag de ned 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 de ne s[ T =x ] = f s[a=x] j a 2 T g:
Let X VAR be a nite, 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 f;g containing only the empty assignment. The team ; does not have a unique domain; any nite subset of VAR is a domain of ;. The domain of the team f;g is ;. The domain of team U is denoted by Dom(U ).
Let T be a set. We de ne U [ T =x ] := f s[a=x] j a 2 T; s 2 U g. Let f : U ! P(T ) be a function, where P denotes the power set operator. We de ne U [ f =x ] := S s[ f (s)=x ]:
s 2 U
Let V be a team. Let k 2 Z+, where Z+ denotes the positive integers. Let x1; :::; xk 2 Dom(V ). De ne Rel V; (x1; :::; xk) := f s(x1); :::; s(xk) j s 2 V g:
We then de ne lax team semantics for formulae of rst-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 j=FO denote the ordinary Tarskian satisfaction relation of rst-order logic, i.e., A; s j=FO ' means that the model A satis es the rst-order formula ' under the assignment s. We de ne A; U j= x = y , 8s 2 U A; s j=FO x = y ; A; U j= :x = y , 8s 2 U A; s j=FO :x = y ; A; U j= R(x1; :::; xk) , 8s 2 U A; s j=FO R(x1; :::; xk) ; A; U j= :R(x1; :::; xk) , 8s 2 U A; s j=FO :R(x1; :::; xk) ; A; U j= (' ^ ) , A; U j= ' and A; U j= ; A; U j= (' _ ) , A; U0 j= ' and A; U1 j= for some
teams U0; U1 U such that U0 [ U1 = U; A; U j= 8x ' , A; U [ A=x ] j= ';
A; U j= 9x ' , A; [ f =x ] j= ' for some f : U ! (P(A) n ;): A sentence ' is true in A (A j= ') if A; f;g j= '. It is well known and easy to show that for an FO-formula ', we have A; U j= ' i A; s j=FO ' for all s 2 U . Proposition 1. Let ' be a formula of rst-order logic. Let U be a team. Then A; U j= ' i 8s 2 U (A; s j=FO '): tu
Dependence logic (D) is the extension of rst-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 j==(x1; :::; xk) i for each s; t 2 U such that s(xi) = t(xi) for each i 2 f1; :::; k 1g, 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 j= :=(x1; :::; xk) i U = ;, these negated atoms can be replaced by 9x(x 6= x).
Inclusion logic is obtained by extending rst-order logic in negation normal form by atoms x1; :::; xk y1; :::; yk with the semantics A; U j= x1; :::; xk y1; :::; yk i Rel (U; (x1; :::; xk)) Rel (U; (y1; :::; yk)). Here k can be any positive integer. Similarly, exclusion logic extends rst-order logic in negation normal form with atoms x1; :::; xk j y1; :::; yk such that A; U j= x1; :::; xk j y1; :::; yk i Rel (U; (x1; :::; xk)) \ Rel (U; (y1; ::; yk)) = ;. Again k can be any positive integer. Independence logic extends rst-order logic in negation normal form with atoms x1; :::; xk ?z1;:::;zm y1; :::; yn such that A; U j= x1; :::; xk ?z1;:::;zm y1; :::; yn i for all s; s0 2 U there exists a t 2 U such that ^ s(zi) = s0(zi) ) i m ^ t(xi) = s(xi) ^ i k ^ t(zi) = s(zi) ^ ^ t(yi) = s0(yi) : i m i n Here k, m, n can be any positive integers. Independence logic also contains atoms x1; :::; xk ? y1; :::; yn such that A; U j= x1; :::; xk ? y1; :::; yn i for all s; s0 2 U there exists a t 2 U such that Vi k t(xi) = s(xi) and Vi n t(yi) = s0(yi): Here k and n can be any positive integers.
Let A be a model and its vocabulary. Let S 6= ; be nite 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 2 . The model B is called a nite bloating of A.
We then de ne 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 rst-order variables. Let D+ denote the logic obtained by extending rst-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 de ne A; U j= Ix ' i there exists a nite bloating A + S of A such that A + S; U [S=x] j= '. We note that there are connections between di erent 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 [ fAg to be the canonical bloating of A by one element and Ak+1 := Ak [ fAkg the bloating of A by k + 1 elements. 3
D
Let be a vocabulary. Sentences of existential second-order logic (ESO) over are formulae of the type 9X1:::9Xk ', where X1; :::; Xk are relation variables and ' a sentence of FO over [ fX1; :::; Xkg. The symbols X1; :::; Xk are not in . We extend ESO by de ning a logic LRE , whose -sentences are of the type IY , where Y 62 is a unary relation variable and an ESO-sentence over [ fY g. Let A be a -model. The semantics of LRE is de ned such that A j= IY i there exists a nite set S 6= ; such that the following conditions hold. 1. A \ S = ;. 2. Let A+ be the model of the vocabulary [ fY g with domain A [ S such that Y A+ = S and RA+ = RA for all R 2 . We have A+ j= .
As we shall see, the logic LRE can de ne in the nite exactly all recursively enumerable classes of nite models.
Let 6= ; be a nite set of unary relation symbols and Succ a binary relation symbol. A word model over the vocabulary fSuccg [ is a model A de ned as follows. 1. The domain A of A is a nonempty nite 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 2 A be the smallest element with respect to Succ. We have b 62 P A for all P 2 . (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 2 A n fbg, there is exactly one P 2 such that a 2 P A.
Word models canonically encode nite words. For example the word abbaa over the alphabet fa; bg is encoded by the word model M over the vocabulary fSucc; Pa; Pbg de ned such that M = f0; :::; 5g and SuccM is the canonical successor relation on M , and we have PaM = f1; 4; 5g and PbM = f2; 3g.
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 [
Let R 2 be a k-ary relation symbol. The encoding enc(RA) of RA is the jAjk-bit string de ned as follows. Consider an enumeration of all k-tuples over A in the lexicographic order de ned with respect to <A. In the lexicographic order, (a1; :::; ak) is smaller than (a01; :::; a0k) i there exists i 2 f1; :::; kg such that ai < a0i and aj = a0j for all j < i. There are jAjk tuples in Ak, and the string enc(RA) is the word t 2 f0; 1g of the length jAjk such that the bit ti of t = t1 ::: tjAjk is 1 if and only if the i-th tuple (a1; :::; ak) 2 Ak in the lexicographic order is in the relation RA.
The encoding enc(A) is de ned as follows. We rst 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 de ne enc(A) := 0jAj 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 di erent orderings of the domain of A.
Let be a nite vocabulary. A Turing machine TM de nes a semi-decision algorithm for a class C of nite -models i there is an accepting run for TM on an input w 2 f0; 1g exactly when w is some encoding of some structure A 2 C. Proposition 2. In the nite, LRE can de ne exactly all recursively enumerable classes of models.
Proof. Let TM be a Turing machine that de nes a semi-decision algorithm for some class of models. It is routine to write a formula 'TM := IY 9X such that A j= 'TM if there exists an extension B of A that consist essentially of a copy of A and another part C that encodes the computation table of an accepting computation of TM on an input enc(A). We can use the predicates in 9X in order to de ne word models that encode enc(A) and other strings that correspond to the Turing machine tape at di erent stages of the computation. Symbols in 9X can also be used, inter alia, in order to de ne 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 9X of LRE, we can de ne a Turing machine that rst non-deterministically provides a number k 2 Z+ of fresh points to be added to the domain of the model considered, and then checks if 9X holds in the obtained larger model. tu
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 rst de ne a translation from dependence logic to D+. Ronnholm
considers a translation with similar intuitions in [
Let be a sentence of dependence logic over a vocabulary such that Y 62 . Let y; v; u; u0 be variables that do not occur in . We next de ne a translation TYy ( ) of into D+ by recursion on the structure of . (Strictly speaking, the variables v; u; u0 are xed parameters of the translation just like y and Y , so we should write T y;v;u;u0 ( ) instead of TY ( ). The issue here is only that when y
Y 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 T y
Y (:x = z) := :x = z 43.. TTYYyy ((Y=((xx)1); :::=:; xxk) ) y:=an=d(TxYy1;(::::Y; x(kx))) := xjy 5. TYy( (' ^ ) ) := ( (TYy(') ^ TYy( ) ) 6. TYy( (' _ ) ) := 9v v?z y ^ (TYy(') ^ v = u) _ (TYy( ) ^ v = u0) , where z contains exactly all variables quanti ed superordinate to (' _ ) in , i.e., exactly each x such that (' _ ) is in the scope of 9x or 8x. 7. Assume 9x ' is subordinate to a disjunction in , meaning that there is a subformula ( _ ) of and 9x ' is a subformula of ( _ ). We de ne TYy(9x ') := 9x x?z yv ^ TYy(') ; where z contains exactly all variables quanti ed superordinate to 9x ' in , with the exception that z never contains x; the exception is relevant if contains nested quanti cation of x. 8. Assume 9x ' is not subordinate to a disjunction in . Then TYy(9x ') := 9x x?z y ^ TYy(') ; where z contains exactly all variables quanti ed superordinate to 9x ' in , with the exception that z never contains x. 9. TYy(8x ') := 8x (TYy('))
Let A be a model such that jAj 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. 1. Call Z := Dom(U ). Z contains exactly all variables quanti ed superordinate to ' in . Dom(V ) is Z [ fy; u; u0g or Z [ fy; v; u; u0g; we have v 2 Dom(V ) i ' is subordinate to a disjunction in . 2. We have U = V Z, i.e., U = f s Z j s 2 V g, 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 2 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 di erent from that of u0.
When (U; V ) satis es 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 62 be a unary relation symbol. We let (B; P 7! T ) denote the expansion of B to the vocabulary [ fP g such that P B = T .
Let s be an assignment with domain X. Let fx1; :::; xkg be a nite set of variables. We let s fx1;:::;xkg denote the assignment s (X n fx1; :::; xkg). 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 (f;g; V ) be a suitable pair of for A, S, (y; v; u; u0) and ( ; ). Then we have A; Y 7! S ; f;g j= i A; V j= TYy ( ).
Proof. Prove by induction on the structure of that for any subformula ' of , the equivalence A; Y 7! S ; U j= ' , A; V j= TYy (') holds for all suitable pairs (U; V ) for A, S, (y; v; u; u0) and ('; ). tu
De ne TYy (') := 9u9u0 u 6= u0 ^ =(u) ^ =(u0) ^ TYy (') ): The following Lemma now follows directly.
Lemma 2. Let A be a model such that jAj 2. Let S A be a nonempty nite 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); f;g j= ' i A; f;g[S=y] j= TYy ('). tu
Proof. It is well known that every sentence of ESO translates to an equivalent
sentence # of dependence logic, see [
Let ' := IY 9X be a sentence of LRE , where is a rst-order sentence. The following chain of equivalences, where the penultimate equivalence follows by Lemma 2, settles the current theorem.
A j= ' ,
A + S; Y 7! S j= 9X , A + S; Y 7! S ; f;g j=
y , A + S; f;g[S=y] j= TY
y , A; f;g j= Iy TY
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 rst nondeterministically constructs a tuple n 2 (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 satis es ' with the given tuple n of cardinalites to be added
during the evaluation. TM is a semi-decision algorithm corresponding to '.
We have shown how the standard logics based on team semantics extend
naturally 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 quanti ers and generalized
atoms ([