INDEPENDENCE LOGIC AND ABSTRACT INDEPENDENCE RELATIONS 5 1 0 GIANLUCAPAOLINI 2 y a M Abstract. Wecontinuetheworkontherelationsbetweenindependencelogic and the model-theoretic analysis of independence, generalizing the results of 1 [16]totheframeworkofabstractindependencerelationsforanarbitraryAEC. 2 Wegiveamodel-theoreticinterpretationoftheindependenceatomandcharac- terizeunderwhichconditionswecanproveacompletenessresultwithrespect ] tothedeductivesystemthataxiomatizesindependenceinteamsemanticsand O statistics. L . h Contents t a 1. Introduction 1 m 2. Abstract Independence Relations 3 [ 2.1. Abstract Independence Relations in First-Order Theories 3 5 2.2. Abstract Independence Relations in Abstract Elementary Classes 4 v 3. Federation 6 7 3.1. Federated Pregeometries 7 0 3.2. Federated Sequences in Stable Theories 9 9 4. Independence Logic 10 6 . 4.1. Atomic Independence Logic 11 1 4.2. Abstract Independence Relation Atomic Independence Logic 13 0 5. Conclusion 20 4 1 References 20 : v i X r 1. Introduction a Inmathematicsandmodeltheorytheconceptsofdependenceandindependence areofcrucialimportance,itisinfactalwaysinfunctionofanindependencecalculus that a classificationtheory for a class of classes ofstructures is developed. For this reason,the notionsofdependence andindependence areobjectsofintense studyin the model-theoretic community. Three main frameworks in which (in)dependence has been studied are: pregeometries, first-order theories and abstract elementary classes (AECs). Table 1 lists the most important cases of (in)dependence studied in these contexts. The research of the author was supported by the Finnish Academy of Science and Letters (Vilho,Yrj¨oandKalleV¨ais¨al¨afoundation)andgrantTM-13-8847ofCIMO.Theauthorwouldlike tothankaboveallTapaniHyttinen,butalsoJohnBaldwin,˚AsaHirvonen,andJoukoV¨a¨an¨anen forusefulconversationsrelatedtothispaper. Theauthorwouldalsoliketothanktherefereefor hiscarefulreadingofthepaper,hiscorrectionsandhissuggestions. 1 2 GIANLUCAPAOLINI Recently, Va¨a¨n¨anen [20] developed a logical approach to the notions of depen- dence and independence, establishing a generaltheory of(in)dependence that goes under the name of dependence logic. Dependence logic provides an abstract char- acterization of (in)dependence, which accounts for the way dependence and inde- pendence behave in several disciplinary fields, e.g. database theory and statistics. Pregeometries Forking Indep. Indep. in AECs Vector ω-stable ℵ -stable 0 spaces theories homogeneous Alg. closed Stable Excellent fields theories classes Graphs Simple Finitary theories AECs Table 1. Independence in model theory In[16]thecasesof(in)dependenceoccurringinpregeometriesandω-stabletheo- rieswerealsoshownto be instances ofthis theory. We now generalizethese results to the other cases of independence listed in Table 1. We work in the framework of abstract independence relations for an arbitrary abstract elementary class, which subsumes most of the cases of independence of interest in model theory. Thekeyfeatureofthefamilyoflogicsstudiedindependencelogicisthepresence of logical atoms different from the equational one. Each kind of atom corresponds toadifferentnotionof(in)dependence,andeachlogicinthefamilyischaracterized bythelogicalatomspresentinthesyntax. Thismakesthestudyoftheatomiclevel of the (in)dependence logics of great relevance, as indeed this is the added layer of expressivity that these systems have at disposal. This study often results in the analysisofthe implicationproblemforasetofatomsofaparticularform. Thatis, the searchfor a complete deductive system for these atoms. Emblematic examples are the axiomatizations of functional dependence and stochastic independence due to Armstrong [2] and Geiger, Paz and Pearl[6], respectively. Our specific aim in this paper is the solution of the implication problem for the independence atom under a model-theoretic interpretation. This analysis was initiated in [16], where several (in)dependence atoms were shown to have natural model-theoretic counterparts. In the present study we deal exclusively with the independenceatom~x⊥~y and,onlymarginally,withitsconditionalversion~x⊥ ~y. ~z In Section 2 we set the stage, defining what is an abstract elementary class and what is the axiomatization of independence to which we refer. We also give the principalexamplesofindependence, amongwhichforking independenceinasimple theory,andpregeometric independence inanAECwithauniformpregeometricop- erator. InSection3weintroduceaparticularclassofindependencerelations,which wecallfederated. We showthatthesearea generalizationofthe wayindependence behave in vector spaces, algebraically closed fields, and abelian groups. We then focus on its pregeometric version, and show that any ω-homogenous non-trivial pregeometryis federated (modulo a finite localization). Thus, we use this result to deduce that in any first-order stable theory that admits non-trivial regular types forking independence is federated (over some set of parameters). In Section 4 we usethetheorydevelopedinSection3tocharacterizeunderwhichconditionswecan INDEPENDENCE LOGIC AND ABSTRACT INDEPENDENCE RELATIONS 3 prove a completeness result with respect to the deductive system that axiomatizes independence in team semantics and statistics, giving a complete answer to the motivating question of the paper. 2. Abstract Independence Relations To makeclearthe levelsofgeneralizationatwhichwe work,wefirstdefine what is anabstractindependence relationinthe contextoffirst-ordertheories,andthen generalize this definition to the context of abstract elementary classes. 2.1. Abstract Independence Relations in First-Order Theories Werefertotheframeworkof[3]and[1]. Wefixsomenotation. AB isshorthand forA∪B. Fora complete first-ordertheoryT,wedenote by Mits monstermodel. Definition 2.1. Let T be a complete theory and | a ternary relation between ⌣ (bounded) subsets of the monster model M. We say that | is a pre-independence ⌣ relation if it satisfies the following axioms. (a.) (Invariance) If A | B and f ∈Aut(M), then f(A) | f(B). ⌣C ⌣f(C) (b.) (Existence) A | B, for any A,B ⊆M. ⌣A (c.) (Monotonicity) If A | B and D ⊆A, then D | B. ⌣C ⌣C (d.) (Base Monotonicity) Let D ⊆C ⊆B. If A | B, then A | B. ⌣D ⌣C (e.) (Symmetry) If A | B, then B | A. ⌣C ⌣C (f.) (Transitivity) Let D ⊆C ⊆B. If B | A and C | A, then B | A. ⌣C ⌣D ⌣D (g.) (Normality) If A | B, then AC | B. ⌣C ⌣C (h.) (Finite Character) If A | B for all finite A ⊆A, then A | B. 0 ⌣C 0 ⌣C (i.) (Anti-Reflexivity) If A | A, then A | C for any C ⊆M. ⌣B ⌣B If in addition | satisfies the following two axioms, then we say that | is an ⌣ ⌣ independence relation. (j.) (Extension) If A | B and B ⊆ D, then there is f ∈ Aut(M) fixing BC ⌣C pointwise such that f(A) | D. ⌣C (k.) (Local Character) There is a cardinal κ(T) such that for every~a ∈ M<ω and B ⊆M there is C ⊆B with |C|<κ(T) and~a | B. ⌣C In this context we do not distinguish between finite sets and finite sequences. Thus, if A = {a ,...,a }, B = {b ,...,b } and C = {c ,...,c }, we may 0 n−1 0 m−1 0 k−1 write a ···a | b ···b instead of A | B. By Transitivity we will 0 n−1 ⌣c0···ck−1 0 m−1 ⌣C refer to the following (a-priori) stronger property. Proposition 2.2 (Transitivity). A | B andA | D ifandonlyifA | BD. ⌣C ⌣CB ⌣C Proof. For the direction (⇒), suppose that A | BD. We have that A | B by ⌣C ⌣C Monotonicity. Furthermore,bySymmetryandNormalitywehavethatA | BCD ⌣C and so, by Base Monotonicity, A | BCD. Thus, by Monotonicity, A | D. ⌣CB ⌣CB For the direction (⇐), suppose that A | B and A | D. By Symmetry, ⌣C ⌣CB B | A and D | A, so, by Normality, CB | A and DCB | A. Thus, ⌣C ⌣CB ⌣C ⌣CB by Transitivity (the axiom), DCB | A and so, by Monotonicity and Symmetry, ⌣C A | BD. ⌣C The following principle will be of crucial importance in Section 4. Corollary 2.3 (Exchange). If A | B and AB | C, then A | BC. ⌣D ⌣D ⌣D 4 GIANLUCAPAOLINI Proof. A | B and AB | C ⌣D ⌣D ⇓ A | B and C | AB ⌣D ⌣D ⇓ A | B and C | A [by Transitivity] ⌣D ⌣DB ⇓ A | B and A | C [by Symmetry] ⌣D ⌣DB ⇓ A | BC [by Transitivity]. ⌣D In the following two orthogonal examples (not generalizing each others), that cover a broad class of first-order theories. The second one is by far the most important example of independence that has ever been formulated, the original definition is due to Shelah [18]. Example 2.4 (Independence in o-minimal theories [17]). Let T be an o-minimal theory. For A,B,C ⊆ M, define A |acl C if for every ~a ∈ A we have that ⌣B dim (~a/B∪C)=dim (~a/B). Then |acl is a pre-independence relation. acl acl ⌣ Example 2.5 (Forking in simple theories [14]). Let T be a simple theory. For A,B,C ⊆ M, define A |f C if for every ~a ∈ A we have that tp(~a/B ∪C) is a ⌣B non-forking extension of tp(~a/B). Then |f is an independence relation. ⌣ 2.2. Abstract Independence Relations in Abstract Elementary Classes The axiomatization of independence that we gave in the previous section does not refer to any intrinsically first-order property, it thus makes sense to generalize it to the context of abstract elementary classes [19]. First of all we define what an abstract elementary class is and what are the analog of the first-order notions of amalgamationand joint embedding. Definition 2.6 (Abstract Elementary Class [19]). Let K be a class of structures in the signature L. We say that (K,4) is an abstract elementary class (AEC) if the following conditions are satisfied. (1) K and 4 are closed under isomorphism. (2) If A4B, then A⊆B. (3) The relation 4 is a partial order on K. (4) If (A ) is an increasing 4-chain, then: i i<δ (4.1) A ∈K; i<δ i S (4.2) for each j <δ, A 4 A ; j i<δ i S (4.3) if each A 4M, then A 4M. j i<δ i S (5) If A,B,C ∈K, A4C, B 4C and A⊆B, then A4B. (6) There is a Lo¨wenheim-Skolem number LS(K) such that if A∈K and B ⊆A, then there is A′ ∈K such that B ⊆A′, A′ 4A and |A′|=|B|+|L|+LS(K). Definition 2.7. If M,N ∈ K and f : M → N is an embedding such that f(M)4N, then we say that f is a 4-embedding. Let κ be a cardinal, we let K ={A∈K||A|=κ}. κ Definition 2.8. Let (K,4) be an AEC. INDEPENDENCE LOGIC AND ABSTRACT INDEPENDENCE RELATIONS 5 (i) Wesaythat(K,4)hastheamalgamationproperty(AP)ifforanyA,B ,B ∈ 0 1 K with A4B for i<2, there are C ∈K and 4-embeddings f :B →C for i i i i<2, such that f ↾A=f ↾A. 0 1 (ii) Wesaythat(K,4)hasthejointembeddingproperty(JEP)ifforanyB ,B ∈ 0 1 K there are C ∈K and 4-embeddings f :B →C for i<2. i i (iii) Wesaythat(K,4)hasarbitrarilylargemodels(ALM)ifforeveryκ>LS(K), K 6=∅. κ If (K,4) has AP, JEP and ALM, then, using the same technique as in the elementary case, we can build a monster model for (K,4). Consistent with the notation used for the elementary case, we denote this model by M. We are now in the position to generalize Definition 2.6 to the context of AECs. Also in this case we distinguish between pre-independence and independence relations. In our study we will work only at the level of pre-independence, but we consider worth mentioning what are (some of) the further axioms that are required in order to develop a classification theory for the AEC under examination. Definition 2.9. Let(K,4)beanAECwithAP,JEPandALM,and | aternary ⌣ relation between (bounded) subsets of the monster model M. We say that | is a ⌣ pre-independence relation if it satisfies the following axioms. (a.) (Invariance) If A | B and f ∈Aut(M), then f(A) | f(B). ⌣C ⌣f(C) (b.) (Existence) A | B, for any A,B ⊆M. ⌣A (c.) (Monotonicity) If A | B and D ⊆A, then D | B. ⌣C ⌣C (d.) (Base Monotonicity) Let D ⊆C ⊆B. If A | B, then A | B. ⌣D ⌣C (e.) (Symmetry) If A | B, then B | A. ⌣C ⌣C (f.) (Transitivity) Let D ⊆C ⊆B. If B | A and C | A, then B | A. ⌣C ⌣D ⌣D (g.) (Normality) If A | B, then AC | B. ⌣C ⌣C (h.) (Finite Character) If A | B for all finite A ⊆A, then A | B. 0 ⌣C 0 ⌣C (i.) (Anti-Reflexivity) If A | A, then A | C for any C ⊆M. ⌣B ⌣B If in addition | satisfies the following two axioms, then we say that | is an ⌣ ⌣ independence relation. (j.) (Extension) If A | B and B ⊆ D, then there is f ∈ Aut(M) fixing BC ⌣C pointwise such that f(A) | D. ⌣C (k.) (Local Character) There is a cardinal κ(K) such that for every~a∈M<ω and B ⊆M there is C ⊆B with |C|<κ(K) and~a | B. ⌣C Asintheprevioussection,byTransitivitywewillrefertothefollowing(a-priori) stronger property. Proposition2.10(Transitivity). A | BandA | DifandonlyifA | BD. ⌣C ⌣CB ⌣C Proof. As in Proposition 2.2. Corollary 2.11 (Exchange). If A | B and AB | C, then A | BC. ⌣D ⌣D ⌣D Proof. As in Corollary 2.3. IfT isacompletefirst-ordertheoryandwedenoteby4therelationofelementary substructure,thenthepair(Mod(T),4)isanAECwithAP,JEPandALM. Thus allthe cases ofindependence examinedin the previous sectionareinstances ofthis 6 GIANLUCAPAOLINI more general definition. Furthermore, the generality at which we work allow us to subsume also the non-elementary cases of independence. Example 2.12 (Independence in Pregeometries [8]). Let (K,4) be an AEC with AP, JEP and ALM, and cl : M → M a pregeometric operator. For A,B,C ⊆ M, define A |cl C if forevery~a∈A we havedim (~a/B∪C)=dim (~a/B). Then |cl ⌣B cl cl ⌣ is a pre-independence relation. Example2.13(HilbertSpaces). LetKbetheclassofHilbertSpacesoverR(resp. C)and4theclosedlinearsubspacerelation,then(K,4)isanAECwithAP,JEP and ALM. Given a closed linear subspace C ⊆M and a∈M, we denote by P (a) C the orthogonal projection of a onto C. For D,B ⊆M, we then say that D |ort B ⌣A if for every a ∈ D and b ∈ B we have PA⊥(a) ⊥ PA⊥(b). Then ⌣|ort is orthogonal over A for any A⊆M. Example 2.14 (Independence in Finitary AECs). See [12]. 3. Federation We introduce two fundamental notions: independent sequences and algebraic tuples. Independent sequences play a fundamental role in classification theory, where they often occur in the form of sequences of indiscernibles. Definition 3.1 (Independent Sequence). Let | be a pre-independence relation ⌣ and (I,<) a linear order. Let A ⊆ M and (a | i ∈ I) ∈ MI injective. We say i that (a | i ∈ I) is an | -independent sequence over A if for all j ∈ I, we have i ⌣ (a | i < j) | a . We say that (a | i ∈ I) is an | -independent sequence if it is i ⌣A j i ⌣ an | -independent sequence over ∅. ⌣ Definition3.2(AlgebraicTuple). Let | apre-independencerelation. Wesaythat ⌣ ~e∈M<ω is | -algebraic over A if~e | ~e. We say that~e∈M<ω is | -algebraic if ⌣ ⌣A ⌣ it is | -algebraic over ∅. ⌣ When it is clear to which pre-independence relation | we refer, we just talk of ⌣ independent sequences and algebraic tuples. Lemma 3.3. Let | be a pre-independence relation and (a | i ∈ I) ∈ MI an ⌣ i independent sequence over A. Then for all~a,~b ⊆ (a | i ∈ I) ∈ MI with~a∩~b = ∅ i we have~a | ~b. ⌣A Proof. It suffices to show that for~a = (a ,...,a ) and~b = (a ,...,a ) with k0 kn−1 j0 jm−1 k < ··· < k , j < ··· < j and~a∩~b = ∅, we have that~a | ~b. We prove 0 n−1 0 m−1 ⌣A this by induction on max(k ,j )=t. n−1 m−1 t=0. If this is the case,then either a=∅ or b=∅ because~a∩~b=∅. Suppose the first,theothercaseissymmetrical. ByExistenceA | b,andso,byMonotonicity, ⌣A ∅ | b. ⌣A t>0. Suppose that t=j , the other case is symmetrical. By the independence m−1 of the sequence and Monotonicity, it follows that a ···a b ···b | b . k0 kn−1 j0 jm−2 ⌣ jm−1 A Noticenowthatmax(k ,j )<tbecause~a∩~b=∅,thus by inductionhypoth- n−1 m−2 esis we have that a ···a | b ···b . k0 kn−1 ⌣ j0 jm−2 A INDEPENDENCE LOGIC AND ABSTRACT INDEPENDENCE RELATIONS 7 Hence by Exchange we can conclude that a ···a | b ···b . k0 kn−1 ⌣ j0 jm−1 A Corollary 3.4. Let | be a pre-independence relation and (a | i ∈ I) ∈ MI ⌣ i be an independent sequence over A, then for every ~a ⊆ (a | i ∈ I), we have i ~a | (a |i∈I)−~a. ⌣A i Proof. Follows from Lemma 3.3 by Finite Character. We define the notion of federation. This notion is a generalizationof the notion of federated pregeometry introduced in [4]. For an independent sequence to be federated we ask the existence of a point which is dependent from all the members of the sequence, but independent from all but one. It can be thought as a strong form of independence. We denote by ω∗ the set ω−{0}. Definition 3.5 (Federation). Let | be a pre-independence relation, n ∈ ω∗ and ⌣ (a |i < n) ∈ Mn an independent sequence over A. We say that (a |i < n) is i i federated over A if there exists d∈M such that d6| a ···a and d | (a |i<n)−a for every j <n. ⌣ 0 n−1 ⌣ i j A A We say that (a |i<n) is federated if it is federated over ∅. For (a |i<ω)∈Mω i i independent (over A), we say that (a |i<ω) is federated (over A) if (a |i<n) is i i federated (over A) for every n∈ω∗. Definition 3.6. Let | be apre-independencerelationandA⊆M. We define the ⌣ index of federation of | over A, in symbols IF( | ;A), as ⌣ ⌣ sup{n∈ω∗| there is (a |i<n)∈Mn federated over A}. i We say that | is federated over A if IF( | ;A)=ω. We say that | is federated if ⌣ ⌣ ⌣ it is federated over ∅. Clearly, the easiest way to show that a particular pre-independence relation is federated is to find a federated sequence of length ω in the monster model. This will be our way to establish the federation of a pre-independence relation. 3.1. Federated Pregeometries In the following three important examples of federated independent relations. Example 3.7 (Vector spaces [16]). Let VSinf denote the theory of infinite vector K spaces over a fixed field K. Let hi : M → M be such that A 7→ hAi, i.e. the linear span of A, then hi is a pregeometric operator. Notice that the theory VSinf K is superstable (if K is countable it actually is ω-stable)and stronglyminimal. Fur- thermore,the spanoperatorcoincides with the algebraicclosureoperator. Thus in this case we have that |hi= |acl= |f . Let A⊆M be such that dim(A)=ℵ and ⌣ ⌣ ⌣ 0 let(a |i∈ω)beaninjectiveenumerationofabasisB forAinM,then(a |i∈ω) i i is a federated sequence. Notice that 0∈M is an algebraic point. 8 GIANLUCAPAOLINI Example 3.8 (Algebraically closed fields [16]). Let ACF denote the theory of p algebraically closed fields of characteristic p, where p is either 0 or a prime. Let acl:M→Mbe suchthat A7→acl(A), i.e. the algebraicclosureof A, then aclis a pregeometric operator. Notice that the theory ACF is ω-stable and, furthermore, p it is strongly minimal, thus in this case we have that |acl= |f . Let A ⊆ M be ⌣ ⌣ such that dim(A) = ℵ and let (a | i ∈ ω) be an injective enumeration of a basis 0 i B for A in K, then (a |i∈ω) is a federated sequence. Notice that any member of i the prime field of M is an algebraic point. Example 3.9 (Abelian groups). Let K be the class of abelian groups. Given G,H ∈ K we say that G is a pure subgroup of H if G is a subgroup of H and for every g ∈ G and n < ω, the equation nx = g is solvable in G, whenever it is solvable in H. Let 4 be the pure subgroup relation, then the class (K,4 ) pure pure is an AEC with AP, JEP and ALM. Let hi :M→M be such that A7→hAi = P P {b∈M|∃n∈ω∗ with nb∈hAi}, i.e. the pure subgroup generated by A, then hi is a pregeometric operator. Let A ⊆ M be such that dim(A) = ℵ and let P 0 (a | i ∈ ω) be an injective enumeration of a basis B for A in M, then (a | i ∈ ω) i i is a federated sequence. Notice that 0∈M is an algebraic point. The three examples above are instances of a generalpregeometric phenomenon, namely federation. This is the notion consideredin [4], which we generalizedto an arbitrary pre-independence relation. Definition 3.10 (Federated Pregeometry). Let (X,cl) be a pregeometry. We say that the pregeometry is federated if for every independent D ⊆ X, cl(D ) 6= 0 ω 0 cl(D). SD(D0 In infinite dimensional federated pregeometries we can always find federated sequences of length ω. Example3.11. Let(K,4)beanAECwithAP,JEPandALM,andcl:M→Ma pregeometricoperatorsuchthatitdeterminesafederatedpregeometry. LetA⊆M be such that dim(A) = ℵ , and (a | i ∈ ω) an injective enumeration of a basis B 0 i for A in M, then (a | i ∈ ω) is a federated sequence. Notice that if there exists i e∈cl(∅), then e is an algebraic point. We conclude this sectionwith animportant characterizationof federated prege- ometries. Definition 3.12. Let (X,cl) be a pregeometry. i) We say that (X,cl) is trivial if cl(A)= cl({a}) for every A⊆X. Sa∈A ii) We saythat(X,cl)isω-homogeneousifforeveryA⊆ X anda,b∈X−cl(A) ω there is f ∈Aut((X,cl)/A) such that f(a)=b. Clearly federated pregeometries are non-trivial, more interestingly under the assumption of ω-homogeneity we also have the following partial converse. Theorem 3.131 (Hyttinen). Let (X,cl) be an ω-homogeneous pregeometry. If (X,cl) is non-trivial, then there exists A ⊆ X such that (X,cl ) is federated. 0 ω A0 1Thistheorem isduetoTapani Hyttinen. Theproofisgivenwithhispermission. INDEPENDENCE LOGIC AND ABSTRACT INDEPENDENCE RELATIONS 9 Proof. Suppose that (X,cl) is non-trivial, then there is A⊆X such that d∈cl(A) but d∈/ cl({a}). By Finite Character, there is A∗∗ ⊆ A, such that Sa∈A ω (⋆) d∈cl(A∗∗) but d∈/ cl({a}). [ a∈A∗∗ Let A∗ = {a ,...,a } ⊆ A∗∗ be of minimal cardinality with respect to property 0 n−1 (⋆), then we must have that d∈cl({a ,...,a }), but 0 n−1 d∈/ cl({a ,...,a }∪{a }) and d∈/ cl({a ,...,a }∪{a }). 0 n−3 n−2 0 n−3 n−1 Let A ={a ,...,a }, we claim that (X,cl ) is federated. For ease of notation, 0 0 n−3 A0 for a,b ∈ X instead of cl({a,b}) we just write cl(a,b), and analogously for single- tons. Let D ={d ,...,d } be independent in (X,cl ). By induction on m we 0 0 m−1 A0 construct d∗,...,d∗ ∈X such that for i<m−1: 0 m−1 i) d∗ ∈/ cl (d ) and d ∈/ cl (d∗); i A0 i+1 i+1 A0 i and, for 16i<m: ii) d∗ ∈cl (d∗ ,d )−(cl (d∗ )∪cl (d )); i A0 i−1 i A0 i−1 A0 i iii) d∗ ∈cl (d∗,d )−(cl (d∗)∪cl (d )); i−1 A0 i i A0 i A0 i iv) d ∈cl (d∗ ,d∗)−(cl (d∗ )∪cl (d∗)). i A0 i−1 i A0 i−1 A0 i By properties ii) - iv) it will then be clear that d∗ ∈ D − cl(D), as wanted. We start the construction. Let d∗ = d .m−S1uppos0e thSenD(thDa0t we have 0 0 defined d∗, we want to define d∗ . We notice the following: i i+1 1) a ∈/ cl (∅) and d∗ ∈/ cl (∅); n−2 A0 i A0 2) a ∈/ cl (a ) and d ∈/ cl (d∗); n−1 A0 n−2 i+1 A0 i 3) d∈cl (a ,a )−(cl (a )∪cl (a )). A0 n−1 n−2 A0 n−2 A0 n−1 Because of ω-homogeneity and 1) we can find f ∈ Aut((X,cl)/A ) such that 1 0 f (a ) = d∗. But then by 2) we have f (a ) ∈/ (cl (d∗)), and so again 1 n−2 i 1 n−1 A0 i by ω-homogeneity we can find f ∈Aut((X,cl)/A ∪{d∗}) such that 2 0 i a 7−f→1 d∗ 7−f→2 d∗ n−2 i i a 7−f→1 f (a )7−f→2 d . n−1 1 n−1 i+1 Let d∗ = f (f (d)). We show that d∗ has properties i) - iv). Property ii) i+1 2 1 i+1 is clear from 3), and properties iii) and iv) follow from ii) by Exchange. Re- garding property i), if i = m−1 there is nothing to prove. Suppose then that i < m − 1. If d ∈ cl (d∗ ), then d ∈ cl ({d |j <i+2}), because i+2 A0 i+1 i+2 A0 j d∗ ∈ cl ({d |j <i+2}), hence we contradict the independence of D . Fi- i+1 A0 j 0 nally, suppose that d∗ ∈cl (d ). By the already proved ii) for i+1 it follows i+1 A0 i+2 in particular that d∗ ∈/ cl (∅), hence by Exchange d ∈ cl (d∗ ), and so we i+1 A0 i+2 A0 i+1 are in the case just considered, which leads to a contradiction. 3.2. Federated Sequences in Stable Theories2 We are driven by the following questions. Question 3.14. Let G be an ω-stable (resp. superstable and stable) group. Can we find |f -federated sequences in the monster model for Th(G)? Under which ⌣ conditions is an |f -independent sequence a |f -federated sequence? ⌣ ⌣ 2Theauthor wouldliketothankTapaniHyttinenforthehelpinthewritingofthissection. 10 GIANLUCAPAOLINI Question 3.15. Are there known classes of theories in which we can always find |f -federated sequences? Under which conditions can we find |f -federated se- ⌣ ⌣ quences in the stability-theoretic classes of theories, e.g. classifiable or stable? We give a complete answer to Question 3.14 and a partial answer to Ques- tion 3.15. Proposition 3.16. Let G be a stable group,then in the monster model for Th(G) we can find a |f -federated sequence. In fact, any |f -independent sequence of ⌣ ⌣ generic elements is federated. Proof. Let (a |i ∈ ω) be such that a realizes a generic type over (a |j < i), for i i j every i<ω. Then for every n∈ω∗ we have that f f a 6| a ···a and a | (a |i<n)−a for every j <n. X i⌣ 0 n−1 X i ⌣ i j i<n ∅ i<n ∅ Theorem 3.17. Let T be a stable theory, A ⊆ M, p ∈ S (A) a regular type and n X ⊆ Mn the set of realizations of p in M. Then on X the forking dependence relation determines an infinite dimensional ω-homogenous pregeometry (X,clf). Proof. See for example [3]. From Theorems 3.13 and 3.17 it follows directly the following corollary, which ensures that if the theory admits non-trivialregular types then we can always find federated sequences (over some set of parameters). Corollary 3.18. Let T be a stable theory, A⊆ M, p ∈ S (A) a regular type and 1 X ⊆M the set of realizationsof p in M. If (X,clf) is non-trivial,then we can find A ⊆ X and (a |i ∈ ω) ∈ Xω such that (a |i ∈ ω) is a |f -federated sequence 0 ω i i ⌣ over A∪A . 0 Proof. By Theorem 3.13 there is A ⊆ X such that (X,cl ) is federated. Notice 0 ω A0 that the pregeometry (X,cl ) is also infinite dimensional. Let (a |i ∈ ω) be an A0 i enumeration of the fist ω elements in a basis B for (X,cl ). Then (a |i∈ω) is a A0 i |f -federated sequence over A∪A . ⌣ 0 4. Independence Logic We now enter in the dependence logic component of the paper. In the first sectionwe describe how the independence atomis characterizedin team semantics andstudyitsaxiomatization. Teamsemanticsisanewsemantictoolintroducedin [11] and then developed in [20], which is based on the idea of giving semantics to logiclanguagesbymeansofsetsofassignmentsinsteadofsingleassignments. Inthe secondsectionweinterprettheindependenceatomas | andstudytheimplication ⌣ problemfortheresultingsystem. Noticethatallthelogicsystemsdescribedinthis paper have an atomic language, with no connectives and no quantifiers. It may alsobe worthnoticing that the atomic systems describedin Section 4.1 are part of a wider logic language with actual logical operations ∧,∨,¬,∃,∀. For details see [20]. In the case of the systems described in Section 4.2, is it not yet clear what