{'fraction_non_alphanumeric': 0.06186636123020725, 'fraction_numerical': 0.007506926494033154, 'mean_word_length': 3.709724449628226, 'pattern_counts': {'":': 1, '<': 2, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 26, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Characterizing counterfactuals and dependencies over causal and generalized causal teams

We analyze the causal-observational languages that were introduced in Barbero and Sandu (2018), which allow discussing interventionist counterfactuals and functional dependencies in a unified framework. In particular, we systematically investigate the expressive power of these languages in causal team semantics, and we provide complete natural deduction calculi for each language. Furthermore, we introduce a generalized semantics which allows representing uncertainty about the causal laws, and analyze the expressive power and proof theory of the causal-observational languages over this enriched semantics.


Introduction
Counterfactual conditionals express the modality of irreality: they describe what would or might be the case in circumstances that diverge from the actual state of affairs. Pinning down the exact meaning and logic of counterfactual statements has been the subject of a large literature (see e.g. [24] for a survey). We are interested here in a special case: the interventionist counterfactuals, which emerged from the literature on causal inference ( [23,20,18,28]). Under this reading, a conditional X = x ψ expresses that ψ would hold if we were to intervene on the given system, by subtracting the variables X to their current causal mechanisms and forcing them to take the values x.
The logic of interventionist counterfactuals has been mainly studied in the semantic context of deterministic causal models ([12, 17, 7, 32]), which consist of an assignment of values to variables together with a system of structural equations that describe the causal connections among variables. In [3], causal models were generalized to causal teams, in the spirit of team semantics ( [19,26]), by considering a set of assignments (a "team") instead of a single assignment. This opens the possibility of describing e.g. uncertainty, observations, and dependencies ( [26,11,15,13,27,30,14,3,4]). In this paper we also consider a further generalization of causal team semantics. While causal teams only allow describing uncertainty about the current state of the variables (the assignment), their generalized version also encode uncertainty about the causal laws.
One of the main reasons for introducing causal teams was the possibility of comparing, within a unified semantic framework, the logic of dependencies of causal nature (those definable in terms of interventionist counterfactuals) against that of contingent dependencies (those that occur e.g. in sets of empirical data, and which have been thoroughly studied in the literature on team semantics). In the context of team semantics the most commonly studied type of contingent dependency is functional determinacy, which is represented by the so-called dependence atoms =(X; Y), whose intended meaning is that the values of the variables in X determine the value of Y. More precisely, this means that assignments in the team which agree over X also agree over Y. On the causal side, there is a large variety of notions of causal dependence; see for example [28] for a taxonomy of the most common ones. A notable example is the notion of direct cause. A variable X is a direct cause of another variable Y if there is a way of manipulating X, while holding fixed all variables distinct from Y, so that the value of Y will change. This can be made precise and expressed as a boolean combination of counterfactuals: where Z is the set of all variables distinct from X and Y, and the disjunction ranges over the possible values of z, x, x ′ , y, y ′ (with x x ′ , y y ′ ). [4] provided a complete axiomatization for a language CO which describes causal dependencies (but no contingent dependencies) 1 ; the resulting logic is a fragment of the system given by Briggs in [7]. More generally, [3] and [4] give anecdotal evidence of the interactions between the two types of dependence, but offer no complete axiomatizations for languages that also involve contingent dependencies. In this paper we fill this gap in the literature by providing complete deduction systems (in natural deduction style) for the languages COD and CO \\/ (from [3]), which enrich the basic counterfactual language, respectively, with atoms of functional dependence =(X; Y), or with the global disjunction \\/ (in terms of which functional dependence is definable). We also give semantical characterizations, for COD, CO \\/ and the basic counterfactual language CO, in terms of definability of classes of causal teams.
All these results will also be extended to the generalized causal team semantics. We point out that the methods developed in the literature ( [9,30]) for proving completeness results in team semantics can be smoothly adapted to this generalized semantics, whereas these methods do not directly apply to the basic causal team semantics. The technical hindrance here is the fact that it is not always possible to define reasonably the union of two causal teams; this leads to the failure of the disjunction property for \\/ , which is a crucial element for the methods of [9,30]. In order to obtain, nonetheless, completeness results over causal team semantics, our strategy is to add to the systems for the generalized semantics further rules or axioms that characterize the property of being a causal team (i.e. of encoding certainty about the causal connections), or more precisely, the property of being a uniform team (as the languages we consider cannot tell apart causal teams from uniform teams).
The paper is organized as follows. Section 2 introduces the formal languages and two versions of causal team semantics. Section 3 deepens the discussion of the functions which describe causal mechanisms, addressing issues of definability and the treatment of dummy arguments. Section 4 characterizes semantically the language CO and reformulates in natural deduction form the CO calculi that come from [4]. An interesting simple consequence of the semantical analysis is a proof that the counterfactual is not definable in terms of the remaining operators. Section 5 gives semantical characterizations for COD and CO \\/ , and complete natural deduction calculi for both types of semantics. We conclude the paper in Section 6. An early version of this paper has already appeared as [6] in conference proceedings.

Formal languages
In this paper, we consider three classes of causal languages, which were originally introduced in [3]. Each of the causal languages is parametrized by a signature σ, which is a pair σ = (Dom, Ran) with Dom being a nonempty finite set of variables, and Ran a function that associates to each variable X ∈ Dom a nonempty finite set Ran(X) (called the range of X) of constant symbols or values x. 2 Throughout the paper we use the Greek letter σ to denote an arbitrary signature.
A boldface capital letter X stands for a sequence X 1 , . . . , X n of variables; similarly, a boldface lower case letter x stands for a sequence x 1 , . . . , x n of values. We will sometimes abuse notation and treat X and x also as sets. We abbreviate the conjunction of equalities X 1 = x 1 ∧· · · ∧ X n = x n as X = x, where we always assume that x i ∈ Ran(X i ), and also call X = x an equality (over σ). We write Ran(X) for Ran(X 1 ) × · · · × Ran(X n ).
Given a signature σ = (Dom, Ran), formulas of our basic languages CO[σ] are formed according to the grammar: where X ∪ {X} ⊆ Dom, x ∈ Ran(X), x ∈ Ran(X). 3 The connective is used to form in-terventionist counterfactuals, a peculiar type of conditional formula. Following the literature on team semantics, we also call the disjunction ∨ tensor disjunction. Throughout the paper, we reserve the first letters of the Greek alphabet, α and β for CO [σ] formulas. We also consider two extensions of CO[σ], obtained by adding the global disjunction \\/ , or dependence atoms =(X; Y): where X ∪ {X, Y} ⊆ Dom, x ∈ Ran(X), x ∈ Ran(X), α ∈ CO [σ]. According to our syntax, negation is allowed to occur only in front of CO[σ]-formulas α. 4 This syntax for negation is more liberal than that in [3], where formulas are assumed to be always in negation normal form.

Team semantics over causal teams
We study two variants of team semantics for the three causal languages. In this section, we review (with some modifications) the causal team semantics from [4].
An assignment over a signature σ = (Dom, Ran) is a map s : Dom → X∈Dom Ran(X) such that s(X) ∈ Ran(X) for every X ∈ Dom. Denote by A σ the set of all assignments over σ. A (non-causal) team T − over σ is a set of assignments over σ, i.e., T − ⊆ A σ . The reason for our choice of the notation T − instead of T will become clear later in this section. The team T − clearly respects the ranges of the variables, as, e.g., s 2 (Z) = 6 ∈ Ran(Z). We can represent the team T − as a table: The first row of the table represents the assignment s 1 and the second row represents s 2 in the obvious manner. For instance, the table cell with the number "6" represents the fact that s 2 (Z) = 6, and so on.
A system of functions F over σ is a function that assigns to each variable V in a domain En(F ) ⊆ Dom a set PA F V ⊆ Dom \ {V} of parents of V, and a function F V : Ran(PA F V ) → Ran(V). 5 Variables in the set En(F ) are called endogenous variables of F , and variables in Ex(F ) = Dom \ En(F ) are called exogenous variables of F .
Denote by F σ the set of all systems of functions over σ, which is clearly finite. Any system of functions F ∈ F σ can be naturally associated with a (directed) graph Example 2.2. Consider the system of functions F (over the signature σ from Example 2.1) described by the following graph G F and system of equations: We say that an assignment s ∈ A σ is compatible with a system of functions F ∈ F σ if for all endogenous variables V ∈ En(F ), where all assignments s ∈ T − are compatible with the function component F .
In particular, a pair T = (∅, F ) with the team component being the empty set ∅ is also a causal team. For simplicity, over the same signature σ, we identify all teams with the empty team component and different function components, namely we stipulate 5 We identify the set PA F V with a sequence, in a fixed lexicographical ordering.
The graph of a causal team T is defined as the graph associated to its function component; we denote it as G T . We call T recursive if G T is acyclic. We stipulate that the empty causal team is recursive. Throughout this paper, we will only consider recursive causal teams. The reasons behind this choice are many. First of all, the recursive case might be of greater philosophical importance, as it is sometimes claimed that only the recursive systems of functions admit a causal interpretation (see e.g. [25] for a discussion). Secondly, the logic of counterfactuals in the general case is much more complex than in the recursive case (see [17]) and it requires a separate treatment. 6 Intuitively, a causal team T may be seen as representing an assumption concerning the causal relationships among the variables in Dom (as encoded in F ) together with a range of hypotheses concerning the actual state of the system (as encoded in T − ).
Example 2.4. We now combine the (non-causal) team T − from Example 2.1 and the system F of functions from Example 2.2 into a causal team T = (T − , F ), as illustrated in the following diagram: It is easy to verify that all assignments in the team component T − are compatible with the function component F , e.g., The arrows in the upper part of the table represent the graph G T of the causal team T , which is defined as G F . As demonstrated in Example 2.2, the graph G T contains no cycles, thus the causal team T is recursive. Definition 2.5. Let S = (S − , G) and T = (T − , F ) be causal teams over the same signature σ. We call S a causal subteam of T , denoted as S ⊆ T , if S − ⊆ T − and G = F . We stipulate that the empty causal team ∅ over σ is a causal subteam of any causal team T over σ, i.e., ∅ ⊆ T .
An equality X = x (i.e., X 1 = x 1 ∧ · · · ∧ X n = x n ) is said to be inconsistent if it contains two conjuncts X = x and X = x ′ with distinct values x, x ′ ; otherwise it is said to be consistent. For a sequence X = X 1 , . . . , X n of variables and an assignment s, we write s(X) for s(X 1 ), . . . , s(X n ) . Definition 2.6 (Intervention). Let T = (T − , F ) be a causal team over some signature σ = (Dom, Ran). Let X = x (= X 1 = x 1 ∧ · · · ∧ X n = x n ) be a consistent equality over σ. The intervention do(X = x) on T is the procedure that generates a new causal team T X=x = (T − X=x , F X=x ) over σ defined as follows: -F X=x is the restriction of F to En(F ) \ X, that is, the system of functions that assigns to each variable V ∈ En(F ) \ X the set of parents PA F V and the function F V as prescribed by F ; The endogenous variable X of the original team T becomes exogenous in the new team T X=1 , and the equation F X (U) = U for X is now removed. The new team component T − X=1 is obtained by the rewriting procedure illustrated below: In the first step, rewrite the X-column with value 1. Then, update (recursively) the other columns using the functions from F X=1 . In this step, only the columns that correspond to "descendants" of X will be modified, and the order in which these columns should be updated is completely determined by the (acyclic) graph G T X=1 of T X=1 . Since the variable X becomes exogenous after the intervention, all arrows pointing to X have to be removed; in this case, the arrow from U to X. We refer the reader to [4] for more details and a proof of termination for this rewriting procedure. -T | = X = x iff for all s ∈ T − , s(X) = x. 7 7 Note once more that the symbol x is used as both a syntactical and a semantical object.
As usual, define ⊥ : We write T | = Γ and say that "T satisfies Γ" if T | = ϕ for each ϕ ∈ Γ. As usual, we can define semantic entailment in terms of satisfaction. For any fixed signature σ, we write that Γ | = c ϕ (or simply Γ | = ϕ whenever there is no risk of ambiguity) if every (recursive) causal team T of signature σ that satisfies Γ also satisfies ϕ. We say that ϕ and ψ are equivalent, denoted as ϕ ≡ c ψ (or simply ϕ ≡ ψ) if ϕ | = c ψ and ψ | = c ϕ.
We write a dependence atom =(; Y) with an empty first component as =(Y). Clearly, the semantic clause for =(Y) reduces to: Intuitively, the atom =(Y) states that Y has a constant value in the team and is thus called a constancy atom. In the context of finite signatures -i.e. allowing only finite domains and ranges, as is done throughout this paper -the dependence atoms are definable in terms of the constancy atoms, because of the following equivalence: Furthermore, in CO \\/ [σ], the finitude of σ makes the constancy atoms definable: Thus, by (1) and (2), the dependence atoms themselves are definable in CO \\/ [σ].
Recall that counterfactuals X = x ϕ express that ϕ holds after an intervention. In [3,4], another conditional operator ⊃ called the selective implication also plays an important role. The selective implication α ⊃ ϕ (always with a CO-formula α in the antecedent) expresses that ϕ holds after observing a fact described by α. Its semantics is defined as: It is easy to verify that α ⊃ ϕ ≡ ¬α ∨ ϕ in the languages considered in this paper. 8 We thus treat the selective implication α ⊃ ϕ as a shorthand in our logics. The selective implication generalizes material implication in the sense that it behaves in the same way on singleton causal teams; i.e., The team T X=1 consists only of the assignment in the second row of the table for T , on which Y = 2 holds; so we have that T | = X = 1 ⊃ Y = 2.

Team semantics over generalized causal teams
Causal team semantics was developed in order to support the introduction of counterfactuals and observations within the framework of team semantics. When we look at one of the main interpretations of teams -as a representation of uncertainty among possible states of affairs -we see an asymmetry: causal teams encode uncertainty about the state of the variables, and certainty about the causal laws. Yet, in all sciences the knowledge of the laws of causation may be as uncertain -if not more uncertain -than the knowledge of factual matters. [3] proposed to model uncertainty about causal laws by using the more general partially defined causal teams. In this section we introduce a more general and at the same time simpler approach: the generalized causal teams.
Given a signature σ, we write The pairs (s, F ) ∈ S Ñ σ can be easily identified with the deterministic causal models (also known as deterministic structural equation models) that are considered in the literature on causal inference ( [23], [20], etc.). Even though they are distinct mathematical objects, it is natural to identify a causal team T = (T − , F ) with the set Intuitively, a generalized causal team encodes uncertainty about which causal model governs the variables in Dom -i.e., uncertainty both on the values of the variables and on the laws that determine them. Distinct elements (s, F ), (t, G) of the same generalized causal team may also disagree on what is the set of endogenous variables, or on whether the system is recursive or not. A generalized causal team is said to be recursive if, for each pair (s, F ) in the team, the associated graph G F is recursive. In this paper we only consider recursive generalized causal teams.
The first element (s, F ) differs from the second one (s, G) in its function component (as F G). Since both F and G are recursive, the generalized causal team T is recursive.
The above is a toy example that illustrates the content of a generalized causal team and its graphical presentation. Let us now discuss some possible applications of generalized causal teams as representation tools. Consider a situation in which we have observational data about some phenomenon. It is very common to organize the data in the form of a database or a table. When we are uncertain among alternative causal explanations F 1 , . . . , F n that might have produced these data, we may represent the situation by a generalized causal team that contains causal models (s, F 1 ), . . . , (s, F n ) for each distinct entry s of the original database. 9 In the worst case, we may be completely clueless about the causal explanations, and thus our generalized causal team will include a causal model (s, F ) for each system of functions F compatible with all entries from the original database. More commonly, we are not completely ignorant about the causal explanations. Let us consider three possible types of situations of this kind.

In the first case, we know what causes what, and what does not -in other words, we
are certain about what the causal graph G is -but we have no quantitative description of the laws. This can be represented in a generalized causal team by including copies of the entries for each system of functions that agrees with the causal dependencies encoded in G. 10 In the second case, the data arises from the observation of different individuals that may be of different types, and are thus bound to react differently to a possible intervention. Our uncertainty about these types and how the individual will be affected by interventions may be represented by associating multiple function components to an individual. In other words, we can use the generalized causal teams to represent the dispositions of objects, such as the property of being flammable (in some circumstances) or not. In the third case, we may use generalized causal teams to represent our partial knowledge about a causal law. This corresponds to the scenarios in which we can predict reasonably the behaviour of a physical system only within certain ranges for the values of the variables. For example, we know that if we heat the gas in a balloon, its volume will increase linearly (by Charles' law), but not if we raise its temperature by 5000 • C (the balloon will melt at this temperature). The generalized causal team for this situation will include every system of (total) functions that agree with the known partial law within the "safe" range of values. 11 Let us now come back to the formal theory. We have already mentioned that a causal team T = (T − , F ) can be identified with the generalized causal team We stipulate that the empty generalized causal team ∅ corresponds to the empty causal team ∅, i.e., ∅ c = ∅. In particular, a singleton generalized causal team {(s, F )} corresponds to a singleton causal team ({s}, F ). Applying a (consistent) intervention do(X = x) on the causal team ({s}, F ) generates a causal team ({s F X=x }, F X=x ) as specified in Definition 2.6. We can then define the result of the intervention do(X = x) on the generalized causal team {(s, F )} to be the generalized causal team ( Interventions on arbitrary generalized causal teams are defined as follows. Definition 2.12 (Intervention over generalized causal teams). Let T be a (recursive) generalized causal team, and X = x a consistent equality over σ. The intervention do(X = x) on T generates the generalized causal team Example 2.13. Consider the generalized causal team T from Example 2.11. The intervention do(Y = 1) is computed analogously as it would be done on a causal team, except that in this case the entries in each row must be updated according to the function component corresponding to the row. The team T X=x after the intervention is as follows: The function components are F Y=1 = F and G Y=1 = G, since Y is exogenous for both F and G. Since Y is not a parent of any endogenous variable of F , the values of other variables in the first row remain unchanged after the intervention.
Definition 2.14. Let ϕ be a formula of the language CO \\/ [σ] or COD[σ], and let T be a generalized causal team over σ. The satisfaction relation T | = g ϕ (or simply T | = ϕ) over generalized causal teams is defined in the same way as in Definition 2.8, except for slight differences in the following clause: For any fixed σ, we also write Γ | = g ϕ (or simply Γ | = ϕ) if all (recursive) generalized causal teams of signature σ that satisfy Γ also satisfy ϕ; and ϕ ≡ g ψ (or simply ϕ ≡ ψ) if ϕ | = g ψ and ψ | = g ϕ.
In the next theorem we list some closure properties for our logics over both causal teams and generalized causal teams. The proof is left to the reader, or see [4] for the causal team case. In addition, CO[σ]-formulas α are closed under unions: The empty team property, downward closure and union closure together are equivalent to the flatness property, which CO[σ]-formulas satisfy: The next lemma shows that the team semantics over causal teams and that over generalized causal teams with a constant function component are essentially equivalent.
(ii) For any generalized causal team T with a unique function component, we have Proof.. Both items are proved by straightforward induction.
Proof.. Assume ∆ | = c α, and let T be a generalized causal team such that T | = g ∆. If T = ∅, by the empty team property we have T | = α, and we are done. Otherwise observe that, by the flatness of ∆, The converse direction is proved analogously.

Characterizing function components
As is common in the literature on causation, our formal languages only talk of variables and values; they do not explicitly mention the causal laws nor the functions that describe them. In order to understand the expressive power of these languages, we need to first understand to what extent they allow an implicit description of the laws. In this section we will answer to this question; the answer is: to a great extent. In the following subsection we begin addressing the aspects of the functional laws that cannot be described by our languages.

Equivalence of function components
Consider a binary function f and a quaternary function g defined as f (X, ). Essentially f and g are the same function: Z 1 , Z 2 are dummy arguments of g. In some formal presentations of causal reasoning, the distinction between f and g is quotiented out. We preferred to maintain this distinction in the present paper, following the approaches in [7,3,4]. This type of distinction might be needed in case the framework is applied to realistic scenarios. Given a complex description of a function, it might be unfeasible to check whether some of its arguments are dummy in case the variable ranges are large. On the other hand, however, this additional degree of generality brings with it a burden of bookkeeping, which we now address.
First of all, we define formally what it means for two functions (and more generally, two function components) to be equivalent up to dummy arguments. -Let V ∈ Dom. The two functions F V and G V are said to be equivalent up to dummy arguments, denoted as (where we assume w.l.o.g. the shown orderings of the arguments of the functions).
-Let Cn(F ) denote the set of endogenous variables V of F for which F V is a constant function, i.e., for some fixed c ∈ Ran(V), It is easy to see that ∼ is an equivalence relation. Furthermore, the relation ∼ is preserved under interventions.
We now generalize the equivalence relation ∼ to the causal team level. Two nonempty causal teams T = (T − , F ) and S = (S − , G) of the same signature σ are said to be similar, denoted as T ∼ S , if F ∼ G; equivalent, denoted as T ≈ S , if T ∼ S and T − = S − . This definition of equivalence is meant to describe, semantically, the conditions under which S and T cannot be distinguished by our formal languages.
Let us now define equivalence also for generalized causal teams. For any generalized causal team T , write Two generalized causal teams S and T are said to be equivalent, denoted as Moreover, we define the equivalence relation ≈ between elements of S Ñ σ by We now show that formulas in the logics we consider in this paper are invariant under causal equivalence. In other words, none of our languages can distinguish causal teams which are equivalent up to dummy arguments. Proof.. The theorem is proved by induction on ϕ. The case ϕ = X = x ψ follows from the fact that T X=x ≈ S X=x (Fact 3.2). The case ϕ = ψ ∨ χ for causal teams follows directly from the induction hypothesis. We now give the proof for this case for generalized causal teams. We only prove the left to right direction (the other direction is symmetric).

Characterization of the function components
In this subsection we show that, up to dummy arguments, every system of functions of signature σ is definable in CO[σ]. This result is crucial for adapting the standard methods of team semantics to the causal context.
For any function component F over σ, define a CO[σ]-formula Intuitively, for each non-constant endogenous variable V of F , the formula η σ (V) specifies that all assignments in the (generalized) causal team T in question behave exactly as required by the function F V . For each variable V which, according to F , is exogenous or generated by a constant function, the formula ξ σ (V) states that V is not affected by interventions on other variables. Notice that, if V ∈ Cn(F ), then V has a ξ but not an η clause. Our languages cannot tell apart an endogenous variable that is constant "by law" from an exogenous variable that happens to be (contingently) constant in a team.
Theorem 3.4. Let F ∈ F σ be a function component over some signature σ.
(i) For any generalized causal team T over σ, we have that (ii) For any nonempty causal team T = (T − , G) over σ, we have that Proof.. (i). The second " ⇐⇒ " clearly holds. We now show the first " ⇐⇒ ". If T = ∅, the equivalence holds by the empty team property. Now assume that T ∅.
By the definition of intervention, we must have that For the former, take any w ∈ Ran(W) and p ∈ Ran(PA F V ), and let Z = z abbreviate For the latter, take any v ∈ Ran(V) and w ∈ Ran . Let T be a nonempty causal team. Consider its associated generalized causal team T g . The claim then follows from Lemma 2.16 and item (i).
We call a generalized causal team T uniform if for all (s, F ), (t, G) ∈ T , F ∼ G. In particular, the empty team ∅ is uniform. Uniformity is easily definable in CO \\/ by using the characterizing formulas Φ F of the various function components.
Corollary 3.5. For any generalized causal team T over some signature σ, For any causal team T = (T − , F ), the associated generalized causal team T g = = {(s, F ) | s ∈ T − } is clearly uniform. It thus follows from Lemma 2.16(i) that the formula \\/ F ∈F σ Φ F is valid in causal team semantics.
Furthermore, we now show that the two entailment relations | = g and | = c are equivalent modulo the formula that defines uniformity.
Proof.. ⇐=: Suppose T | = c Γ for some causal team T . Consider the generalized causal team T g generated by T . By Lemma 2.16(i), T g | = g Γ. Since T g is uniform, Corollary 3.5 gives that T g | = g \\/ F ∈F σ Φ F . Then, by assumption, we obtain that T g | = g ψ, which, by Lemma 2.16(i) again, implies that T | = c ψ.
=⇒: Suppose T | = g Γ and T | = g \\/ F ∈F σ Φ F for some generalized causal team T . If T = ∅, then T | = g ψ by the empty team property. Now assume that T ∅. By Corollary 3.5 we know that T is uniform. Pick (t, F ) ∈ T . Consider the generalized causal team S = {(s, F ) | s ∈ T − }. Observe that T ≈ S . Thus, by Theorem 3.3, we have that S | = g Γ, which further implies, by Lemma 2.16(ii), that S c | = c Γ. Hence, by the assumption we conclude that S c | = c ψ. Since (S c ) g = S ≈ T , by applying Lemma 2.16(ii) and Theorem 3.3 again, we obtain T | = g ψ.
The Φ F formulas also help us in understanding the behaviour of the global disjunction \\/ in our languages. In propositional inquisitive logic ( [9]) and propositional dependence logic ( [30]), the global disjunction was shown to have the disjunction property, i.e., | = ϕ \\/ ψ implies | = ϕ or | = ψ. It follows immediately from Theorem 3.4 that the disjunction property of \\/ fails in the context of causal teams, because | = c \\/ F ∈F σ Φ F , whereas | = c Φ F for any F ∈ F σ . Nevertheless, the global disjunction does admit the disjunction property over generalized causal teams.
Regarding causal team semantics (an not the generalized semantics) there is another peculiarity in the behaviour of the global disjunction \\/ : when applied to causally incompatible formulas, the global disjunction \\/ "collapses" to tensor disjunction ∨. We say that two formulas ϕ and ψ in COD[σ] or CO \\/ [σ] are (causally) incompatible if, for all nonempty causal teams S = (S − , F ) and T = (T − , G), For instance, it follows immediately from Theorem 3.4 that the formulas Φ F and Φ G are incompatible when F ∼ G. The key formula in Corollary 3.5, \\/ F ∈F σ Φ F , is thus a global disjunction of pairwise incompatible formulas Φ F . By the result below, we will Since T − ∅, at least one S i is nonempty. If both S i = (S − i , F ) and S j = (S − j , F ) were nonempty (i j), then since ϕ i and ϕ j are incompatible, we would have that F ∼ F ; a contradiction. Hence, we conclude that exactly one S i is nonempty, and thus S i = T . Therefore T | = ϕ i , from which T | = \\/ i∈I ϕ i follows.
The above "collapse" does not only occur in causal team semantics; for a simple example: α ∨ α ≡ c/g α ≡ c/g α \\/ α for any CO-formula α (e.g., α = Φ F ). However, it easy to show that in the generalized (as well as in the non-causal) team semantics, the entailment ϕ ∨ ψ | = g ϕ \\/ ψ implies that ϕ | = ψ or ψ | = ϕ (provided ϕ and ψ are downward closed). 13 On the contrary, the equivalence Φ F ∨ Φ G ≡ c Φ F \\/ Φ G , for F ∼ G, which holds in causal team semantics, does not respect this necessary condition, as neither Φ F implies Φ G nor vice versa.

Characterizing CO
In this section, we characterize the expressive power of CO over causal teams. We also present a system of natural deduction for CO that is sound and complete over both (recursive) causal teams and generalized causal teams. The system is equivalent to the Hilbert-style system of the same logic over (recursive) causal teams introduced in [4].

Expressivity
We show that CO-formulas capture the flat class of (generalized) causal teams, up to ≈-equivalence. Our result is analogous to known characterizations of flat languages in propositional team semantics ( [31]). But in the case of causal teams we have a twist, given by the fact that only the unions of similar causal teams can be reasonably defined. We define such unions as follows.
Clearly, H ∼ F ∼ G and thus S ∪ T ∼ S ∼ T . Let us also remark that even though the definition may seem to look asymmetric as it appears to rely more on F than on G in its details, the notion of union is indeed well-defined, and it guarantees that S ∪ T = T ∪ S . This is because the definition requires that F ∼ G, from which it follows that En(H) = En(F ) \ Cn(F ) = En(G) \ Cn(G), and also that H A formula ϕ over a signature σ determines a class K ϕ of (generalized) causal teams over σ defined as K ϕ = {T | T has signature σ and T | = ϕ}.
We say that a formula ϕ defines a class K of (generalized) causal teams over σ if K = K ϕ . Definition 4.2. We say that a class K of (generalized) causal teams over σ is causally downward closed if T ∈ K and S ⊆ T imply S ∈ K; closed under causal unions if, whenever T 1 , T 2 ∈ K and T 1 ∪T 2 is defined (which is always the case for generalized causal teams), closed under equivalence if T ∈ K and T ≈ S imply S ∈ K.
Fact 4.3. A class K of (generalized) causal teams over σ is flat iff K contains the empty team, is causally downward closed and closed under causal unions.
The class K ϕ is always nonempty as the empty team is always in K ϕ (by Theorem 2.15). By Theorems 2.15 and 3.3, if α is a CO-formula, then K α is flat and closed under equivalence. The main result of this section is the following characterization theorem which gives also the converse direction. Before we present the proof of the theorem, let us first introduce a relation between causal teams that is of central use in this proof. For any (generalized) causal teams S and T , we write S T if S ≈ R ⊆ T for some (generalized) causal team R. In particular, we stipulate ∅ T for all (generalized) causal teams T .

Fact 4.5. A class K of (generalized) causal teams over σ is causally downward closed and closed under equivalence iff K is closed under the relation , i.e., T ∈ K and T S imply S ∈ K.
We leave it for the reader to verify that is a partial order (modulo ≈); in particular, S T and T S imply S ≈ T . The next lemma lists some other useful properties of the relation , where recall that, for every generalized causal team T , we define T F = {(s, G) ∈ T | G ∼ F }.

(ii) If T = T F is uniform and S T , then S is also uniform and S = S F . (iii) If S T , then S
(iv) If S , T are causal teams, then S T ⇐⇒ S g T g . (

v) If S i T i (i ∈ I), then i∈I S i i∈I T i (vi) If S i∈I T i , then for every i ∈ I, there exists S i T i such that S = i∈I S i .
Proof.. Item (i) is easy to prove, items (ii) and (iii) are obvious, and item (iv) follows easily from the fact that both S g and T g are uniform. We only give detailed proof for items (v) and (vi).
Let us begin with (v). Suppose that S i ≈ R i ⊆ T i for some R i (i ∈ I). Let R = i∈I R i . Clearly, i∈I R i ⊆ i∈I T i . It remains to show that S ≈ R for S = i∈I S i . For every F ∈ F σ and every i ∈ I, Now we prove (vi). By the assumption, there is an R such that S ≈ R ⊆ T = i∈I T i . For every i ∈ I, define R i := R ∩ T i and Clearly, R i ⊆ T i . To see that S i T i , it remains to verify that S i ≈ R i . For any F ∈ F σ , we have that Finally, we show that S = i∈I S i . By definition, S i ⊆ S for every i ∈ I. Conversely, for every (s, F ) ∈ S , since S ≈ R, we have by item (i) that Thus, {(s, F )} R i for some i ∈ I. Hence, by definition, (s, F ) ∈ S i . We will next introduce a formula that characterizes the relation in a certain sense. An important part of this characterizing formula is a CO[σ]-formula Θ T − that defines the property "having as team component a subset of T − ". This formula is inspired by a similar one introduced in [30] in the context of propositional team logics. For each (generalized) causal team T over σ = (Dom, Ran), define

(i) Let S and T be generalized causal teams over
(ii) For any causal teams S = (S − , G) and T = ( Proof.. (i) If S = ∅, then ∅ | = g Θ T − ∧ Φ F by the empty team property, and ∅ T by On the other hand, since S | = Φ F , by Theorem 3.4 we must have that (S G ) − = ∅. (ii) Observe that the generalized causal team T g = {(s, F ) | s ∈ T − } associated with T is uniform, T g = (T g ) F and T − = (T g ) − . Thus, by Lemma 2.16(i), item (i) and Lemma 4.6(iv), Corollary 4.9. For any generalized causal teams S and T over σ, we have that Now, assume that T ∅. For each F ∈ F σ , the team T F is uniform. Thus, We are now ready to prove the main theorem of the section.
Proof of Theorem 4.4 . It suffices to prove the direction "⇐=". We first consider the generalized causal team case. Let K be a nonempty class of generalized causal teams that is flat and closed under equivalence. Put T = K. Since K is closed under unions, T ∈ K. Consider the CO[σ]-formula We show that K ϕ = K. For any generalized causal team S , we first deduce, by applying Corollary 4.9 that S ∈ K ϕ ⇐⇒ S | = g ϕ ⇐⇒ S K.
Now assume S ∈ K ϕ ; since then S K, and since K ∈ K and K is closed under , we have that S ∈ K, which gives K ϕ ⊆ K. Conversely, if S ∈ K, then obviously S ≈ S ⊆ K, namely, S K, from which we conclude that S ∈ K ϕ . Next, we consider the causal team case. Let K be a nonempty class of causal teams that is flat and closed under equivalence. For each F ∈ F σ , let Since K is closed under unions and equivalence, ((T F ) − , F ) ∈ K. Consider the generalized causal team T = K g , where K g = {T g | T ∈ K}. Observe that (T F ) − = (T F ) − . Consider the above-defined CO[σ]-formula ϕ with respect to the generalized causal team T . Thus, K ϕ = K over causal teams, since for any causal team S = (S − , G), S | = c ϕ ⇐⇒ S g | = g ϕ (Lemma 2.16(i)) ⇐⇒ S g T (Corollary 4.9) (since ((T G ) − , G) ∈ K and K is closed under ) In the proof above, the case for causal teams is obtained by a reduction to the generalized case. For a direct proof, see [6]. We end this section with some remarks on the sublanguage of CO without the operator . We show that this language is strictly less expressive than CO (and similarly for CO \\/ and COD).
For causal team semantics, we reason similarly by considering instead the class of This proposition implies that causal discourse cannot be entirely reduced to the (propositional) pure team setting, in analogy with the motto that causation cannot be explained in terms of correlation. 14 A further simple consequence of the above proposition is the undefinability of in terms of the other connectives (see [29,8] for details on the notion of definability of connectives in the context of team semantics).

Deduction system
The logic CO over (recursive) causal teams was axiomatized in [4] by means of a sound and complete Hilbert-style deduction system. In this section, we present an equivalent system of natural deduction and show it to be sound and complete also over (recursive) generalized causal teams.
Recall that we have confined ourselves to recursive (generalized) causal teams only. The deduction system we introduce in this section will therefore contain some rules that are not valid over nonrecursive causal teams (such as the rule I). Furthermore, it will have a rule (labelled as Recur) that characterizes recursiveness. In order to present this rule Recur in a compact form, following [17], we write X Y ("X causally affects Y") as an abbreviation for the CO[σ] formula: This formula states that there is some (possibly null) intervention do(Z = z) after which intervening further on X may alter the value of Y. It is in a sense the weakest possible statement of causal dependence between X and Y.

⊥ RAA α -Rules for :
Note that the above system is parametrized with the signature σ. We write Γ ⊢ σ ϕ (or simply Γ ⊢ ϕ when σ is clear from the context) if the formula ϕ can be derived from Γ by applying the rules in the above system.
The connective rules are as in [30]. The axioms ValDef and ValUnq are special cases of the Definiteness and Uniqueness axioms of Galles and Pearl ([12]). The rules Eff and Recur correspond to the Effectiveness and Recursivity from [12]. We remark that Recur is actually a scheme of rules (one rule for each 1 < k ∈ N. Its formulation strongly depends on the finitude of the signature, but it could be in principle replaced by a more elementary rule that does not have this requirement. 15 Furthermore, the role of in the formulation of Recur could be taken instead by the relation of direct cause, as shown in [5]. Rule I is a rule of conjunction conditionalization, from which the Composition rule of [12] is derivable, as we show in the next proposition. The rules ∧I, ∨E and ¬ E correspond to (part of) some additional rules introduced by Halpern ([16]) for the purpose of reducing the complexity of consequents of unnested counterfactuals. Since we also allow right-nested counterfactuals, we need further rules Extr (Extraction) and Exp (Exportation) to remove or add occurrences of from the consequents. A comment might be due concerning the notation used in Extr. As X = x abbreviates a conjunction of equalities X 1 = x 1 ∧· · ·∧ X n = x n , in the context of this rule X ′ = x ′ denotes the formula obtained from X = x after removing all conjuncts X i = x i such that the variable X i is in Y. The four remaining rules, Rpl A , Rpl C , ex falso and ⊥E, were recognized in [4] as implicitly used in earlier completeness proofs; they concern replacement in antecedents and consequents of counterfactuals, and the treatment of inconsistent antecedents/consequents. We remark that a few of the rules in Definition 4.12 and derived rules in Proposition 4.13 below are formulated using the initial Greek letters α, β; we do this to emphasize that these rules are still sound for the extended languages COD and CO \\/ only when α, β are restricted to CO-formulas.
It is easy to verify that all rules in our system are sound over recursive (generalized) causal teams. The axioms and rules in the deduction system of [4] are either included or derivable in our natural deduction system, as shown in the next proposition.
Proposition 4.13. The following are derivable in the system for CO[σ]: Proof.. Item (i) follows from ¬E and ∨E. Items (ii),(iv) follow from ValUnq, ∧E and Rpl C . For item (v), we first derive by applying ∧I, and ⊥E that . Now assume W X. Then we have that θ.

(by Extr)
For item (vi), we first consider the case that X = x is inconsistent. From right to left, we then have ⊢ X = x ϕ ∨ ψ by rule ex falso . From left to right, we can first derive X = x ϕ by ex falso and then ⊢ (X = x ϕ) ∨ (X = x ψ) by ∨I. Now assume that X = x is consistent.
For the right-to-left direction, first we derive For the left-to-right direction, we first use De Morgan's laws (which are easily derivable in the usual way) plus Rpl C to derive from X = x ϕ ∨ ψ that X = x ¬(¬ϕ ∧ ¬ψ), which then gives, by item (v), that ¬ X = x (¬ϕ ∧ ¬ψ) . Next, we derive by applying ¬ E and ∧I, together with ∧E and ∧I, that Then, by applying ¬I and ¬E, we derive the contrapositive of the above, namely By De Morgan's laws again, the formula in the conclusion above is equivalent to (X = x ϕ) ∨ (X = x ψ). This finishes the proof. For item (vii), we first derive by Eff that ⊢ X = x X = x, where X = x is an arbitrary equality from X = x. By ValDef we also have that ⊢ y∈Ran(Y) Y = y. Thus, we conclude by applying Proof.. Since our system derives all axioms and rules of the deduction system of [4], the completeness of our system over causal teams follows from that of [4]. The completeness of the system over generalized causal teams follows from the fact that ∆ | = c α iff ∆ | = g α, given by Corollary 2.17.

Extensions of CO
In this section, we study two extensions of CO, namely CO \\/ and COD. We first show in Section 5.1 that the two logics are both expressively complete in the class of nonempty properties that are causally downward closed and closed under ≈equivalence. Then in Sections 5.2 and 5.3 we axiomatize the two logics over generalized causal team semantics. The axiomatizations for the logics over causal team semantics are given in Section 5.4.

Expressive power of CO \\/ and COD
In this subsection, we characterize the expressive power of CO \\/ and COD over (generalized) causal teams. We show that both logics characterize the nonempty causally downward closed team properties up to causal equivalence, and the two logics are thus expressively equivalent.
Theorem 5.1. Let K be a nonempty class of (generalized) causal teams over some signature σ. Then the following are equivalent: (i) K is causally downward closed and closed under equivalence (or in other words, K is closed under ).

(iii) K is definable by a COD[σ]-formula.
Notice that any such class K is finite. By Theorems 2.15 and 3.3, for every CO \\/ [σ]-or COD[σ]-formula ϕ, the set K ϕ is nonempty, causally downward closed and closed under causal equivalence. Thus items (ii) and (iii) of the above theorem imply item (i). Since dependence atoms =(X; Y) are definable in CO \\/ [σ] (see (1) and (2) in Section 2.2), item (iii) implies item (ii). It then suffices to show that item (i) implies item (iii). We give the proof for the causal team and generalized causal team case simultaneously. In this proof, we make essential use of a formula Ξ T that defines the complement of the set of -successors of a (generalized) causal team T . This formula resembles, in the causal setting, a similar one introduced in [30] in the pure team setting.
The formula Ξ T is a disjunction of three parts. The first disjunct requires some words of comment. Its purpose is to characterize the size of a (generalized) causal team. The size of a causal team T = (T − , F ) can be (naturally) defined as the cardinality of its team component T − . Generalized causal teams have a more complex structure, therefore the notion of size is more subtle. Consider for example the generalized causal team T = {(s, F ), (s, G)}. If F and G are not similar (i.e., F ∼ G), the two elements of T should be counted as distinct; therefore, the cardinality of T − (i.e., |T − | = |{s}| = 1) is not a correct measure of the size of T . On the other hand, if F and G are similar (i.e., F ∼ G, or (s, F ) ≈ (s, G)), the two elements (s, F ) and (s, G) cannot be told apart using our languages; thus our languages do not allow us to distinguish the size of T from that of one of its singleton subteams. We are then forced to say that T has size 1; therefore also |T | = 2 is not a correct measure of the size of T . For these reasons, for generalized causal teams T , we shall be more concerned with the cardinality of the quotient team of T over ≈ between pairs (s, F ) ∈ T , denoted as T/ ≈ .
If T is uniform, then clearly |T/ ≈ | = |T − |. In particular, if S = (S − , F ) is a causal team, then for the generalized causal team S g = {(s, F ) | s ∈ S − } it generates, we have that |S − | = |S g / ≈ |.
In the next lemma, we introduce a formula χ that defines the property of the quotient team T/ ≈ of having cardinality at most 1.
Lemma 5.2. Let T be a generalized causal team over some vocabulary σ.
Proof.. (i) Let T = {(s, F 1 ), . . . , (s, F n )}. If F 1 ∼ · · · ∼ F n , then T ≈ {(s, F 1 )}. Clearly, {(s, F 1 )} | = µ, thus we obtain T | = µ by Theorem 3.3. For the converse direction, suppose T is not uniform, i.e., F i ∼ F j for some 1 ≤ i < j ≤ n. If (w.l.o.g.) En(F i ) \ Cn(F i ) En(F j ) \ Cn(F j ), then there exists V such that V ∈ En(F i ) \ Cn(F i ) and V En(F j ) \ Cn(F j ). The former implies that there are . Let w, w ′ ∈ Ran(W V ) be extensions of the sequences p, p ′ respectively. Clearly, In the second case we have that, for some Then, for any extension w ∈ Ran(W V ) of the sequence xyz, A causal team T can be identified with a (uniform) generalized causal team T g , and, as pointed out already, |T − | = |T g / ≈ |. The above lemma thus gives a characterization of "having size/cardinality at most 1" for causal teams as well. Furthermore, since T g is always uniform, the formula µ that defines uniformity in item (i) above becomes trivial over singleton causal teams. Therefore: For causal teams the formula χ defined above can be simplified as follows: Proof.. For any causal team S , we have that We now introduce COD[σ]-formulas that characterize the cardinality of T/ ≈ . For every natural number k, define a formula χ k as χ 0 = ⊥ and χ k := χ ∨ · · · ∨ χ k for k ≥ 1 Proposition 5.4. Let σ be a vocabulary and k a natural number.
(ii) For any causal team T , by item (i) we have that Now, we are ready to define the crucial formula Ξ T in COD[σ]. Let T be a nonempty generalized causal team with |T/ ≈ | = k + 1. Define where T − = A σ \ T − . If T is a causal team, define Ξ T := Ξ T g . We show in the next lemma the desired characterization property of the formula Ξ T . Recall from Lemma 4.6(i) that T S iff there exists (t, F ) ∈ T such that {(t, F )} S . Proof.. We first show the generalized causal team case. "=⇒": The first clause implies that |S 0 / ≈ | ≤ k, by Proposition 5.4. Since |T/ ≈ | = k + 1, there must exist a (t, G) ∈ T such that {(t, G)} S 0 . Moreover, since S 1 | = Θ T − , we have by Since S − 1 ⊆ T − , by Lemma 4.7 we obtain S 1 | = Θ T − . Let S 2 = S \ (S 0 ∪ S 1 ). Observe that For each (s, F ) ∈ S 2 , we have that {(s, F )} | = Θ {s} ∧ Φ F by Lemma 4.7 and Theorem 3.4. Thus (using also the empty team property) (3) holds. Altogether, we conclude that S | = ϕ.
Next, observe that the causal team case follows from the generalized causal team case, since for any causal teams S , T , we have that Ξ T = Ξ T g and by Lemma 2.16(i) and Lemma 4.6(iv).
Finally, we give the proof of our main theorem of this section.
Proof of Theorem 5.1 . We prove that item (i) implies item (iii). Let K be a nonempty class of (generalized) causal teams as described in item (i). Since K is nonempty and causally downward closed, the empty team belongs to K. Thus, every (generalized) causal team T ∈ C σ \ K is nonempty, where C σ denotes the (finite) set of all (generalized) causal teams over σ. Now, define ϕ = T ∈C σ \K Ξ T . We show that For any S K, i.e., S ∈ C σ \ K, since S S and S − ∅, by Lemma 5.5 we have that S | = Ξ S . Thus S | = ϕ, i.e., S K ϕ . Conversely, suppose S ∈ K. Take any T ∈ C σ \ K. If T S , then since K is closed under we must conclude that T ∈ K; a contradiction. Thus, by Lemma 5.5, S | = Ξ T . Hence S | = ϕ, i.e., S ∈ K ϕ .

Axiomatizing CO \\/ over generalized causal teams
In this section, we introduce a sound and complete system of natural deduction for CO \\/ [σ], which extends the system for CO [σ], and can also be seen as a variant of the systems for propositional dependence logics introduced in [ . . .
-Rules for \\/ : The double line in rule ∨Dst indicates that we are also including the inverse of the rule in the calculi.
The rules in our system are clearly sound. Since our system for CO \\/ [σ] is an extension of that for CO[σ], the clauses in Proposition 4.13 are still derivable (assuming that the formula α that appears in some of the clauses ranges over CO[σ]-formulas only) by the same derivations, except for item (vi) whose proof uses the rule ∨E and the rules for negation which are not sound for arbitrary CO \\/ [σ]-formulas. This item is thus now directly included in the system for CO \\/ [σ]as rule ∨Dst. We now derive some additional useful clauses.
Definition 5.8. Let ϕ be a CO \\/ [σ]-formula. Define the set R(ϕ) of its resolutions inductively as follows: The set R(ϕ) is clearly a finite set of CO[σ]-formulas.
Again, for the rules from Definition 4.12 we assume that α ranges over CO[σ] formulas only. The rule ConE states that if ψ can be derived from the formula ϕ(X = x/[=(X), k]) for every x ∈ Ran(X), then we conclude ψ from ϕ. The rule DepI is read as: if the constancy atom =(Y) can be derived from the constancy atoms =(X 1 ), . . . , =(X n ) (possibly together with other assumptions Γ), then the dependence atom =(X 1 , . . . , X n ; Y) follows (from Γ).
Since the above system contains all applicable rules from the system for CO \\/ [σ], Proposition 4.13 and Proposition 5.7(iii) are still derivable in the system for COD [σ].
It is easy to show that the entailment relation ⊢ is monotone with respect to the substitution of positive subformula occurrences. Proof.. A routine inductive proof, using Rpl A and Rpl C in the case.
In the next proposition we derive some other useful clauses involving dependence atoms.
Proof.. Item (i) follows from ConI and DepE. We now prove item (ii). We will implicitly use Lemma 5.12 in many of the steps. For the left to right direction, we first have by ValDef that ⊢ x∈Ran(X) X = x. Thus, For the right to left direction, putting X = X 1 , . . . , X n , by DepI, it suffices to derive =(X 1 ), . . ., =(X n ), x∈Ran(X) (X = x∧ =(Y)) ⊢=(Y), which, by ConE, is further reduced to for all x ′ ∈ Ran(X) and all y ∈ Ran(Y). Now, we have that (∧E, ConI) Since dependence atoms never occur in the scope of ¬ or in the antecedent of , by Lemma 5.12 and Proposition 5.13(ii), we can transform every COD[σ]-formula into an equivalent one with constancy dependence atoms only.
The rule ConI is clearly sound, since =(X) ≡ \\/ x∈Ran(X) X = x. The soundness of the more complex rule ConE follows from the equivalence which is a special case of a more general equivalence we shall prove in Lemma 5.15 below. In order to state the more general fact, let us first introduce some terminologies. Let d = [=(X 1 ), k 1 ], . . . , [=(X n ), k n ] be a sequence of occurrences of constancy dependence atoms in a formula ϕ. A function f : {1, . . . , n} → 1≤i≤n Ran(X i ) is called an instantiating function over d if f (i) ∈ Ran(X i ) for each i. We define an f -instantiation of ϕ, denoted by ϕ f , as the formula If d lists all occurrences of constancy dependence atoms in ϕ, then we call the formula ϕ f a full instantiation of ϕ. Proof.. We prove the proposition by induction on ϕ. If ϕ is a constancy dependence atom =(X 1 ), it is easy to verify that =( ϕ is a CO[σ]-formula, then the claim is trivial. If ϕ = ψ * χ for * ∈ {∧, ∨}, then the claim follows from the induction hypothesis and the fact that (η \\/ θ) * χ ≡ (η * χ) \\/ (θ * χ). If ϕ = X = x ψ, then by induction hypothesis we have that ψ ≡ \\/ f ∈F ψ f . We then have that Now, we know that the equivalence (4) holds, and thus our system for COD[σ] is sound. For any COD[σ]-formula ϕ, consider the equivalent formula ϕ * given by Corollary 5.14. Denote the set of all full instantiations of ϕ * by I(ϕ). Since all dependence atoms occurring in ϕ * are constancy atoms, I(ϕ) is a finite set of CO[σ]-formulas. Proof.. By Corollary 5.14 and the soundness of the rules, we have ϕ ≡ ϕ * . Then by Lemma 5.15, \\/I(ϕ) ≡ ϕ * ≡ ϕ.
As a further corollary, we have that each validity of COD is "witnessed" by a CO validity, one of its instatiations; or, more generally, we have the following analogous of the disjunction property: To prove the completeness, we will make use of the disjunctive normal form ϕ ≡ \\/I(ϕ). While the global disjunction \\/ in the equivalence is not in the vocabulary of COD[σ], we now show that in our system ϕ behaves proof-theoretically as \\/I(ϕ), in the sense that it proves the same consequences and it is derivable from the same assumptions. (i) For any instantiating function f over d, we have that ϕ f ⊢ ϕ.
(ii) Let f 1 be an arbitrary instantiating function over d. For any arbitrary x ∈ Ran(X 1 ), let g x be the instantiating function over d such that g x (1) = x and g x (i) = f 1 (i) for all 2 ≤ i ≤ n. By the assumption, we have then Γ, ϕ g x ⊢ ψ. Since we can obtain this clause for each x ∈ Ran(X 1 ), we conclude by ConE that for an arbitrary instantiating function f 1 over d. By the same argument, we can show, by using (5) and ConE, that for arbitrary instantiating function f 2 over [=(X 2 ), k 2 ], . . ., [=(X n ), k n ] . Proceeding in the same way, in the end we obtain that Γ, ϕ ⊢ ψ, as required. Now, we can prove the completeness theorem by essentially the same argument as in the proof of Theorem 5.10. Proof.. We prove the direction "=⇒". As in Theorem 5.10, it suffices to prove it for Γ = {ϕ}. Suppose ϕ | = ψ. By Corollary 5.16, we have that \\/I(ϕ) | = \\/I(ψ). It then follows that for every γ ∈ I(ϕ), we have that γ | = \\/I(ψ). Since each γ is a CO[σ]formula, by Theorem 3.8, there is a CO[σ]-formula β ∈ I(ψ) such that γ | = β. Now, by applying Theorem 4.14 and Lemma 5.18(i), we obtain that γ ⊢ β ⊢ ψ for all γ ∈ I(ϕ), which implies by Lemma 5.18(ii) that Γ ⊢ ψ.

Axiomatizing CO \\/ and COD over causal teams
In this section, we axiomatize CO \\/ and COD over causal teams. It can be verified that all the rules in the systems of the two logics over generalized causal teams are also sound over causal teams; in the case of rules without discharging of assumptions, this immediately follows from the fact that causal teams can be regarded as generalized causal teams with uniform function components. To obtain complete systems over causal teams, we shall then add new axioms or rules to characterize the property of having uniform function components (and thus being "indistinguishable" from a causal team). Recall from Corollary 3.5 that the property is defined by the formula \\/ F ∈F σ Φ F , which is, however, not a formula of COD. To give a unified axiomatization for both CO \\/ and COD, we will instead extend the corresponding system with a new rule. Let us now present our systems. The new rule FunE states that if ψ can be derived from Φ F for every F ∈ F σ , then ψ can be derived. The soundness of this rule follows immediately from Corollary 3.6. We write ⊢ c for the entailment relation associated with the system of CO \\/ [σ] or COD[σ] over causal teams (which system is meant will always be clear from the context). Obviously, ⊢ c is an extension of the entailment relation ⊢ g for the corresponding system over generalized causal teams. Proof.. The first " ⇐⇒ " is easy to verify. For the second " ⇐⇒ ", suppose first that Γ, Φ F | = g ψ for all F ∈ F σ . Then we have Γ, Φ F ⊢ g ψ for all F ∈ F σ by the completeness theorem of the CO \\/ [σ]-system (or COD[σ]-system) over generalized causal teams. This then gives that Γ, Φ F ⊢ c ψ for all F ∈ F σ . Finally we derive Γ ⊢ c ψ by applying the rule FunE. Conversely, if Γ ⊢ c ψ, then we have Γ | = c ψ by the soundness theorem. But then we conclude by Lemma 3.7 that Γ, \\/ F ∈F σ Φ F | = g ψ, which completes the proof. Proof.. It suffices to show the direction "=⇒". Suppose Γ | = c ψ. By Lemma 3.7, we have that Γ, \\/ F ∈F σ Φ F | = g ψ, which then gives Γ ⊢ c ψ by Lemma 5.21. Now that we have axiomatized the two logics CO \\/ and COD over causal teams, let us devote the rest of the section to alternative complete systems for these logics, or equivalently, alternative ways to axiomatize the property of a generalized causal team having a uniform function component.
As mentioned already, such a property can be axiomatized in CO \\/ [σ] using the following axiom instead of the rule FunE: It is straightforward to show that the rule FunE and the above axiom Unf\ \/ are interderivable from the rules \\/ I and \\/ E. Therefore, the system consisting of all rules of CO \\/ [σ] over generalized causal teams together with the axiom Unf\ \/ is also sound and complete for CO \\/ [σ] over causal teams.
We now turn to the logic COD. Consider the following axiom schema: For s, t ∈ A σ and F , G ∈ F σ , We now show that the above axiom schema Unf D also defines uniformity of generalized causal teams.
Lemma 5.23. For any generalized causal team T over some signature σ, T | = Ξ {(s,F ),(t,G)} for all s, t ∈ A σ and F , G ∈ F σ with F ∼ G ⇐⇒ T is uniform.
Proof.. Suppose T is uniform. Then T = T H for some H ∈ F σ . For any F , G ∈ F σ with F ∼ G, it must be that either F ∼ H or G ∼ H. Thus, for any s, t ∈ A σ , we have {(s, F ), (t, G)} T , which by Lemma 5.5 implies that T | = Ξ {(s,F ),(t,G)} .
The above lemma implies (by Corollary 3.5) that the axiom schema Unf D is equivalent to the axiom Unf\ \/ , and thus to the rule FunE, given \\/ I and \\/ E. From these it follows that the system consisting of all rules of COD[σ] over generalized causal teams together with the axiom schema Unf D is sound and complete for COD[σ] over causal teams.

Conclusion
We have answered the main questions concerning the expressive power and the existence of complete deduction calculi for the languages that were proposed in [3] and [4], and which involve both interventionist counterfactuals and (contingent) dependencies. We have introduced a generalized causal team semantics that extends the causal discourse to cases in which there may be uncertainty about the causal laws; and we have analyzed the properties of the languages from [3,4] also when they are evaluated in this generalized semantics. We believe the present work may provide guidelines for the investigation of further notions of dependence and causation in causal team semantics and its variants.
Our work shows that many of the methodologies developed in the literature on team semantics can be adapted to the (generalized) causal team semantics. At the same time, a number of peculiarities emerged that set apart these semantic frameworks from the usual team semantics. An interesting anomaly (as noted in [4]) is the existence of formulas whose interpretation only depends on the causal structure; this is the case for the "direct cause" formula mentioned in the introduction (call it β DC (X, V)), or for the following formula: β En (V) := which can be shown to characterize the property of V being endogenous (via a nonconstant function). One unusual aspect of such formulas is that not only the class of causal teams they define is downward closed, but also its complement (taken together with the empty team) is. Some more peculiarities have emerged that only concern the original causal team semantics: first, the failure of the disjunction property for \\/ , and of analogous instantiation properties for the dependence atoms; and secondly, the collapse of \\/ (global disjunction) to ∨ (tensor disjunction) for some special classes of disjuncts. This kind of "collapse" is possible in pure team semantics (and over generalized causal teams) only if one of the disjuncts entails the other, which is however not the case in some of the examples we isolated. We point out that our calculi are sound only for recursive systems, i.e., when the causal graph is acyclic. The general case (and special cases such as the "Lewisian" systems considered in [32]) will require a separate study. We point out, however, that each of our deduction systems can be adapted to the case of unique-solution (possibly generalized) causal teams by replacing the Recur rule with an inference rule that expresses the Reversibility axiom from [12]: See [4] for the details on how the semantics should be adapted for this case. The analysis of causal languages beyond the unique-solution case leads naturally to the consideration of operators (such as the might-counterfactuals) that do not preserve downward closure. It is difficult to guess, at this stage, to what extent the methodologies of team semantics can be adapted to the study of causal languages that are not downward closed. When this issue is solved, it might be interesting to investigate languages that also include non-downward closed contingent (in)dependencies, such as the independence atoms and inclusion atoms considered in the literature on pure team semantics ( [15,13]). Finally, it would be interesting to consider counterfactuals with more complex antecedents -e.g., antecedents containing disjunctions or negations. There have been a number of (often conflicting) proposals in the literature for the semantics of such interventionist counterfactuals [7,1,10,22,21]; it is our hope that causal team semantics can shed some light on this issue. For example, a natural interpretation of a counterfactual (X = 1 ∨ X = 2) ψ is that ψ certainly holds, even if we are not sure which of the interventions do(X = 1) or do(X = 2) has been performed. This uncertainty may be modeled by taking the union of the two (generalized) causal teams resulting from applying each intervention.