# Characterizing counterfactuals and dependencies over causal and generalized
causal teams

Fausto Barbero  Department of Philosophy, History and Art Studies, University
of Helsinki
PL 24 (Unioninkatu 40), 00014 University of Helsinki, Finland
<EMAIL_ADDRESS>
Fan Yang  Department of Mathematics and Statistics, University of Helsinki
PL 68 (Pietari Kalmin katu 5), 00014 University of Helsinki, Finland
<EMAIL_ADDRESS>

###### Abstract

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.

###### keywords:

Interventionist counterfactuals , causal teams , dependence logic , team
semantics

###### MSC:

[2010] 03B60 , 62D20

††journal:

##  1 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
$\mathbf{X}=\mathbf{x}\boxright\psi$ expresses that $\psi$ would hold if we
were to intervene on the given system, by subtracting the variables
$\mathbf{X}$ to their current causal mechanisms and forcing them to take the
values $\mathbf{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_ $=({\mathbf{X}};{Y})$, whose intended
meaning is that the values of the variables in $\mathbf{X}$ determine the
value of $Y$. More precisely, this means that assignments in the team which
agree over $\mathbf{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:

$\bigvee_{\mathbf{z},x\neq x^{\prime},y\neq
y^{\prime}}\big{(}(\mathbf{Z}=\mathbf{z}\land X=x)\boxright
Y=y\land(\mathbf{Z}=\mathbf{z}\land X=x^{\prime})\boxright
Y=y^{\prime}\big{)}$

where $\mathbf{Z}$ is the set of all variables distinct from $X$ and $Y$, and
the disjunction ranges over the possible values of
$\mathbf{z},x,x^{\prime},y,y^{\prime}$ (with $x\neq x^{\prime}$, $y\neq
y^{\prime}$). [4] provided a complete axiomatization for a language
$\mathcal{CO}$ which describes causal dependencies (but no contingent
dependencies)111More precisely, what was axiomatized was a class of languages
$\mathcal{CO}[\sigma]$, each determined by a _signature_ $\sigma$. The
signatures are as in [7].; 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 $\mathcal{COD}$ and
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ (from
[3]), which enrich the basic counterfactual language, respectively, with atoms
of functional dependence $=({\mathbf{X}};{Y})$, or with the global disjunction
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$ (in terms of
which functional dependence is definable). We also give semantical
characterizations, for $\mathcal{COD}$,
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ and the
basic counterfactual language $\mathcal{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
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$, 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 $\mathcal{CO}$ and reformulates in natural deduction
form the $\mathcal{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 $\mathcal{COD}$ and
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$, 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.

##  2 Syntax and semantics

###  2.1 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 $\sigma$, which is a pair $\sigma=(\mathrm{Dom},\mathrm{Ran})$
with $\mathrm{Dom}$ being a nonempty finite set of variables, and
$\mathrm{Ran}$ a function that associates to each variable $X\in\mathrm{Dom}$
a nonempty finite set $\mathrm{Ran}(X)$ (called the range of $X$) of constant
symbols or values $x$. 222Note that we do not encode a distinction between
exogenous and endogenous variables into the signatures, as done in [17].
Instead, we follow the style of Briggs [7]. Doing so will result in more
general completeness results. Throughout the paper we use the Greek letter
$\sigma$ to denote an arbitrary signature.

A boldface capital letter $\mathbf{X}$ stands for a sequence $\langle
X_{1},\dots,X_{n}\rangle$ of variables; similarly, a boldface lower case
letter $\mathbf{x}$ stands for a sequence $\langle x_{1},\dots,x_{n}\rangle$
of values. We will sometimes abuse notation and treat $\mathbf{X}$ and
$\mathbf{x}$ also as sets. We abbreviate the conjunction of equalities
$X_{1}=x_{1}\land\dots\land X_{n}=x_{n}$ as $\mathbf{X}=\mathbf{x}$, where we
always assume that $x_{i}\in Ran(X_{i})$, and also call
$\mathbf{X}=\mathbf{x}$ an equality (over $\sigma$). We write
$\mathrm{Ran}(\mathbf{X})$ for
$\mathrm{Ran}(X_{1})\times\cdots\times\mathrm{Ran}(X_{n})$.

Given a signature $\sigma=(\mathrm{Dom},\mathrm{Ran})$, formulas of our basic
languages $\mathcal{CO}[\sigma]$ are formed according to the grammar:

$\alpha::=X=x\mid\neg\alpha\mid\alpha\land\alpha\mid\alpha\lor\alpha\mid\mathbf{X}=\mathbf{x}\boxright\alpha$

where $\mathbf{X}\cup\\{X\\}\subseteq\mathrm{Dom}$, $x\in\mathrm{Ran}(X)$,
$\mathbf{x}\in\mathrm{Ran}(\mathbf{X})$.333We are identifying syntactical
variables and values with their semantical counterpart, following the
conventions of the literature on interventionist counterfactuals, e.g. [12,
17, 7, 32]. In this convention, distinct symbols (e.g. $x,x^{\prime}$) denote
distinct objects. Obviously, syntax and semantics could in principle be also
kept completely separated; see [4] for details. The connective $\boxright$ is
used to form _interventionist counterfactuals_ , a peculiar type of
conditional formula. Following the literature on team semantics, we also call
the disjunction $\lor$ _tensor disjunction_. Throughout the paper, we reserve
the first letters of the Greek alphabet, $\alpha$ and $\beta$ for
$\mathcal{CO}[\sigma]$ formulas.

We also consider two extensions of $\mathcal{CO}[\sigma]$, obtained by adding
the _global disjunction_
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$, or
dependence atoms $=({\mathbf{X}};{Y})$:

  * -

$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]:~{}~{}\varphi::=X=x\mid\neg\alpha\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\varphi\mid\mathbf{X}=\mathbf{x}\boxright\varphi$

  * -

$\mathcal{COD}[\sigma]:~{}~{}\varphi::=X=x\mid\
=({\mathbf{X}};{Y})\mid\neg\alpha\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\mathbf{X}=\mathbf{x}\boxright\varphi$

where $\mathbf{X}\cup\\{X,Y\\}\subseteq\mathrm{Dom}$, $x\in\mathrm{Ran}(X)$,
$\mathbf{x}\in\mathrm{Ran}(\mathbf{X})$, $\alpha\in\mathcal{CO}[\sigma]$.
According to our syntax, negation is allowed to occur only in front of
$\mathcal{CO}[\sigma]$-formulas $\alpha$.444Following the tradition in the
field of logics of (in)dependence, we do not allow the negation to occur in
front of formulas with occurrences of
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$ or of
dependence atoms. The main reason is that, if we apply to such formulas the
usual semantic clause for negation, we obtain many trivializing results such
as $\neg=({\mathbf{X}};{Y})\equiv\bot$ and
$\neg(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)\equiv\neg(\psi\lor\chi)$.
This syntax for negation is more liberal than that in [3], where formulas are
assumed to be always in negation normal form.

###  2.2 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 $\sigma=(\mathrm{Dom},\mathrm{Ran})$ is a map
$s:\mathrm{Dom}\rightarrow\bigcup_{X\in\mathrm{Dom}}\mathrm{Ran}(X)$ such that
$s(X)\in\mathrm{Ran}(X)$ for every $X\in\mathrm{Dom}$. Denote by
$\mathbb{A}_{\sigma}$ the set of all assignments over $\sigma$. A (non-causal)
team $T^{-}$ over $\sigma$ is a set of assignments over $\sigma$, i.e.,
$T^{-}\subseteq\mathbb{A}_{\sigma}$. The reason for our choice of the notation
$T^{-}$ instead of $T$ will become clear later in this section.

######  Example 2.1.

Let $\mathrm{Dom}=\\{U,X,Y,Z\\}$ be a set of variables, and let

$\mathrm{Ran}(U)=\mathrm{Ran}(X)=\\{0,1\\},~{}\mathrm{Ran}(Y)=\\{1,2\\},\text{
and }~{}\mathrm{Ran}(Z)=\\{2,3,4,5,6\\}.$

Consider the team $T^{-}=\\{s_{1},s_{2}\\}$ over the signature
$\sigma=(\mathrm{Dom},\mathrm{Ran})$, where

$s_{1}=\\{(U,0),(X,0),(Y,1),(Z,2)\\}\text{ and
}s_{2}=\\{(U,1),(X,1),(Y,2),(Z,6)\\}.$

The team $T^{-}$ clearly respects the ranges of the variables, as, e.g.,
$s_{2}(Z)=6\in\mathrm{Ran}(Z)$. We can represent the team $T^{-}$ as a table:

U X Y Z
---
$0$ | $0$ | $1$ | $2$
$1$ | $1$ | $2$ | $6$

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 $\mathcal{F}$ over $\sigma$ is a function that assigns
to each variable $V$ in a domain
$\mathrm{En}(\mathcal{F})\subseteq\mathrm{Dom}$ a set
$PA^{\mathcal{F}}_{V}\subseteq\mathrm{Dom}\setminus\\{V\\}$ of parents of $V$,
and a function
$\mathcal{F}_{V}:\mathrm{Ran}(PA^{\mathcal{F}}_{V})\rightarrow\mathrm{Ran}(V)$.555We
identify the set $PA^{\mathcal{F}}_{V}$ with a sequence, in a fixed
lexicographical ordering. Variables in the set $\mathrm{En}(\mathcal{F})$ are
called endogenous variables of $\mathcal{F}$, and variables in
$\mathrm{Ex}(\mathcal{F})=\mathrm{Dom}\setminus\mathrm{En}(\mathcal{F})$ are
called exogenous variables of $\mathcal{F}$.

Denote by $\mathbb{F}_{\sigma}$ the set of all systems of functions over
$\sigma$, which is clearly finite. Any system of functions
$\mathcal{F}\in\mathbb{F}_{\sigma}$ can be naturally associated with a
(directed) graph $G_{\mathcal{F}}=(\mathrm{Dom},E_{\mathcal{F}})$, defined as

$(X,Y)\in E_{\mathcal{F}}\text{ iff }X\in PA_{Y}^{\mathcal{F}}.$

A cycle is a subset of $E_{\mathcal{F}}$ of the form
$\\{(X_{1},X_{2}),(X_{2},X_{3}),\dots,(X_{n},X_{1})\\}$, where $X_{1},\dots
X_{n}$ ($n\geq 1$) are distinct variables. We say that $\mathcal{F}$ is
recursive if $G_{\mathcal{F}}$ is acyclic, i.e., no subset of
$E_{\mathcal{F}}$ is a cycle.

######  Example 2.2.

Consider the system of functions $\mathcal{F}$ (over the signature $\sigma$
from Example 2.1) described by the following graph $G_{\mathcal{F}}$ and
system of equations:

U  X  Y  Z
---

$\left\\{\begin{array}[]{lcl}\mathcal{F}_{X}(U)&=&U\\\
\mathcal{F}_{Y}(X)&=&X+1\\\ \mathcal{F}_{Z}(X,Y,U)&=&2Y+X+U\\\
\end{array}\right.$

The system of equations above describes the “laws” that generate the values of
the variables $X,Y$ and $Z$ in terms of the values of other variables. For
instance, in the graph $G_{\mathcal{F}}$ the arrow from $U$ to $Z$ represents
an edge $(U,Z)$. The equations are consistent with the graph
$G_{\mathcal{F}}$. Since $G_{\mathcal{F}}$ contains no cycles, $\mathcal{F}$
is recursive. The variable $U$ with no incoming arrows is the only exogenous
variable; the other variables are endogenous. That is,
$\mathrm{Ex}(\mathcal{F})=\\{U\\}$, and
$\mathrm{En}(\mathcal{F})=\\{X,Y,Z\\}$. The parents of each endogenous
variable can also be easily read off from the above graph and equations:
$PA^{\mathcal{F}}_{X}=\\{U\\}$, $PA^{\mathcal{F}}_{Y}=\\{X\\}$ and
$PA^{\mathcal{F}}_{Z}=\\{X,Y,U\\}$.

We say that an assignment $s\in\mathbb{A}_{\sigma}$ is compatible with a
system of functions $\mathcal{F}\in\mathbb{F}_{\sigma}$ if for all endogenous
variables $V\in\mathrm{En}(\mathcal{F})$,

$s(V)=\mathcal{F}_{V}(s(PA_{V}^{\mathcal{F}})).$

######  Definition 2.3.

A causal team over a signature $\sigma$ is a pair $T=(T^{-},\mathcal{F})$
consisting of

  * -

a team $T^{-}$ over $\sigma$, called the team component of $T$, and

  * -

a system of functions $\mathcal{F}$ over $\sigma$, called the function
component of $T$,

where all assignments $s\in T^{-}$ are compatible with the function component
$\mathcal{F}$.

In particular, a pair $T=(\emptyset,\mathcal{F})$ with the team component
being the empty set $\emptyset$ is also a causal team. For simplicity, over
the same signature $\sigma$, we identify all teams with the empty team
component and different function components, namely we stipulate
$\emptyset:=(\emptyset,\mathcal{F})=(\emptyset,\mathcal{G})$ for any function
components $\mathcal{F},\mathcal{G}$ over $\sigma$. We call the causal team
$\emptyset$ the empty causal team (over $\sigma$).

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.666In particular, it naturally involves the treatment of
_might_ -counterfactuals, which are not downward closed formulas in the sense
explained in Theorem 2.15. They are thus out of the reach of the methods used
in the present paper.

Intuitively, a causal team $T$ may be seen as representing an assumption
concerning the causal relationships among the variables in $\mathrm{Dom}$ (as
encoded in $\mathcal{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
$\mathcal{F}$ of functions from Example 2.2 into a causal team
$T=(T^{-},\mathcal{F})$, as illustrated in the following diagram:

$T^{-}$:  U  X  Y  Z $0$ $0$ $1$ $2$ $1$ $1$ $2$ $6$
$\left\\{\begin{array}[]{lcl}\mathcal{F}_{X}(U)&=&U\\\
\mathcal{F}_{Y}(X)&=&X+1\\\ \mathcal{F}_{Z}(X,Y,U)&=&2Y+X+U\\\
\end{array}\right.$

It is easy to verify that all assignments in the team component $T^{-}$ are
compatible with the function component $\mathcal{F}$, e.g.,

$s_{2}(Z)=6=2\cdot 2+1+1=2\cdot
s(Y)+s(X)+s(U)=\mathcal{F}_{Z}(s(X),s(Y),s(U)).$

The arrows in the upper part of the table represent the graph $G_{T}$ of the
causal team $T$, which is defined as $G_{\mathcal{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^{-},\mathcal{G})$ and $T=(T^{-},\mathcal{F})$ be causal teams over
the same signature $\sigma$. We call $S$ a causal subteam of $T$, denoted as
$S\subseteq T$, if $S^{-}\subseteq T^{-}$ and $\mathcal{G}=\mathcal{F}$. We
stipulate that the empty causal team $\emptyset$ over $\sigma$ is a causal
subteam of any causal team $T$ over $\sigma$, i.e., $\emptyset\subseteq T$.

An equality $\mathbf{X}=\mathbf{x}$ (i.e., $X_{1}=x_{1}\wedge\dots\wedge
X_{n}=x_{n})$ is said to be inconsistent if it contains two conjuncts $X=x$
and $X=x^{\prime}$ with distinct values $x,x^{\prime}$; otherwise it is said
to be consistent. For a sequence $\mathbf{X}=\langle X_{1},\dots,X_{n}\rangle$
of variables and an assignment $s$, we write $s(\mathbf{X})$ for $\langle
s(X_{1}),\dots,s(X_{n})\rangle$.

######  Definition 2.6 (Intervention).

Let $T=(T^{-},\mathcal{F})$ be a causal team over some signature
$\sigma=(\mathrm{Dom},\mathrm{Ran})$. Let
$\mathbf{X}=\mathbf{x}\,(=X_{1}=x_{1}\wedge\dots\wedge X_{n}=x_{n})$ be a
consistent equality over $\sigma$. The intervention
$do(\mathbf{X}=\mathbf{x})$ on $T$ is the procedure that generates a new
causal team
$T_{\mathbf{X}=\mathbf{x}}=(T_{\mathbf{X}=\mathbf{x}}^{-},\mathcal{F}_{\mathbf{X}=\mathbf{x}})$
over $\sigma$ defined as follows:

  * -

$\mathcal{F}_{{\mathbf{X}=\mathbf{x}}}$ is the restriction of $\mathcal{F}$ to
$\mathrm{En}(\mathcal{F})\setminus\mathbf{X}$, that is, the system of
functions that assigns to each variable
$V\in\mathrm{En}(\mathcal{F})\setminus\mathbf{X}$ the set of parents
$PA^{\mathcal{F}}_{V}$ and the function $\mathcal{F}_{V}$ as prescribed by
$\mathcal{F}$;

  * -

$T_{\mathbf{X}=\mathbf{x}}^{-}=\\{s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}}\mid
s\in T^{-}\\}$, where each $s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}}$ is an
assignment compatible with $\mathcal{F}_{{\mathbf{X}=\mathbf{x}}}$ defined
(recursively) as

$s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}}(V)=\begin{cases}x_{i}&\text{ if
}V=X_{i}\text{ for some }1\leq i\leq n,\\\ s(V)&\text{ if
}V\in\mathrm{Ex}(\mathcal{F})\setminus\mathbf{X},\\\
\mathcal{F}_{V}(s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}}(PA_{V}^{\mathcal{F}}))&\text{
if }V\in\mathrm{En}(\mathcal{F})\setminus\mathbf{X}.\end{cases}$

Every $s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}}$ defined above represents the
result of the intervention on the single assignment $s$ with respect to
$\mathcal{F}$. In the following, when the $\mathcal{F}$ is clear from the
context, we sometimes simply write $s_{\mathbf{X}=\mathbf{x}}$.

We stipulate that the intervention $do(\mathbf{X}=\mathbf{x})$ on the empty
causal team $\emptyset$ generates the empty causal team itself, i.e.,
$\emptyset_{\mathbf{X}=\mathbf{x}}=\emptyset$.

######  Example 2.7.

Recall the recursive causal team $T$ in Example 2.4. By applying the
intervention $do(X=1)$ to $T$, we obtain a new causal team
$T_{X=1}=(T_{X=1}^{-},\mathcal{F}_{X=1})$ as follows. The function component
$\mathcal{F}_{X=1}$ is determined by the following system of equations:

$\left\\{\begin{array}[]{lcl}(\mathcal{F}_{X=1})_{Y}(X)&=&X+1\\\
(\mathcal{F}_{X=1})_{Z}(X,Y)&=&2Y+X+U\\\ \end{array}\right.$

The endogenous variable $X$ of the original team $T$ becomes exogenous in the
new team $T_{X=1}$, and the equation $\mathcal{F}_{X}(U)=U$ for $X$ is now
removed. The new team component $T_{X=1}^{-}$ is obtained by the rewriting
procedure illustrated below:

U  X  Y  Z
---
$0$ |  $\mathbf{1}$ | … | …
$1$ | $\mathbf{1}$ | … | …

$\rightsquigarrow$ U  X  Y  Z $0$ $1$ $\mathbf{2}$ … $1$ $1$ $\mathbf{2}$ …
$\rightsquigarrow$ U  X  Y  Z $0$ $1$ $2$ $\mathbf{5}$ $1$ $1$ $2$
$\mathbf{6}$

In the first step, rewrite the $X$-column with value $1$. Then, update
(recursively) the other columns using the functions from
$\mathcal{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.

######  Definition 2.8.

Let $\varphi$ be a formula in the language
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
or $\mathcal{COD}[\sigma]$, and $T=(T^{-},\mathcal{F})$ a causal team over
$\sigma$. We define the satisfaction relation $T\models^{c}\varphi$ (or simply
$T\models\varphi$) over causal teams inductively as follows:

  * -

$T\models X=x$ iff for all $s\in T^{-}$, $s(X)=x$.777Note once more that the
symbol $x$ is used as both a syntactical and a semantical object.

  * -

$T\models\,=({\mathbf{X}};{Y})$ iff for all $s,s^{\prime}\in T^{-}$,
$s(\mathbf{X})=s^{\prime}(\mathbf{X})$ implies $s(Y)=s^{\prime}(Y)$.

  * -

$T\models\neg\alpha$ iff for all $s\in T^{-}$,
$(\\{s\\},\mathcal{F})\not\models\alpha$.

  * -

$T\models\varphi\land\psi$ iff $T\models\varphi$ and $T\models\psi$.

  * -

$T\models\varphi\lor\psi$ iff there are two causal subteams
$T_{1},T_{2}\subseteq T$ such that $T_{1}^{-}\cup T_{2}^{-}=T^{-}$,
$T_{1}\models\varphi$ and $T_{2}\models\psi$.

  * -

$T\models\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$
iff $T\models\varphi$ or $T\models\psi$.

  * -

$T\models\mathbf{X}=\mathbf{x}\boxright\varphi$ iff $\mathbf{X}=\mathbf{x}$ is
inconsistent or $T_{\mathbf{X}=\mathbf{x}}\models\varphi$.

As usual, define $\bot:=X=x\wedge X\neq x$, where $X\neq x$ is short for
$\neg(X=x)$. Clearly, $T\models\bot$ iff $T=\emptyset$.

We write $T\models\Gamma$ and say that “$T$ satisfies $\Gamma$” if
$T\models\varphi$ for each $\varphi\in\Gamma$. As usual, we can define
semantic entailment in terms of satisfaction. For any fixed signature
$\sigma$, we write that $\Gamma\models^{c}\varphi$ (or simply
$\Gamma\models\varphi$ whenever there is no risk of ambiguity) if every
(recursive) causal team $T$ of signature $\sigma$ that satisfies $\Gamma$ also
satisfies $\varphi$. We say that $\varphi$ and $\psi$ are equivalent, denoted
as $\varphi\equiv^{c}\psi$ (or simply $\varphi\equiv\psi$) if
$\varphi\models^{c}\psi$ and $\psi\models^{c}\varphi$.

We write a dependence atom $=({};{Y})$ with an empty first component as
$=({Y})$. Clearly, the semantic clause for $=({Y})$ reduces to:

  * -

$T\models\,=({Y})$ iff for all $s,s^{\prime}\in T^{-}$, $s(Y)=s^{\prime}(Y)$.

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:

$=({\mathbf{X}};{Y})\equiv\bigvee_{\mathbf{x}\in\mathrm{Ran}(\mathbf{X})}(\mathbf{X}=\mathbf{x}\,\wedge=({Y})).$
(1)

Furthermore, in
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$,
the finitude of $\sigma$ makes the constancy atoms definable:

$\displaystyle=({Y})\equiv\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{y\in\mathrm{Ran}(Y)}Y=y.$
(2)

Thus, by (1) and (2), the dependence atoms themselves are definable in
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$.

Recall that counterfactuals $\mathbf{X}=\mathbf{x}\boxright\varphi$ express
that $\varphi$ holds after an intervention. In [3, 4], another conditional
operator $\supset$ called the _selective implication_ also plays an important
role. The selective implication $\alpha\supset\varphi$ (always with a
$\mathcal{CO}$-formula $\alpha$ in the antecedent) expresses that $\varphi$
holds after observing a fact described by $\alpha$. Its semantics is defined
as:

  * -

$T\models\alpha\supset\varphi\iff T^{\alpha}\models\varphi$, where
$T^{\alpha}$ is the (unique) causal subteam of $T=(T^{-},\mathcal{F})$ with
team component $(T^{\alpha})^{-}=\\{s\in
T^{-}\mid(\\{s\\},\mathcal{F})\models\alpha\\}$.

It is easy to verify that $\alpha\supset\varphi\equiv\neg\alpha\lor\varphi$ in
the languages considered in this paper.888The equivalence holds due to the
fact that the languages are _downward closed_ (see Theorem 2.15). In the
absence of downward closure, $\supset$ is still definable by the more general
equivalence $\alpha\supset\varphi\equiv\neg\alpha\lor(\alpha\land\varphi)$. We
thus treat the selective implication $\alpha\supset\varphi$ 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.,

$(\\{s\\},\mathcal{F})\models\alpha\supset\varphi\iff(\\{s\\},\mathcal{F})\not\models\alpha\text{
or }(\\{s\\},\mathcal{F})\models\varphi.$

######  Example 2.9.

Consider the causal team $T$ and the intervention $do(X=1)$ from Examples 2.4
and 2.7. Clearly, $T_{X=1}\models Y=2$, and thus $T\models X=1\boxright Y=2$.
We also have that $T\models=({Y};{Z})$, while $T_{X=1}\not\models=({Y};{Z})$
(contingent dependencies are not in general preserved by interventions).
Observe that $T\models Y\neq 2\lor Y=2$, while $T\not\models Y\neq
2\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}Y=2$.
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\models X=1\supset
Y=2$.

###  2.3 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 $\sigma$, we write

$\mathbb{S}\mathbbm{em}_{\sigma}:=\\{(s,\mathcal{F})\in\mathbb{A}_{\sigma}\times\mathbb{F}_{\sigma}\mid
s\text{ is compatible with }\mathcal{F}\\}.$

The pairs $(s,\mathcal{F})\in\mathbb{S}\mathbbm{em}_{\sigma}$ 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^{-},\mathcal{F})$ with the set

$T^{g}=\\{(s,\mathcal{F})\mid s\in T^{-}\\}$

of deterministic causal models with a common function component $\mathcal{F}$.
We now introduce the notion of generalized causal team, in which the function
component $\mathcal{F}$ does not have to be constant throughout the team.

######  Definition 2.10.

A generalized causal team $T$ over a signature $\sigma$ is a set of pairs
$(s,\mathcal{F})\in\mathbb{S}\mathbbm{em}_{\sigma}$, that is,
$T\subseteq\mathbb{S}\mathbbm{em}_{\sigma}$. We call the set

$T^{-}:=\\{s\mid(s,\mathcal{F})\in T\text{ for some }\mathcal{F}\\}$

the team component of $T$. A causal subteam of $T$ is a subset $S$ of $T$,
denoted as $S\subseteq T$. In particular, the empty set $\emptyset$ is a
generalized causal team, and $\emptyset\subseteq T$ for all generalized causal
teams $T$.

The union $S\cup T$ of two generalized causal teams $S,T$ is their set-
theoretic union.

Intuitively, a generalized causal team encodes uncertainty about which causal
model governs the variables in $\mathrm{Dom}$ \- i.e., uncertainty both on the
values of the variables and on the laws that determine them. Distinct elements
$(s,\mathcal{F}),(t,\mathcal{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,\mathcal{F})$ in the team, the associated graph
$G_{\mathcal{F}}$ is recursive. In this paper we only consider recursive
generalized causal teams.

######  Example 2.11.

Let $\sigma=(\mathrm{Dom},\mathrm{Ran})$ be a signature with variables
$\mathrm{Dom}=\\{X,Y,Z\\}$ and ranges $\mathrm{Ran}(X)=\\{1,2\\}$,
$\mathrm{Ran}(Y)=\\{2,3\\}$ and $\mathrm{Ran}(Z)=\\{3,4,5\\}$. Let
$\mathcal{F},\mathcal{G}\in\mathbb{F}_{\sigma}$ be two (recursive) systems of
functions described by the following two systems of equations:

$\left\\{\begin{array}[]{lcl}\mathcal{F}_{Z}(X)=2X\\\ \end{array}\right.$
$\left\\{\begin{array}[]{lcl}\mathcal{G}_{Z}(X,Y)=X+Y\\\ \end{array}\right.$

Consider two assignments $s=\\{(X,2),(Y,2),(Z,4)\\}\text{ and
}t=\\{(X,1),(Y,3),(Z,4)\\}$ over $\sigma$. Now, the generalized causal team
$T=\\{(s,\mathcal{F}),(s,\mathcal{G}),(t,\mathcal{G})\\}$ over $\sigma$ can be
represented as the following table:

$X$ $Y$ $Z$
---
2 | 2 | 4 | $\mathcal{F}$
2 | 2 | 4 | $\mathcal{G}$
1 | 3 | 4 | $\mathcal{G}$

The first element $(s,\mathcal{F})$ differs from the second one
$(s,\mathcal{G})$ in its function component (as $\mathcal{F}\neq\mathcal{G}$).
Since both $\mathcal{F}$ and $\mathcal{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
$\mathcal{F}_{1},\dots,\mathcal{F}_{n}$ that might have produced these data,
we may represent the situation by a generalized causal team that contains
causal models $(s,\mathcal{F}_{1}),\dots,(s,\mathcal{F}_{n})$ for each
distinct entry $s$ of the original database.999If one wants to make
considerations of probabilistic nature, it might be necessary to allow
multiple copies of the same causal model to occur in the model. We are not
pursuing the probabilistic view in this paper, but see [3] for some ideas in
this direction. 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,\mathcal{F})$ for each system of functions $\mathcal{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$.101010In a discussion
with the first author, Johan van Benthem suggested the possibility of using
teams to represent uncertainty about the correct causal graph. With a little
extra toil, also this can be represented by a generalized causal team. 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^{\circ}$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.111111[3] proposed a different solution to this
representation problem, the _partially defined causal teams_. This framework
can then be identified with a very special case of generalized causal team
semantics. On the other hand, the kind of representation proposed in [3] might
be more efficient for this specialized task.

Let us now come back to the formal theory. We have already mentioned that a
causal team $T=(T^{-},\mathcal{F})$ can be identified with the generalized
causal team $T^{g}=\\{(s,\mathcal{F})\mid s\in T^{-}\\}$, which has a constant
function component in all its elements. Conversely, if $T$ is a nonempty
generalized causal team in which all elements have the same function component
$\mathcal{F}$, i.e., $T=\\{(s,\mathcal{F})\mid s\in T^{-}\\}$, we can
naturally identify $T$ with the causal team

$T^{c}=(T^{-},\mathcal{F}).$

We stipulate that the empty generalized causal team $\emptyset$ corresponds to
the empty causal team $\emptyset$, i.e., $\emptyset^{c}=\emptyset$. In
particular, a singleton generalized causal team $\\{(s,\mathcal{F})\\}$
corresponds to a singleton causal team $(\\{s\\},\mathcal{F})$. Applying a
(consistent) intervention $do(\mathbf{X}=\mathbf{x})$ on the causal team
$(\\{s\\},\mathcal{F})$ generates a causal team
$(\\{s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}}\\},\mathcal{F}_{\mathbf{X}=\mathbf{x}})$
as specified in Definition 2.6. We can then define the result of the
intervention $do(\mathbf{X}=\mathbf{x})$ on the _generalized_ causal team
$\\{(s,\mathcal{F})\\}$ to be the generalized causal team
$(\\{s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}}\\},\mathcal{F}_{\mathbf{X}=\mathbf{x}})^{g}=\\{(s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}},\mathcal{F}_{\mathbf{X}=\mathbf{x}})\\}$.
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 $\mathbf{X}=\mathbf{x}$
a consistent equality over $\sigma$. The intervention
$do(\mathbf{X}=\mathbf{x})$ on $T$ generates the generalized causal team

$T_{\mathbf{X}=\mathbf{x}}:=\\{(s^{\mathcal{F}}_{\mathbf{X}=\mathbf{x}},\mathcal{F}_{\mathbf{X}=\mathbf{x}})\mid(s,\mathcal{F})\in
T\\}.$

######  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_{\mathbf{X}=\mathbf{x}}$ after the intervention is as follows:

X Y Z
---
2 | 1 | 4 | $\mathcal{F}_{Y=1}$
2 | 1 | 3 | $\mathcal{G}_{Y=1}$
1 | 1 | 2 | $\mathcal{G}_{Y=1}$

The function components are $\mathcal{F}_{Y=1}=\mathcal{F}$ and
$\mathcal{G}_{Y=1}=\mathcal{G}$, since $Y$ is exogenous for both $\mathcal{F}$
and $\mathcal{G}$. Since $Y$ is not a parent of any endogenous variable of
$\mathcal{F}$, the values of other variables in the first row remain unchanged
after the intervention.

######  Definition 2.14.

Let $\varphi$ be a formula of the language
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
or $\mathcal{COD}[\sigma]$, and let $T$ be a generalized causal team over
$\sigma$. The satisfaction relation $T\models^{g}\varphi$ (or simply
$T\models\varphi$) over generalized causal teams is defined in the same way as
in Definition 2.8, except for slight differences in the following clause:

  * -

$T\models^{g}\neg\alpha$ iff for all $(s,\mathcal{F})\in T$,
$\\{(s,\mathcal{F})\\}\not\models\alpha$.

For any fixed $\sigma$, we also write $\Gamma\models^{g}\varphi$ (or simply
$\Gamma\models\varphi$) if all (recursive) generalized causal teams of
signature $\sigma$ that satisfy $\Gamma$ also satisfy $\varphi$; and
$\varphi\equiv^{g}\psi$ (or simply $\varphi\equiv\psi$) if
$\varphi\models^{g}\psi$ and $\psi\models^{g}\varphi$.

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.

######  Theorem 2.15.

Let $T,S$ be (generalized) causal teams over some signature $\sigma$, and let
$\varphi$ be a
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$-formula
or $\mathcal{COD}[\sigma]$-formula.

Empty team property

$\emptyset\models\varphi$.

Downward closure

If $T\models\varphi$ and $S\subseteq T$, then $S\models\varphi$.

In addition, $\mathcal{CO}[\sigma]$-formulas $\alpha$ are closed under unions:

Union closure

If $T\models\alpha$ and $S\models\alpha$, then $T\cup S\models\alpha$,
whenever $T\cup S$ is defined.121212The unions of generalized causal teams are
always defined, as in definition 2.10. The union of two causal teams with
distinct function components, instead, will not generally produce a causal
team. See section 4.1 for a definition of the union of (similar) causal teams.

The empty team property, downward closure and union closure together are
equivalent to the flatness property, which $\mathcal{CO}[\sigma]$-formulas
satisfy:

Flatness

$T\models\alpha\iff(\\{s\\},\mathcal{F})\models^{c}\alpha\text{ for all }s$ in
$T=(T^{-},\mathcal{F})$

$\hskip 100.0pt(\text{resp. }\\{(s,\mathcal{F})\\}\models^{g}\alpha\text{ for
all }(s,\mathcal{F})\in T).$

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.

######  Lemma 2.16.

Let $\varphi$ be a
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
or a $\mathcal{COD}[\sigma]$ formula.

  1. (i)

For any causal team $T$, we have that $T\models^{c}\varphi\iff
T^{g}\models^{g}\varphi.$

  2. (ii)

For any generalized causal team $T$ with a unique function component, we have
that $T\models^{g}\varphi\iff T^{c}\models^{c}\varphi.$

#### Proof.

Both items are proved by straightforward induction. $\square$

######  Corollary 2.17.

For any set $\Delta\cup\\{\alpha\\}$ of $\mathcal{CO}[\sigma]$-formulas,
$\Delta\models^{g}\alpha$ iff $\Delta\models^{c}\alpha$.

#### Proof.

Assume $\Delta\models^{c}\alpha$, and let $T$ be a generalized causal team
such that $T\models^{g}\Delta$. If $T=\emptyset$, by the empty team property
we have $T\models\alpha$, and we are done. Otherwise observe that, by the
flatness of $\Delta$, $\\{(s,\mathcal{F})\\}\models^{g}\Delta$ for each
$(s,\mathcal{F})\in T$. By Lemma 2.16, we then have that
$(\\{s\\},\mathcal{F})\models^{c}\Delta$ for each $(s,\mathcal{F})\in T$. By
the assumption $\Delta\models^{c}\alpha$, we have
$(\\{s\\},\mathcal{F})\models^{c}\alpha$ for each $(s,\mathcal{F})\in T$. By
lemma 2.16 again, $\\{(s,\mathcal{F})\\}\models^{g}\alpha$ for each
$(s,\mathcal{F})\in T$. By flatness of $\alpha$, we conclude
$T\models^{g}\alpha$. The converse direction is proved analogously. $\square$

##  3 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 can _not_ be
described by our languages.

###  3.1 Equivalence of function components

Consider a binary function $f$ and a quaternary function $g$ defined as
$f(X,Y)=X+Y\text{ and }g(X,Y,Z_{1},Z_{2})=X+Z_{1}+0/Z_{2}+(Y-Z_{1}).$
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.

######  Definition 3.1.

Let $\mathcal{F},\mathcal{G}$ be two function components over
$\sigma=(\mathrm{Dom},\mathrm{Ran})$.

  * -

Let $V\in\mathrm{Dom}$. The two functions $\mathcal{F}_{V}$ and
$\mathcal{G}_{V}$ are said to be equivalent up to dummy arguments, denoted as
$\mathcal{F}_{V}\sim\mathcal{G}_{V}$, if for any
$\mathbf{x}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}}\cap PA_{V}^{\mathcal{G}})$,
$\mathbf{y}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}}\setminus
PA_{V}^{\mathcal{G}})$ and
$\mathbf{z}\in\mathrm{Ran}(PA_{V}^{\mathcal{G}}\setminus
PA_{V}^{\mathcal{F}})$, we have that

$\mathcal{F}_{V}(\mathbf{x}\mathbf{y})=\mathcal{G}_{V}(\mathbf{x}\mathbf{z})$

(where we assume w.l.o.g. the shown orderings of the arguments of the
functions).

  * -

Let $\mathrm{Cn}(\mathcal{F})$ denote the set of endogenous variables $V$ of
$\mathcal{F}$ for which $\mathcal{F}_{V}$ is a constant function, i.e., for
some fixed $c\in\mathrm{Ran}(V)$,

$\mathcal{F}_{V}(\mathbf{p})=c\text{ for all }\mathbf{p}\in
PA_{V}^{\mathcal{F}}.$

We say that $\mathcal{F}$ and $\mathcal{G}$ are equivalent up to dummy
arguments, denoted as $\mathcal{F}\sim\mathcal{G}$, if

    * (a)

$\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})=\mathrm{En}(\mathcal{G})\setminus\mathrm{Cn}(\mathcal{G})$,

    * (b)

and $\mathcal{F}_{V}\sim\mathcal{G}_{V}$ holds for all
$V\in\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$.

It is easy to see that $\sim$ is an equivalence relation. Furthermore, the
relation $\sim$ is preserved under interventions.

######  Fact 3.2.

For any function components $\mathcal{F},\mathcal{G}\in\mathbb{F}_{\sigma}$
and consistent equality $\mathbf{X}=\mathbf{x}$ over $\sigma$, we have that
$\mathcal{F}\sim\mathcal{G}$ implies
$\mathcal{F}_{\mathbf{X}=\mathbf{x}}\sim\mathcal{G}_{\mathbf{X}=\mathbf{x}}$.

#### Proof.

Straightforward; see [6]. $\square$

We now generalize the equivalence relation $\sim$ to the causal team level.
Two nonempty causal teams $T=(T^{-},\mathcal{F})$ and $S=(S^{-},\mathcal{G})$
of the same signature $\sigma$ are said to be similar, denoted as $T\sim S$,
if $\mathcal{F}\sim\mathcal{G}$; equivalent, denoted as $T\approx S$, if
$T\sim 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

$T^{\mathcal{F}}:=\\{(s,\mathcal{G})\in T\mid\mathcal{G}\sim\mathcal{F}\\}.$

Two generalized causal teams $S$ and $T$ are said to be equivalent, denoted as
$S\approx T$, if $(S^{\mathcal{F}})^{-}=(T^{\mathcal{F}})^{-}$ for all
$\mathcal{F}\in\mathbb{F}_{\sigma}$.

Moreover, we define the equivalence relation $\approx$ between elements of
$\mathbb{S}\mathbbm{em}_{\sigma}$ by taking

$(s,\mathcal{F})\approx(t,\mathcal{G})~{}\text{ iff
}~{}\\{(s,\mathcal{F})\\}\approx\\{(t,\mathcal{G})\\}~{}~{}(\text{ iff
}~{}s=t\text{ and }\mathcal{F}\sim\mathcal{G}).$

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.

######  Theorem 3.3 (Invariance under causal equivalence).

Let $T,S$ be two (generalized) causal teams over $\sigma$ with $T\approx S$.
For any formula $\varphi$ of $\mathcal{CO}[\sigma]$,
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
or $\mathcal{COD}[\sigma]$, we have that $T\models\varphi\iff
S\models\varphi.$

#### Proof.

The theorem is proved by induction on $\varphi$. The case
$\varphi=\,\mathbf{X}=\mathbf{x}\boxright\psi$ follows from the fact that
$T_{\mathbf{X}=\mathbf{x}}\approx S_{\mathbf{X}=\mathbf{x}}$ (Fact 3.2). The
case $\varphi=\psi\vee\chi$ 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). Suppose $T\models^{g}\psi\vee\chi$. Then there are
$T_{0},T_{1}\subseteq T$ such that $T=T_{0}\cup T_{1}$, $T_{0}\models^{g}\psi$
and $T_{1}\models^{g}\chi$. Consider $S_{i}=\big{\\{}(s,\mathcal{F})\in
S\mid(s,\mathcal{F})\approx(s,\mathcal{G})\text{ for some }(s,\mathcal{G})\in
T_{i}\big{\\}}$ ($i=0,1$). It is not hard to see that $S_{i}\approx T_{i}$
($i=0,1$) and $S=S_{0}\cup S_{1}$. By induction hypothesis we have that
$S_{0}\models^{g}\psi$ and $S_{1}\models^{g}\chi$. Hence
$S\models^{g}\psi\vee\chi$. $\square$

###  3.2 Characterization of the function components

In this subsection we show that, up to dummy arguments, every system of
functions of signature $\sigma$ is definable in $\mathcal{CO}[\sigma]$. This
result is crucial for adapting the standard methods of team semantics to the
causal context.

For any function component $\mathcal{F}$ over $\sigma$, define a
$\mathcal{CO}[\sigma]$-formula

$\displaystyle\Phi^{\mathcal{F}}:=\bigwedge_{V\in\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})}\eta_{\sigma}(V)\land\bigwedge_{V\notin\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})}\xi_{\sigma}(V).$

where

$\displaystyle\eta_{\sigma}(V):=\bigwedge\big{\\{}$
$\displaystyle(\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{p})\boxright V=\mathcal{F}_{V}(\mathbf{p})$
$\displaystyle\quad\quad\mid\mathbf{W}=\mathrm{Dom}\setminus(PA_{V}^{\mathcal{F}}\cup\\{V\\}),~{}\mathbf{w}\in\mathrm{Ran}(\mathbf{W}),~{}\mathbf{p}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}})\big{\\}}$
$\displaystyle\text{and }~{}\xi_{\sigma}(V):=\bigwedge\big{\\{}$
$\displaystyle V=v\supset(\mathbf{W}_{V}=\mathbf{w}\boxright V=v)$
$\displaystyle\quad\quad\quad\quad\quad\quad\quad\mid
v\in\mathrm{Ran}(V),\mathbf{W}_{V}=\mathrm{Dom}\setminus\\{V\\},\mathbf{w}\in\mathrm{Ran}(\mathbf{W}_{V})\big{\\}}.$

Intuitively, for each non-constant endogenous variable $V$ of $\mathcal{F}$,
the formula $\eta_{\sigma}(V)$ specifies that all assignments in the
(generalized) causal team $T$ in question behave exactly as required by the
function $\mathcal{F}_{V}$. For each variable $V$ which, according to
$\mathcal{F}$, is exogenous or generated by a constant function, the formula
$\xi_{\sigma}(V)$ states that $V$ is not affected by interventions on other
variables. Notice that, if $V\in\mathrm{Cn}(\mathcal{F})$, then $V$ has a
$\xi$ but not an $\eta$ 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 $\mathcal{F}\in\mathbb{F}_{\sigma}$ be a function component over some
signature $\sigma$.

  1. (i)

For any generalized causal team $T$ over $\sigma$, we have that

$T\models^{g}\Phi^{\mathcal{F}}\iff\text{for all }(s,\mathcal{G})\in
T:\mathcal{G}\sim\mathcal{F}\iff T^{\mathcal{F}}=T.$

  2. (ii)

For any nonempty causal team $T=(T^{-},\mathcal{G})$ over $\sigma$, we have
that

$T\models^{c}\Phi^{\mathcal{F}}\iff\mathcal{G}\sim\mathcal{F}.$

#### Proof.

(i). The second “$\iff$” clearly holds. We now show the first “$\iff$”. If
$T=\emptyset$, the equivalence holds by the empty team property. Now assume
that $T\neq\emptyset$.

$\Longrightarrow$: Suppose $T\models^{g}\Phi^{\mathcal{F}}$ and
$(s,\mathcal{G})\in T$. We show that then $\mathcal{G}\sim\mathcal{F}$.
$\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})\subseteq\mathrm{En}(\mathcal{G})\setminus\mathrm{Cn}(\mathcal{G})$:
For any $V\in\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$, there
are distinct
$\mathbf{p},\mathbf{p}^{\prime}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}})$ such
that $\mathcal{F}_{V}(\mathbf{p})\neq\mathcal{F}_{V}(\mathbf{p}^{\prime})$.
Since $T\models\eta_{\sigma}(V)$, for any $\mathbf{w}\in Ran(\mathbf{W})$, we
have that

$\begin{array}[]{l}\\{(s,\mathcal{G})\\}\models(\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{p})\boxright V=\mathcal{F}_{V}(\mathbf{p}),\\\
\\{(s,\mathcal{G})\\}\models(\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{p}^{\prime})\boxright
V=\mathcal{F}_{V}(\mathbf{p}^{\prime}).\end{array}$

where $\mathbf{W}=\mathrm{Dom}\setminus({PA_{V}^{\mathcal{F}}\cup\\{V\\}})$.
Thus,

$s^{\mathcal{G}}_{\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{p}}(V)=\mathcal{F}_{V}(\mathbf{p})\neq\mathcal{F}_{V}(\mathbf{p}^{\prime})=s^{\mathcal{G}}_{\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{p}^{\prime}}(V).$

So, $V$ is neither in $\mathrm{Cn}(\mathcal{G})$ nor exogenous (since the
value of such variables is not affected by interventions on different
variables). Thus,
$V\in\mathrm{En}(\mathcal{G})\setminus\mathrm{Cn}(\mathcal{G})$.

$\mathrm{En}(\mathcal{G})\setminus\mathrm{Cn}(\mathcal{G})\subseteq\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$:
For any $V\in\mathrm{En}(\mathcal{G})\setminus\mathrm{Cn}(\mathcal{G})$, there
are distinct $\mathbf{p},\mathbf{p}^{\prime}\in Ran(PA_{V}^{\mathcal{G}})$
such that
$\mathcal{G}_{V}(\mathbf{p})\neq\mathcal{G}_{V}(\mathbf{p}^{\prime})$. Now, if
$V\notin\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$, then
$T\models\xi_{\sigma}(V)$. Let $v=s(V)$ and
$\mathbf{Z}=\mathbf{W}_{V}\setminus PA_{V}^{\mathcal{G}}$. Since
$\\{(s,\mathcal{G})\\}\models V=v$ and $V\notin PA_{V}^{\mathcal{G}}$, for any
$\mathbf{z}\in\mathrm{Ran}(\mathbf{Z})$, we have that

$\begin{array}[]{l}\\{(s,\mathcal{G})\\}\models(\mathbf{Z}=\mathbf{z}\land
PA_{V}^{\mathcal{G}}=\mathbf{p})\boxright V=v,\\\
\\{(s,\mathcal{G})\\}\models(\mathbf{Z}=\mathbf{z}\land
PA_{V}^{\mathcal{G}}=\mathbf{p}^{\prime})\boxright V=v.\end{array}$

By the definition of intervention, we must have that

$v=s^{\mathcal{G}}_{\mathbf{Z}=\mathbf{z}\land
PA_{V}^{\mathcal{G}}=\mathbf{p}}(V)=\mathcal{G}_{V}(\mathbf{p})\neq\mathcal{G}_{V}(\mathbf{p}^{\prime})=s^{\mathcal{G}}_{\mathbf{Z}=\mathbf{z}\land
PA_{V}^{\mathcal{G}}=\mathbf{p}^{\prime}}(V)=v,$

which is impossible. Hence,
$V\in\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$.

$\mathcal{F}_{V}\sim\mathcal{G}_{V}$ for any
$V\in\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$: Since
$T\models\eta_{\sigma}(V)$ and $V\notin PA_{V}^{\mathcal{G}}$, for all
$\mathbf{x}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}}\cap PA_{V}^{\mathcal{G}})$,
$\mathbf{y}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}}\setminus
PA_{V}^{\mathcal{G}})$,
$\mathbf{z}\in\mathrm{Ran}(PA_{V}^{\mathcal{G}}\setminus
PA_{V}^{\mathcal{F}})$ and $\mathbf{w}\in\mathrm{Ran}(\mathbf{W})$ with
$\mathbf{w}\upharpoonright(PA_{V}^{\mathcal{G}}\setminus
PA_{V}^{\mathcal{F}})=\mathbf{z}$ we have that

$\\{(s,\mathcal{G})\\}\models(\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{x}\mathbf{y})\boxright
V=\mathcal{F}_{V}(\mathbf{x}\mathbf{y}).$

Note that $(\mathcal{G}_{\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{x}\mathbf{y}})_{V}=\mathcal{G}_{V}$, as
$V\notin\mathbf{W}\cup PA_{V}^{\mathcal{F}}$. Thus,

$\mathcal{F}_{V}(\mathbf{x}\mathbf{y})=s^{\mathcal{G}}_{\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{x}\mathbf{y}}(V)=\mathcal{G}_{V}(s^{\mathcal{G}}_{\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{x}\mathbf{y}}(PA_{V}^{\mathcal{G}}))=\mathcal{G}_{V}(\mathbf{x}\mathbf{z}),$

as required.

$\Longleftarrow$: Suppose that $\mathcal{G}\sim\mathcal{F}$ for all
$(s,\mathcal{G})\in T$. Since the formula $\Phi^{\mathcal{F}}$ is flat, it
suffices to show that $\\{(s,\mathcal{G})\\}\models\eta_{\sigma}(V)$ for all
$V\in\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$, and
$\\{(s,\mathcal{G})\\}\models\xi_{\sigma}(V)$ for all
$V\notin\mathrm{En}(\mathcal{F}))\setminus\mathrm{Cn}(\mathcal{F})$.

For the former, take any $\mathbf{w}\in\mathrm{Ran}(\mathbf{W})$ and
$\mathbf{p}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}})$, and let
$\mathbf{Z}=\mathbf{z}$ abbreviate $\mathbf{W}=\mathbf{w}\land
PA_{V}^{\mathcal{F}}=\mathbf{p}$. We show that
$\\{(s_{\mathbf{Z}=\mathbf{z}},\mathcal{G}_{\mathbf{Z}=\mathbf{z}})\\}\models
V=\mathcal{F}_{V}(\mathbf{p})$. Since $\mathcal{G}\sim\mathcal{F}$, by Fact
3.2 we have that
$\mathcal{G}_{\mathbf{Z}=\mathbf{z}}\sim\mathcal{F}_{\mathbf{Z}=\mathbf{z}}$.
Thus,

$\begin{array}[]{rlr}s^{\mathcal{G}}_{\mathbf{Z}=\mathbf{z}}(V)=(\mathcal{G}_{\mathbf{Z}=\mathbf{z}})_{V}(s^{\mathcal{G}}_{\mathbf{Z}=\mathbf{z}}(PA_{V}^{\mathcal{G}_{\mathbf{Z}=\mathbf{z}}}))&=(\mathcal{F}_{\mathbf{Z}=\mathbf{z}})_{V}(s^{\mathcal{G}}_{\mathbf{Z}=\mathbf{z}}(PA_{V}^{\mathcal{F}_{\mathbf{Z}=\mathbf{z}}}))&(\text{since
}\mathcal{G}_{\mathbf{X}=\mathbf{x}}\sim\mathcal{F}_{\mathbf{X}=\mathbf{x}})\\\
&=\mathcal{F}_{V}(s^{\mathcal{G}}_{\mathbf{Z}=\mathbf{z}}(PA_{V}^{\mathcal{F}}))&(\text{since
}V\notin\mathbf{Z})\\\ &=\mathcal{F}_{V}(\mathbf{p}).&\end{array}$

For the latter, take any $v\in\mathrm{Ran}(V)$ and
$\mathbf{w}\in\mathrm{Ran}(\mathbf{W}_{V})$. Assume that
$\\{(s,\mathcal{G})\\}\models V=v$, i.e., $s(V)=v$. Since
$V\notin\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$ and
$\mathcal{F}\sim\mathcal{G}$, we know that $V\notin\mathrm{En}(\mathcal{G})$
or $V\in\mathrm{Cn}(\mathcal{G})$. In both cases we have that
$\\{(s,\mathcal{G})\\}\models\mathbf{W}_{V}=\mathbf{w}\boxright V=v$.

(ii). 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).
$\square$

We call a generalized causal team $T$ uniform if for all
$(s,\mathcal{F}),(t,\mathcal{G})\in T$, $\mathcal{F}\sim\mathcal{G}$. In
particular, the empty team $\emptyset$ is uniform. Uniformity is easily
definable in
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ by using
the characterizing formulas $\Phi^{\mathcal{F}}$ of the various function
components.

######  Corollary 3.5.

For any generalized causal team $T$ over some signature $\sigma$,

$\displaystyle
T\models^{g}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}\iff
T\text{ is uniform}.$

For any causal team $T=(T^{-},\mathcal{F})$, the associated generalized causal
team $T^{g}=$ $=\\{(s,\mathcal{F})\mid s\in T^{-}\\}$ is clearly uniform. It
thus follows from Lemma 2.16(i) that the formula
$\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}$
is valid in causal team semantics.

######  Corollary 3.6.

$\models^{c}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}$.

Furthermore, we now show that the two entailment relations $\models^{g}$ and
$\models^{c}$ are equivalent modulo the formula that defines uniformity.

######  Lemma 3.7.

For any set $\Gamma\cup\\{\psi\\}$ of $\mathcal{CO}[\sigma]$\- or
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$\-
or $\mathcal{COD}[\sigma]$-formulas,

$\displaystyle\Gamma\models^{c}\psi\iff\displaystyle\Gamma,\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}\models^{g}\psi.$

#### Proof.

$\Longleftarrow$: Suppose $T\models^{c}\Gamma$ for some causal team $T$.
Consider the generalized causal team $T^{g}$ generated by $T$. By Lemma
2.16(i), $T^{g}\models^{g}\Gamma$. Since $T^{g}$ is uniform, Corollary 3.5
gives that
$T^{g}\models^{g}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}$.
Then, by assumption, we obtain that $T^{g}\models^{g}\psi$, which, by Lemma
2.16(i) again, implies that $T\models^{c}\psi$.

$\Longrightarrow$: Suppose $T\models^{g}\Gamma$ and
$T\models^{g}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}$
for some generalized causal team $T$. If $T=\emptyset$, then
$T\models^{g}\psi$ by the empty team property. Now assume that
$T\neq\emptyset$. By Corollary 3.5 we know that $T$ is uniform. Pick
$(t,\mathcal{F})\in T$. Consider the generalized causal team
$S=\\{(s,\mathcal{F})\mid s\in T^{-}\\}$. Observe that $T\approx S$. Thus, by
Theorem 3.3, we have that $S\models^{g}\Gamma$, which further implies, by
Lemma 2.16(ii), that $S^{c}\models^{c}\Gamma$. Hence, by the assumption we
conclude that $S^{c}\models^{c}\psi$. Since $(S^{c})^{g}=S\approx T$, by
applying Lemma 2.16(ii) and Theorem 3.3 again, we obtain $T\models^{g}\psi$.
$\square$

The $\Phi^{\mathcal{F}}$ formulas also help us in understanding the behaviour
of the global disjunction
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$ 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.,
$\models\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$
implies $\models\varphi$ or $\models\psi$. It follows immediately from Theorem
3.4 that the disjunction property of
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$ fails in the
context of causal teams, because
$\models^{c}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}$,
whereas $\not\models^{c}\Phi^{\mathcal{F}}$ for any
$\mathcal{F}\in\mathbb{F}_{\sigma}$. Nevertheless, the global disjunction does
admit the disjunction property over generalized causal teams.

######  Theorem 3.8 (Disjunction property).

Let $\Delta$ be a set of $\mathcal{CO}[\sigma]$-formulas, and $\varphi,\psi$
be arbitrary formulas over $\sigma$. If
$\Delta\models^{g}\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$,
then $\Delta\models^{g}\varphi$ or $\Delta\models^{g}\psi$. In particular, if
$\models^{g}\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$,
then $\models^{g}\varphi$ or $\models^{g}\psi$.

#### Proof.

Suppose $\Delta\not\models^{g}\varphi$ and $\Delta\not\models^{g}\psi$. Then
there are two generalized causal teams $T_{1},T_{2}$ such that
$T_{1}\models\Delta$, $T_{2}\models\Delta$, $T_{1}\not\models\varphi$ and
$T_{2}\not\models\psi$. Let $T:=T_{1}\cup T_{2}$. By flatness of $\Delta$, we
have that $T\models\Delta$. On the other hand, by downwards closure, we have
that $T\not\models\varphi$ and $T\not\models\psi$, and thus
$T\not\models\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$.
$\square$

Regarding causal team semantics (an _not_ the generalized semantics) there is
another peculiarity in the behaviour of the global disjunction
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$: when
applied to causally incompatible formulas, the global disjunction
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$ “collapses”
to tensor disjunction $\vee$. We say that two formulas $\varphi$ and $\psi$ in
$\mathcal{COD}[\sigma]$ or
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
are (causally) incompatible if, for all nonempty causal teams
$S=(S^{-},\mathcal{F})$ and $T=(T^{-},\mathcal{G})$,

$S\models\varphi\text{ and
}T\models\psi\implies\mathcal{F}\not\sim\mathcal{G}.$

For instance, it follows immediately from Theorem 3.4 that the formulas
$\Phi^{\mathcal{F}}$ and $\Phi^{\mathcal{G}}$ are incompatible when
$\mathcal{F}\not\sim\mathcal{G}$. The key formula in Corollary 3.5,
$\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}$,
is thus a global disjunction of pairwise incompatible formulas
$\Phi^{\mathcal{F}}$. By the result below, we will have
$\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}\equiv^{c}\bigvee_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}$,
although the same result does not apply to generalized causal teams (as
$\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}\not\equiv^{g}\bigvee_{\mathcal{F}\in\mathbb{F}_{\sigma}}\Phi^{\mathcal{F}}$).

######  Lemma 3.9.

For any set $\\{\varphi_{i}\mid i\in I\\}$ of pairwise incompatible
$\mathcal{COD}[\sigma]$\- or
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$-formulas,
we have that
$\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{i\in
I}\varphi_{i}\equiv^{c}\bigvee_{i\in I}\varphi_{i}.$

#### Proof.

The left-to-right entailment follows easily from the empty team property. Let
us now show the right-to-left entailment. Suppose $T\models^{c}\bigvee_{i\in
I}\varphi_{i}$. If $T=\emptyset$, then
$T\models^{c}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{i\in
I}\varphi_{i}$ by the empty team property. Now assume that $T\neq\emptyset$.
Then there are causal subteams $S_{i}=(S_{i}^{-},\mathcal{F})$ of $T$ such
that $\bigcup_{i\in I}S_{i}^{-}=T^{-}$ and $S_{i}\models\varphi_{i}$ for each
$i\in I$. Since $T^{-}\neq\emptyset$, at least one $S_{i}$ is nonempty. If
both $S_{i}=(S_{i}^{-},\mathcal{F})$ and $S_{j}=(S_{j}^{-},\mathcal{F})$ were
nonempty ($i\neq j$), then since $\varphi_{i}$ and $\varphi_{j}$ are
incompatible, we would have that $\mathcal{F}\not\sim\mathcal{F}$; a
contradiction. Hence, we conclude that exactly one $S_{i}$ is nonempty, and
thus $S_{i}=T$. Therefore $T\models\varphi_{i}$, from which
$T\models\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}_{i\in
I}\varphi_{i}$ follows. $\square$

The above “collapse” does not only occur in causal team semantics; for a
simple example:
$\alpha\vee\alpha\equiv^{c/g}\alpha\equiv^{c/g}\alpha\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\alpha$
for any $\mathcal{CO}$-formula $\alpha$ (e.g., $\alpha=\Phi^{\mathcal{F}}$).
However, it easy to show that in the generalized (as well as in the non-
causal) team semantics, the entailment
$\varphi\lor\psi\models^{g}\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$
implies that $\varphi\models\psi$ or $\psi\models\varphi$ (provided $\varphi$
and $\psi$ are downward closed).131313For contraposition, suppose that
$\varphi\not\models\psi$ and $\psi\not\models\varphi$. Then there are
generalized causal teams $T,S$ such that
$T\models\varphi,T\not\models\psi,S\models\psi$ and $S\not\models\varphi$.
Thus, we conclude $T\cup S\models\varphi\vee\psi$ by definition, and $T\cup
S\not\models\varphi$ and $T\cup S\not\models\psi$ by the downward closure of
$\varphi$ and $\psi$. Hence
$\varphi\vee\psi\not\models\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$.
On the contrary, the equivalence
$\Phi^{\mathcal{F}}\vee\Phi^{\mathcal{G}}\equiv^{c}\Phi^{\mathcal{F}}\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\Phi^{\mathcal{G}}$,
for $\mathcal{F}\not\sim\mathcal{G}$, which holds in causal team semantics,
does not respect this necessary condition, as neither $\Phi^{\mathcal{F}}$
implies $\Phi^{\mathcal{G}}$ nor vice versa.

##  4 Characterizing $\mathcal{CO}$

In this section, we characterize the expressive power of $\mathcal{CO}$ over
causal teams. We also present a system of natural deduction for $\mathcal{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].

###  4.1 Expressivity

We show that $\mathcal{CO}$-formulas capture the flat class of (generalized)
causal teams, up to $\approx$-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.

######  Definition 4.1.

Let $S=(S^{-},\mathcal{F})$ and $T=(T^{-},\mathcal{G})$ be two causal teams
over the same signature $\sigma$ with $S\sim T$. The union of $S$ and $T$ is
defined as the causal team $S\cup T=(S^{-}\cup T^{-},\mathcal{H})$ over
$\sigma$, where

  * -

$\mathrm{En}(\mathcal{H})=\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})$

  * -

and for each $V\in\mathrm{En}(\mathcal{H})$,
$PA^{\mathcal{H}}_{V}=PA^{\mathcal{F}}_{V}\cap PA^{\mathcal{G}}_{V}$, and
$\mathcal{H}_{V}(\mathbf{p})=\mathcal{F}_{V}(\mathbf{p}\mathbf{x})$ for any
$\mathbf{p}\in PA_{V}^{\mathcal{F}}\cap PA_{V}^{\mathcal{G}}$ and
$\mathbf{x}\in PA_{V}^{\mathcal{F}}\setminus PA_{V}^{\mathcal{G}}$.

Clearly, $\mathcal{H}\sim\mathcal{F}\sim\mathcal{G}$ and thus $S\cup T\sim
S\sim T$. Let us also remark that even though the definition may seem to look
asymmetric as it appears to rely more on $\mathcal{F}$ than on $\mathcal{G}$
in its details, the notion of union is indeed well-defined, and it guarantees
that $S\cup T=T\cup S$. This is because the definition requires that
$\mathcal{F}\sim\mathcal{G}$, from which it follows that
$\mathrm{En}(\mathcal{H})=\mathrm{En}(\mathcal{F})\setminus\mathrm{Cn}(\mathcal{F})=\mathrm{En}(\mathcal{G})\setminus\mathrm{Cn}(\mathcal{G})$,
and also that
$\mathcal{H}_{V}(\mathbf{p})=\mathcal{F}_{V}(\mathbf{p}\mathbf{x})=\mathcal{G}_{V}(\mathbf{p}\mathbf{y})$
for any $\mathbf{p}\in PA_{V}^{\mathcal{F}}\cap PA_{V}^{\mathcal{G}}$,
$\mathbf{y}\in PA_{V}^{\mathcal{G}}\setminus PA_{V}^{\mathcal{F}}$ and
$\mathbf{x}\in PA_{V}^{\mathcal{F}}\setminus PA_{V}^{\mathcal{G}}$.

A formula $\varphi$ over a signature $\sigma$ determines a class
$\mathcal{K}_{\varphi}$ of (generalized) causal teams over $\sigma$ defined as

$\mathcal{K}_{\varphi}=\\{T\mid T\text{ has signature $\sigma$ and
}T\models\varphi\\}.$

We say that a formula $\varphi$ defines a class $\mathcal{K}$ of (generalized)
causal teams over $\sigma$ if $\mathcal{K}=\mathcal{K}_{\varphi}$.

######  Definition 4.2.

We say that a class $\mathcal{K}$ of (generalized) causal teams over $\sigma$
is

  * -

causally downward closed if $T\in\mathcal{K}$ and $S\subseteq T$ imply
$S\in\mathcal{K}$;

  * -

closed under causal unions if, whenever $T_{1},T_{2}\in\mathcal{K}$ and
$T_{1}\cup T_{2}$ is defined (which is always the case for generalized causal
teams), $T_{1}\cup T_{2}\in\mathcal{K}$;

  * -

flat if

    * (a)

(for causal teams) $(T^{-},\mathcal{F})\in\mathcal{K}$ iff
$(\\{s\\},\mathcal{F})\in\mathcal{K}$ for all $s\in T^{-}$;

    * (b)

(for generalized causal teams) $T\in\mathcal{K}$ iff
$\\{(s,\mathcal{F})\\}\in\mathcal{K}$ for all $(s,\mathcal{F})\in T$.

  * -

closed under equivalence if $T\in\mathcal{K}$ and $T\approx S$ imply
$S\in\mathcal{K}$.

######  Fact 4.3.

A class $\mathcal{K}$ of (generalized) causal teams over $\sigma$ is flat iff
$\mathcal{K}$ contains the empty team, is causally downward closed and closed
under causal unions.

The class $\mathcal{K}_{\varphi}$ is always nonempty as the empty team is
always in $\mathcal{K}_{\varphi}$ (by Theorem 2.15). By Theorems 2.15 and 3.3,
if $\alpha$ is a $\mathcal{CO}$-formula, then $\mathcal{K}_{\alpha}$ is flat
and closed under equivalence. The main result of this section is the following
characterization theorem which gives also the converse direction.

######  Theorem 4.4.

Let $\mathcal{K}$ be a nonempty class of (generalized) causal teams over some
signature $\sigma$. Then $\mathcal{K}$ is definable by a
$\mathcal{CO}[\sigma]$-formula if and only if $\mathcal{K}$ is flat and closed
under equivalence.

Before we present the proof of the theorem, let us first introduce a relation
$\preccurlyeq$ between causal teams that is of central use in this proof. For
any (generalized) causal teams $S$ and $T$, we write $S\preccurlyeq T$ if
$S\approx R\subseteq T$ for some (generalized) causal team $R$. In particular,
we stipulate $\emptyset\preccurlyeq T$ for all (generalized) causal teams $T$.

######  Fact 4.5.

A class $\mathcal{K}$ of (generalized) causal teams over $\sigma$ is causally
downward closed and closed under equivalence iff $\mathcal{K}$ is closed under
the relation $\succcurlyeq$, i.e., $T\in\mathcal{K}$ and $T\succcurlyeq S$
imply $S\in\mathcal{K}$.

We leave it for the reader to verify that $\preccurlyeq$ is a partial order
(modulo $\approx$); in particular, $S\preccurlyeq T$ and $T\preccurlyeq S$
imply $S\approx T$. The next lemma lists some other useful properties of the
relation $\preccurlyeq$, where recall that, for every generalized causal team
$T$, we define $T^{\mathcal{F}}=\\{(s,\mathcal{G})\in
T\mid\mathcal{G}\sim\mathcal{F}\\}$.

######  Lemma 4.6.

The following holds in the context of generalized causal teams:

  1. (i)

$S\preccurlyeq T\iff\\{(s,\mathcal{F})\\}\preccurlyeq T$ for all
$(s,\mathcal{F})\in S$.

  2. (ii)

If $T=T^{\mathcal{F}}$ is uniform and $S\preccurlyeq T$, then $S$ is also
uniform and $S=S^{\mathcal{F}}$.

  3. (iii)

If $S\preccurlyeq T$, then $S^{\mathcal{F}}\preccurlyeq T^{\mathcal{F}}$ for
all $\mathcal{F}\in\mathbb{F}_{\sigma}$.

  4. (iv)

If $S,T$ are causal teams, then $S\preccurlyeq T\iff S^{g}\preccurlyeq T^{g}$.

  5. (v)

If $S_{i}\preccurlyeq T_{i}$ ($i\in I$), then $\bigcup_{i\in
I}S_{i}\preccurlyeq\bigcup_{i\in I}T_{i}$

  6. (vi)

If $S\preccurlyeq\bigcup_{i\in I}T_{i}$, then for every $i\in I$, there exists
$S_{i}\preccurlyeq T_{i}$ such that $S=\bigcup_{i\in 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}\approx R_{i}\subseteq T_{i}$ for
some $R_{i}$ ($i\in I$). Let $R=\bigcup_{i\in I}R_{i}$. Clearly,
$\bigcup_{i\in I}R_{i}\subseteq\bigcup_{i\in I}T_{i}$. It remains to show that
$S\approx R$ for $S=\bigcup_{i\in I}S_{i}$. For every
$\mathcal{F}\in\mathbb{F}_{\sigma}$ and every $i\in I$, since $S_{i}\approx
R_{i}$, we have that $(S_{i}^{\mathcal{F}})^{-}=(R_{i}^{\mathcal{F}})^{-}$.
Thus,

$(S^{\mathcal{F}})^{-}=\bigcup_{i\in I}(S_{i}^{\mathcal{F}})^{-}=\bigcup_{i\in
I}(R_{i}^{\mathcal{F}})^{-}=(R^{\mathcal{F}})^{-}.$

Now we prove (vi). By the assumption, there is an $R$ such that $S\approx
R\subseteq T=\bigcup_{i\in I}T_{i}$. For every $i\in I$, define $R_{i}:=R\cap
T_{i}$ and

$S_{i}:=\\{(s,\mathcal{F})\in S\mid\\{(s,\mathcal{F})\\}\preccurlyeq
R_{i}\\}.$

Clearly, $R_{i}\subseteq T_{i}$. To see that $S_{i}\preccurlyeq T_{i}$, it
remains to verify that $S_{i}\approx R_{i}$. For any
$\mathcal{F}\in\mathbb{F}_{\sigma}$, we have that

$\displaystyle s\in(S_{i}^{\mathcal{F}})^{-}$
$\displaystyle\iff(s,\mathcal{G})\in S_{i}\text{ for some
}\mathcal{G}\sim\mathcal{F}\iff\\{(s,\mathcal{G})\\}\preccurlyeq R_{i}\text{
for some }\mathcal{G}\sim\mathcal{F}$
$\displaystyle\iff\\{(s,\mathcal{G})\\}\preccurlyeq R_{i}^{\mathcal{F}}\text{
for some }\mathcal{G}\sim\mathcal{F}\iff s\in(R_{i}^{\mathcal{F}})^{-}.$

Finally, we show that $S=\bigcup_{i\in I}S_{i}$. By definition,
$S_{i}\subseteq S$ for every $i\in I$. Conversely, for every
$(s,\mathcal{F})\in S$, since $S\approx R$, we have by item (i) that

$\\{(s,\mathcal{F})\\}\preccurlyeq R=R\cap T=\bigcup_{i\in I}(R\cap
T_{i})=\bigcup_{i\in I}R_{i}.$

Thus, $\\{(s,\mathcal{F})\\}\preccurlyeq R_{i}$ for some $i\in I$. Hence, by
definition, $(s,\mathcal{F})\in S_{i}$. $\square$

We will next introduce a formula that characterizes the relation
$\preccurlyeq$ in a certain sense. An important part of this characterizing
formula is a $\mathcal{CO}[\sigma]$-formula $\Theta^{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
$\sigma=(\mathrm{Dom},\mathrm{Ran})$, define

$\displaystyle\Theta^{T^{-}}:=\bigvee_{s\in
T^{-}}\bigwedge_{V\in\mathrm{Dom}}V=s(V).$

Note that if $T^{-}=\emptyset$, then $\Theta^{T^{-}}=\bigvee\emptyset\ =\
\bot$.

######  Lemma 4.7.

For any (generalized) causal teams $S$ and $T$ over $\sigma$, we have that
$S\models\Theta^{T^{-}}\iff S^{-}\subseteq T^{-}$.

#### Proof.

We only give detailed proof for the statement for causal teams; the
generalized causal team case is analogous.

“$\Longrightarrow$”: Suppose $S\models\Theta^{T^{-}}$ and
$S=(S^{-},\mathcal{F})$. For any $s\in S^{-}$, by downward closure, we have
that $(\\{s\\},\mathcal{F})\models\Theta^{T^{-}}$, which means that for some
$t\in T^{-}$, $(\\{s\\},\mathcal{F})\models V=t(V)$ for all
$V\in\mathrm{Dom}$. This implies that $s=t\in T^{-}$.

“$\Longleftarrow$”: Suppose $S^{-}\subseteq T^{-}$. Observe that
$S\models\Theta^{S^{-}}$ and
$\Theta^{T^{-}}=\Theta^{S^{-}}\vee\Theta^{T^{-}\setminus S^{-}}$. Thus, we
conclude $S\models\Theta^{T^{-}}$ by the empty team property. $\square$

Next, we show that the formula $\Theta^{T^{-}}\wedge\Phi^{\mathcal{F}}$
defines the property of being in the $\preccurlyeq$ relation with a uniform
generalized causal team $T=T^{\mathcal{F}}$ or a causal team
$(T^{-},\mathcal{F})$.

######  Lemma 4.8.

  1. (i)

Let $S$ and $T$ be generalized causal teams over $\sigma$. If
$T=T^{\mathcal{F}}$ is uniform, then
$S\models^{g}\Theta^{T^{-}}\wedge\Phi^{\mathcal{F}}\iff S\preccurlyeq T.$

  2. (ii)

For any causal teams $S=(S^{-},\mathcal{G})$ and $T=(T^{-},\mathcal{F})$ over
$\sigma$, we have that $S\models^{c}\Theta^{T^{-}}\wedge\Phi^{\mathcal{F}}\iff
S\preccurlyeq T.$

#### Proof.

(i) If $S=\emptyset$, then
$\emptyset\models^{g}\Theta^{T^{-}}\wedge\Phi^{\mathcal{F}}$ by the empty team
property, and $\emptyset\preccurlyeq T$ by stipulation. If $T=\emptyset$, then
$\Theta^{T^{-}}=\bigvee\emptyset=\bot$, and thus
$\Theta^{T^{-}}\wedge\Phi^{\mathcal{F}}\equiv\bot$. Obviously,
$S\models^{g}\bot$ iff $S=\emptyset$ iff $S\preccurlyeq\emptyset=T$. Now
assume that $S,T\neq\emptyset$.

“$\Longrightarrow$”: Consider $R=\\{(s,\mathcal{G})\in T\mid s\in
S^{-}\\}\subseteq T.$ It suffices to show that $S\approx R$, i.e.,
$(S^{\mathcal{G}})^{-}=(R^{\mathcal{G}})^{-}$ for all
$\mathcal{G}\in\mathbb{F}_{\sigma}$. If $\mathcal{G}\not\sim\mathcal{F}$,
since $T=T^{\mathcal{F}}$ we have that
$(R^{\mathcal{G}})^{-}\subseteq(T^{\mathcal{G}})^{-}=\emptyset$. On the other
hand, since $S\models\Phi^{\mathcal{F}}$, by Theorem 3.4 we must have that
$(S^{\mathcal{G}})^{-}=\emptyset$. Thus,
$(R^{\mathcal{G}})^{-}=\emptyset=(S^{\mathcal{G}})^{-}$. Now, if
$\mathcal{G}\sim\mathcal{F}$, then $R^{\mathcal{G}}=R^{\mathcal{F}}=R$, since
$R\subseteq T=T^{\mathcal{F}}$. As $S\models\Theta^{T^{-}}$, by Lemma 4.7 we
have that $S^{-}\subseteq T^{-}$, which, by definition of $R$, implies that
$R^{-}=S^{-}$. Moreover, since $S\models\Phi^{\mathcal{F}}$, by Theorem 3.4 we
have that $S=S^{\mathcal{F}}=S^{\mathcal{G}}$. Thus, we conclude that
$(S^{\mathcal{G}})^{-}=S^{-}=R^{-}=(R^{\mathcal{G}})^{-}$.

“$\Longleftarrow$”: Suppose $S\approx R\subseteq T=T^{\mathcal{F}}$. Then
$R^{\mathcal{F}}=R\approx S$. It follows by Lemma 4.6(ii) that
$S^{\mathcal{F}}=S$ and
$S^{-}=(S^{\mathcal{F}})^{-}=(R^{\mathcal{F}})^{-}=R^{-}\subseteq T^{-}$.
Thus, by Theorem 3.4 and Lemma 4.7 we obtain that
$S\models\Phi^{\mathcal{F}}\wedge\Theta^{T^{-}}$.

(ii) Observe that the generalized causal team $T^{g}=\\{(s,\mathcal{F})\mid
s\in T^{-}\\}$ associated with $T$ is uniform, $T^{g}=(T^{g})^{\mathcal{F}}$
and $T^{-}=(T^{g})^{-}$. Thus, by Lemma 2.16(i), item (i) and Lemma 4.6(iv),

$S\models^{c}\Theta^{T^{-}}\wedge\Phi^{\mathcal{F}}\iff
S^{g}\models^{g}\Theta^{(T^{g})^{-}}\wedge\Phi^{\mathcal{F}}\iff
S^{g}\preccurlyeq T^{g}\iff S\preccurlyeq T.$

$\square$

######  Corollary 4.9.

For any generalized causal teams $S$ and $T$ over $\sigma$, we have that

$S\models\bigvee_{\mathcal{F}\in\mathbb{F}_{\sigma}}(\Theta^{(T^{\mathcal{F}})^{-}}\wedge\Phi^{\mathcal{F}})\iff
S\preccurlyeq T.$

#### Proof.

Put
$\displaystyle\psi=\bigvee_{\mathcal{F}\in\mathbb{F}_{\sigma}}(\Theta^{(T^{\mathcal{F}})^{-}}\wedge\Phi^{\mathcal{F}})$.
If $T=\emptyset$, then $T^{\mathcal{F}}=\emptyset$ for all
$\mathcal{F}\in\mathbb{F}_{\sigma}$, so that
$\Theta^{(T^{\mathcal{F}})^{-}}\equiv^{g}\bot$ and thus $\psi\equiv^{g}\bot$.
Then, $S\models\psi$ iff $S=\emptyset$ iff $S\preccurlyeq\emptyset=T$.

Now, assume that $T\neq\emptyset$. For each
$\mathcal{F}\in\mathbb{F}_{\sigma}$, the team $T^{\mathcal{F}}$ is uniform.
Thus,

$\displaystyle
S\models\bigvee_{\mathcal{F}\in\mathbb{F}_{\sigma}}(\Theta^{(T^{\mathcal{F}})^{-}}\wedge\Phi^{\mathcal{F}})$
$\displaystyle\iff$
$\displaystyle\forall\mathcal{F}\in\mathbb{F}_{\sigma}\exists
S_{\mathcal{F}}:S=\bigcup_{\mathcal{F}\in\mathbb{F}_{\sigma}}S_{\mathcal{F}}\text{
and each
}S_{\mathcal{F}}\models\Theta^{(T^{\mathcal{F}})^{-}}\wedge\Phi^{\mathcal{F}}$
$\displaystyle\iff$
$\displaystyle\forall\mathcal{F}\in\mathbb{F}_{\sigma}\exists
S_{\mathcal{F}}:S=\bigcup_{\mathcal{F}\in\mathbb{F}_{\sigma}}S_{\mathcal{F}}\text{
and each }S_{\mathcal{F}}\preccurlyeq T^{\mathcal{F}}$ (by Lemma 4.8)
$\displaystyle\iff$ $\displaystyle S\preccurlyeq T.$ (by Lemma 4.6(v,vi),
since $\displaystyle
T=\bigcup_{\mathcal{F}\in\mathbb{F}_{\sigma}}T^{\mathcal{F}}$)

$\square$

We are now ready to prove the main theorem of the section.

#### Proof of Theorem 4.4

It suffices to prove the direction “$\Longleftarrow$”. We first consider the
generalized causal team case. Let $\mathcal{K}$ be a nonempty class of
generalized causal teams that is flat and closed under equivalence. Put
$T=\bigcup\mathcal{K}$. Since $\mathcal{K}$ is closed under unions,
$T\in\mathcal{K}$. Consider the $\mathcal{CO}[\sigma]$-formula

$\varphi=\bigvee_{\mathcal{F}\in\mathbb{F}_{\sigma}}(\Theta^{(T^{\mathcal{F}})^{-}}\land\Phi^{\mathcal{F}}).$

We show that $\mathcal{K}_{\varphi}=\mathcal{K}$. For any generalized causal
team $S$, we first deduce, by applying Corollary 4.9 that

$S\in\mathcal{K}_{\varphi}\iff S\models^{g}\varphi\iff
S\preccurlyeq\bigcup\mathcal{K}.$

Now assume $S\in\mathcal{K}_{\varphi}$; since then
$S\preccurlyeq\bigcup\mathcal{K}$, and since
$\bigcup\mathcal{K}\in\mathcal{K}$ and $\mathcal{K}$ is closed under
$\succcurlyeq$, we have that $S\in\mathcal{K}$, which gives
$\mathcal{K}_{\varphi}\subseteq\mathcal{K}$. Conversely, if $S\in\mathcal{K}$,
then obviously $S\approx S\subseteq\bigcup\mathcal{K}$, namely,
$S\preccurlyeq\bigcup\mathcal{K}$, from which we conclude that
$S\in\mathcal{K}_{\varphi}$.

Next, we consider the causal team case. Let $\mathcal{K}$ be a nonempty class
of causal teams that is flat and closed under equivalence. For each
$\mathcal{F}\in\mathbb{F}_{\sigma}$, let

$(T_{\mathcal{F}})^{-}=\bigcup\\{T^{-}\mid(T^{-},\mathcal{G})\in\mathcal{K}\text{
for some }\mathcal{G}\sim\mathcal{F}\\}.$

Since $\mathcal{K}$ is closed under unions and equivalence,
$((T_{\mathcal{F}})^{-},\mathcal{F})\in\mathcal{K}$. Consider the generalized
causal team $T=\bigcup\mathcal{K}^{g}$, where $\mathcal{K}^{g}=\\{T^{g}\mid
T\in\mathcal{K}\\}$. Observe that
$(T^{\mathcal{F}})^{-}=(T_{\mathcal{F}})^{-}$. Consider the above-defined
$\mathcal{CO}[\sigma]$-formula $\varphi$ with respect to the generalized
causal team $T$. Thus, $\mathcal{K}_{\varphi}=\mathcal{K}$ over causal teams,
since for any causal team $S=(S^{-},\mathcal{G})$,

$\displaystyle S\models^{c}\varphi$ $\displaystyle\iff
S^{g}\models^{g}\varphi$ (Lemma 2.16(i)) $\displaystyle\iff S^{g}\preccurlyeq
T$ (Corollary 4.9) $\displaystyle\iff S^{g}=(S^{g})^{\mathcal{G}}\preccurlyeq
T^{\mathcal{G}}$ (Lemma 4.6(iii)) $\displaystyle\iff
S\preccurlyeq((T_{\mathcal{G}})^{-},\mathcal{G})$ (by Lemma 4.6(iv), since
$(T^{\mathcal{G}})^{-}=(T_{\mathcal{G}})^{-}$) $\displaystyle\iff
S\in\mathcal{K}.$ (since $((T_{\mathcal{G}})^{-},\mathcal{G})\in\mathcal{K}$
and $\mathcal{K}$ is closed under $\succcurlyeq$)

$\square$

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 $\mathcal{CO}$
without the operator $\boxright$. We show that this language is _strictly_
less expressive than $\mathcal{CO}$ (and similarly for
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ and
$\mathcal{COD}$).

######  Lemma 4.10.

Let $\varphi$ be a
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
or $\mathcal{COD}[\sigma]$ formula without occurrences of $\boxright$. For any
(generalized) causal teams $T,S$ over $\sigma$ with $T^{-}=S^{-}$,
$T\models\varphi\iff S\models\varphi$.

#### Proof.

By a straightforward induction on $\varphi$. $\square$

######  Proposition 4.11.

Let $\sigma=(\mathrm{Dom},\mathrm{Ran})$ be a signature such that
$|\mathrm{Ran}(V)|\geq 2$ for at least one variable $V\in\mathrm{Dom}$. Then
there is a class of (generalized) causal teams that is definable by a
$\mathcal{CO}[\sigma]$ formula, but not definable by any
$\mathcal{CO}[\sigma]$ formula without occurrences of $\boxright$.

#### Proof.

Let $(s,\mathcal{F})\in\mathbb{S}\mathbbm{em}_{\sigma}$. Consider the class of
generalized causal teams
$\mathcal{K}=\wp(\\{(s,\mathcal{G})\mid\mathcal{G}\sim\mathcal{F}\\})$. This
class is flat and closed under equivalence, so by Theorem 4.4 it is definable
by a formula of $\mathcal{CO}[\sigma]$. On the other hand, observe that, given
the cardinality assumption on $\sigma$, there is an
$\mathcal{H}\in\mathbb{F}_{\sigma}$ such that
$\mathcal{H}\not\sim\mathcal{F}$. Now,
$\\{(s,\mathcal{H})\\}\notin\mathcal{K}$ and also
$\\{(s,\mathcal{F})\\}\in\mathcal{K}$. For any formula $\theta$ of
$\mathcal{CO}[\sigma]$ without occurrences of $\boxright$, by Lemma 4.10, we
have that $\\{(s,\mathcal{H})\\}\models\theta$ iff
$\\{(s,\mathcal{F})\\}\models\theta$, that is,
$\\{(s,\mathcal{H})\\}\in\mathcal{K}_{\theta}$ iff
$\\{(s,\mathcal{F})\\}\in\mathcal{K}_{\theta}$. Hence,
$\mathcal{K}_{\theta}\neq\mathcal{K}$.

For causal team semantics, we reason similarly by considering instead the
class of causal teams
$\mathcal{K}=\\{\emptyset\\}\cup\\{(\\{s\\},\mathcal{G})\mid\mathcal{G}\sim\mathcal{F}\\}$.
$\square$

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.141414On the other hand,
the quantifiers of _first-order_ team semantics act as dynamic operators, and
thus they allow, to some extent, to simulate the effect of interventions. This
is discussed in [2]. A further simple consequence of the above proposition is
the undefinability of $\boxright$ in terms of the other connectives (see [29,
8] for details on the notion of definability of connectives in the context of
team semantics).

###  4.2 Deduction system

The logic $\mathcal{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
$\boxright\textsf{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\leadsto Y$ (“$X$ causally affects
$Y$”) as an abbreviation for the $\mathcal{CO}[\sigma]$ formula:

$\displaystyle\bigvee\Big{\\{}\mathbf{Z}$
$\displaystyle=\mathbf{z}\boxright\big{(}(X=x\boxright
Y=y)\land(X=x^{\prime}\boxright Y=y^{\prime})\big{)}$
$\displaystyle\mid\mathbf{Z}\subseteq\mathrm{Dom}\setminus\\{X,Y\\},\mathbf{z}\in\mathrm{Ran}(\mathbf{Z}),x,x^{\prime}\in\mathrm{Ran}(X),y,y^{\prime}\in\mathrm{Ran}(Y),x\neq
x^{\prime},y\neq y^{\prime}\Big{\\}}.$

This formula states that there is some (possibly null) intervention
$do(\mathbf{Z}=\mathbf{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$.

######  Definition 4.12.

The system of natural deduction for $\mathcal{CO}[\sigma]$ consists of the
following rules:

  * -

(Parameterized) rules for value range assumptions:

ValDef $\bigvee_{x\in\mathrm{Ran}(X)}X=x$ |  $X=x$ ValUnq (for $x\neq x^{\prime}$) $X\neq x^{\prime}$
---|---

  * -

Rules for $\wedge,\vee,\neg$:

$\varphi$ $\psi$ $\wedge\textsf{I}$ $\varphi\wedge\psi$ |  $\varphi\wedge\psi$ $\wedge\textsf{E}$ $\varphi$ $\varphi\wedge\psi$ $\wedge\textsf{E}$ $\psi$
---|---
$\varphi$ $\vee\textsf{I}$ $\varphi\vee\psi$ $\varphi$ $\vee\textsf{I}$ $\psi\vee\varphi$ |  $\varphi\vee\psi$ $[\varphi]$ $\vdots$ $\alpha$ $[\psi]$ $\vdots$ $\alpha$ $\vee\textsf{E}$ $\alpha$
$[\alpha]$ $\vdots$ $\bot$ $\neg\textsf{I}$ $\neg\alpha$ $\alpha$ $\neg\alpha$ $\neg\textsf{E}$ $\varphi$ $[\neg\alpha]$ $\vdots$ $\bot$ RAA $\alpha$ |

  * -

Rules for $\boxright$:

$\boxright\\!\textsf{Eff}$ $(\mathbf{X}=\mathbf{x}\land Y=y)\boxright Y=y$
$\mathbf{X}=\mathbf{x}$ $\theta$ $\boxright\textsf{I}$ (1)
$\mathbf{X}=\mathbf{x}\boxright\theta$
---
$\textsf{ex falso}_{\boxright}$ (for $x\neq x^{\prime}$)
$(\mathbf{Y}=\mathbf{y}\land X=x\land X=x^{\prime})\boxright\varphi$
$\mathbf{X}=\mathbf{x}\boxright\bot$ $\boxright\\!\bot\textsf{E}$ (2)
$\varphi$
$\mathbf{X}=\mathbf{x}\boxright\varphi$ $[\mathbf{X}=\mathbf{x}]$ $D_{1}$
$\mathbf{Y}=\mathbf{y}$ $[\mathbf{Y}=\mathbf{y}]$ $D_{2}$
$\mathbf{X}=\mathbf{x}$ $\boxright\\!\\!\textsf{Rpl}_{A}$ (3)
$\mathbf{Y}=\mathbf{y}\boxright\varphi$
$\mathbf{X}=\mathbf{x}\boxright\varphi$ $[\varphi]$ $D$ $\psi$
$\boxright\\!\\!\textsf{Rpl}_{C}$ (3) $\mathbf{X}=\mathbf{x}\boxright\psi$
$\mathbf{X}=\mathbf{x}\boxright\varphi$ $\mathbf{X}=\mathbf{x}\boxright\psi$
$\boxright\\!\\!\wedge\textsf{I}$
$\mathbf{X}=\mathbf{x}\boxright\varphi\land\psi$
$\neg(\mathbf{X}=\mathbf{x}\boxright\alpha)$ $\neg\\!\boxright\\!\textsf{E}$
$\mathbf{X}=\mathbf{x}\boxright\neg\alpha$
$\mathbf{X}=\mathbf{x}\boxright(\mathbf{Y}=\mathbf{y}\boxright\varphi)$
$\boxright\\!\textsf{Extr}$ (4)
$(\mathbf{X^{\prime}}=\mathbf{x^{\prime}}\land\mathbf{Y}=\mathbf{y})\boxright\varphi$
$(\mathbf{X}=\mathbf{x}\land\mathbf{Y}=\mathbf{y})\boxright\varphi$
$\boxright\\!\textsf{Exp}$ (5)
$\mathbf{X}=\mathbf{x}\boxright(\mathbf{Y}=\mathbf{y}\boxright\varphi)$

$X_{1}\leadsto X_{2}\hskip 10.0pt\dots\hskip 10.0pt\dots\hskip
10.0ptX_{k-1}\leadsto X_{k}$ Recur $\neg(X_{k}\leadsto X_{1})$
(1) $\theta$ is $\boxright$-free. (2) $\mathbf{X}=\mathbf{x}$ is consistent.
(3) The derivations $D_{1},D_{2},D$ do not have any undischarged assumptions.
(4) $\mathbf{X}=\mathbf{x}$ is consistent,
$\mathbf{X^{\prime}}=\mathbf{X}\setminus\mathbf{Y}$,
$\mathbf{x^{\prime}}=\mathbf{x}\setminus\mathbf{y}$. (5)
$\mathbf{X}\cap\mathbf{Y}=\emptyset$.

Note that the above system is parametrized with the signature $\sigma$. We
write $\Gamma\vdash_{\sigma}\varphi$ (or simply $\Gamma\vdash\varphi$ when
$\sigma$ is clear from the context) if the formula $\varphi$ can be derived
from $\Gamma$ 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 $\boxright$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\in\mathbb{\mathbb{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.151515The possibility of expressing recursivity with infinite
signatures is suggested in a footnote of [17] and implemented as a rule in
[7]. Furthermore, the role of $\leadsto$ in the formulation of Recur could be
taken instead by the relation of _direct cause_ , as shown in [5]. Rule
$\boxright\textsf{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 $\boxright\\!\\!\land$I, $\boxright\\!\\!\lor$E and
$\neg\\!\boxright\\!\textsf{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 $\boxright$Extr (_Extraction_) and
$\boxright$Exp (_Exportation_) to remove or add occurrences of $\boxright$
from the consequents. A comment might be due concerning the notation used in
$\boxright$Extr. As $\mathbf{X}=\mathbf{x}$ abbreviates a conjunction of
equalities $X_{1}=x_{1}\land\dots\land X_{n}=x_{n}$, in the context of this
rule $\mathbf{X}^{\prime}=\mathbf{x}^{\prime}$ denotes the formula obtained
from $\mathbf{X}=\mathbf{x}$ after removing all conjuncts $X_{i}=x_{i}$ such
that the variable $X_{i}$ is in $\mathbf{Y}$. The four remaining rules,
$\boxright$RplA, $\boxright$RplC, $\textsf{ex falso}_{\boxright}$ and
$\boxright\\!\bot\textsf{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 $\alpha,\beta$; we do this to emphasize that these rules are
still sound for the extended languages $\mathcal{COD}$ and
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ only when
$\alpha,\beta$ are restricted to $\mathcal{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 $\mathcal{CO}[\sigma]$:

  1. (i)

$\alpha,\neg\alpha\vee\beta\vdash\beta$ (weak modus ponens)

  2. (ii)

$\mathbf{X}=\mathbf{x}\boxright Y=y\vdash\mathbf{X}=\mathbf{x}\boxright Y\neq
y^{\prime}$ (Uniqueness)

  3. (iii)

$\mathbf{X}=\mathbf{x}\boxright
W=w,\mathbf{X}=\mathbf{x}\boxright\theta\vdash(\mathbf{X}=\mathbf{x}\wedge
W=w)\boxright\theta$ whenever $\theta$ is $\boxright$-free (Composition)

  4. (iv)

$\mathbf{X}=\mathbf{x}\boxright\varphi\land\psi\vdash\mathbf{X}=\mathbf{x}\boxright\varphi$
(Extraction of conjuncts)

  5. (v)

If $\mathbf{X}=\mathbf{x}$ is consistent,
$\mathbf{X}=\mathbf{x}\boxright\neg\alpha\vdash\neg(\mathbf{X}=\mathbf{x}\boxright\alpha)$

  6. (vi)

$\mathbf{X}=\mathbf{x}\boxright\varphi\vee\psi\dashv\vdash(\mathbf{X}=\mathbf{x}\boxright\varphi)\vee(\mathbf{X}=\mathbf{x}\boxright\psi)$

  7. (vii)

$\bigvee_{y\in\mathrm{Ran}(Y)}(\mathbf{X}=\mathbf{x}\boxright Y=y)$
(Definiteness)

#### Proof.

Item (i) follows from $\neg\textsf{E}$ and $\vee\textsf{E}$. Items (ii),(iv)
follow from ValUnq, $\wedge\textsf{E}$ and $\boxright\\!\textsf{Rpl}_{C}$. For
item (v), we first derive by applying $\boxright\\!\wedge\textsf{I}$, and
$\boxright\\!\bot\textsf{E}$ that

$\mathbf{X}=\mathbf{x}\boxright\neg\alpha,\mathbf{X}=\mathbf{x}\boxright\alpha\vdash\mathbf{X}=\mathbf{x}\boxright\neg\alpha\wedge\alpha\vdash\mathbf{X}=\mathbf{x}\boxright\bot\vdash\bot$

Then, by $\neg\textsf{I}$ we conclude that
$\mathbf{X}=\mathbf{x}\boxright\neg\alpha\vdash\neg(\mathbf{X}=\mathbf{x}\boxright\alpha)$.

For item (iii), if $W\in\mathbf{X}$, then we derive
$\mathbf{X}=\mathbf{x}\boxright\theta\vdash(\mathbf{X}=\mathbf{x}\wedge
W=w)\boxright\theta$ by $\boxright\textsf{Rpl}_{A}$ (if $W=w$ is among
$\mathbf{X}=\mathbf{x}$) or $\textsf{ex falso}_{\boxright}$ (if $W=w^{\prime}$
is among $\mathbf{X}=\mathbf{x}$ for some $w^{\prime}\neq w$). Now assume
$W\notin\mathbf{X}$. Then we have that

$\displaystyle\mathbf{X}=\mathbf{x}\boxright
W=w,\mathbf{X}=\mathbf{x}\boxright\theta$ $\displaystyle\vdash~{}$
$\displaystyle\mathbf{X}=\mathbf{x}\boxright(W=w\wedge\theta)$ (by
$\boxright\wedge\textsf{I}$) $\displaystyle\vdash~{}$
$\displaystyle\mathbf{X}=\mathbf{x}\boxright(W=w\boxright\theta)$ (by
$\land\textsf{E},\boxright\textsf{I}$ and $\boxright\textsf{Rpl}_{C}$)
$\displaystyle\vdash~{}$ $\displaystyle(\mathbf{X}=\mathbf{x}\wedge
W=w)\boxright\theta.$ (by $\boxright\textsf{Extr}$)

For item (vi), we first consider the case that $\mathbf{X}=\mathbf{x}$ is
inconsistent. From right to left, we then have
$\vdash\mathbf{X}=\mathbf{x}\boxright\varphi\vee\psi$ by rule $\textsf{ex
falso}_{\boxright}$. From left to right, we can first derive
$\mathbf{X}=\mathbf{x}\boxright\varphi$ by $\textsf{ex falso}_{\boxright}$ and
then
$\vdash(\mathbf{X}=\mathbf{x}\boxright\varphi)\vee(\mathbf{X}=\mathbf{x}\boxright\psi)$
by $\vee\textsf{I}$. Now assume that $\mathbf{X}=\mathbf{x}$ is consistent.

For the right-to-left direction, first we derive

$\mathbf{X}=\mathbf{x}\boxright\varphi\vdash\mathbf{X}=\mathbf{x}\boxright\varphi\vee\psi\text{
and
}\mathbf{X}=\mathbf{x}\boxright\psi\vdash\mathbf{X}=\mathbf{x}\boxright\varphi\vee\psi$

by applying $\boxright\textsf{Rpl}_{C}$. Thus, by $\vee\textsf{E}$ we conclude
that
$(\mathbf{X}=\mathbf{x}\boxright\varphi)\vee(\mathbf{X}=\mathbf{x}\boxright\psi)\vdash$
$\vdash\mathbf{X}=\mathbf{x}\boxright\varphi\vee\psi$.

For the left-to-right direction, we first use De Morgan’s laws (which are
easily derivable in the usual way) plus $\boxright\\!\textsf{Rpl}_{C}$ to
derive from $\mathbf{X}=\mathbf{x}\boxright\varphi\lor\psi$ that
$\mathbf{X}=\mathbf{x}\boxright\neg(\neg\varphi\land\neg\psi)$, which then
gives, by item (v), that
$\neg\big{(}\mathbf{X}=\mathbf{x}\boxright(\neg\varphi\land\neg\psi)\big{)}$.
Next, we derive by applying $\neg\\!\boxright\\!\textsf{E}$ and
$\boxright\\!\\!\wedge\textsf{I}$, together with $\wedge\textsf{E}$ and
$\wedge\textsf{I}$, that

$\neg(\mathbf{X}=\mathbf{x}\boxright\varphi)\wedge\neg(\mathbf{X}=\mathbf{x}\boxright\psi)\vdash(\mathbf{X}=\mathbf{x}\boxright\neg\varphi)\wedge(\mathbf{X}=\mathbf{x}\boxright\neg\psi)\vdash\mathbf{X}=\mathbf{x}\boxright(\neg\varphi\land\neg\psi).$

Then, by applying $\neg\textsf{I}$ and $\neg\textsf{E}$, we derive the
contrapositive of the above, namely

$\neg\big{(}\mathbf{X}=\mathbf{x}\boxright(\neg\varphi\land\neg\psi)\big{)}\vdash\neg\big{(}\neg(\mathbf{X}=\mathbf{x}\boxright\varphi)\wedge\neg(\mathbf{X}=\mathbf{x}\boxright\psi)\big{)}.$

By De Morgan’s laws again, the formula in the conclusion above is equivalent
to
$(\mathbf{X}=\mathbf{x}\boxright\varphi)\vee(\mathbf{X}=\mathbf{x}\boxright\psi)$.
This finishes the proof.

For item (vii), we first derive by $\boxright\\!\textsf{Eff}$ that
$\vdash\mathbf{X}=\mathbf{x}\boxright X=x$, where $X=x$ is an arbitrary
equality from $\mathbf{X}=\mathbf{x}$. By ValDef we also have that
$\vdash\bigvee_{y\in\mathrm{Ran}(Y)}Y=y$. Thus, we conclude by applying
$\boxright\\!\\!\textsf{Rpl}_{C}$ that
$\vdash\mathbf{X}=\mathbf{x}\boxright\bigvee_{y\in\mathrm{Ran}(Y)}Y=y$, which
then implies that
$\vdash\bigvee_{y\in\mathrm{Ran}(Y)}(\mathbf{X}=\mathbf{x}\boxright Y=y)$ by
item (vi). $\square$

######  Theorem 4.14 (Completeness).

For any set $\Delta\cup\\{\alpha\\}$ of $\mathcal{CO}[\sigma]$-formulas, we
have that $\Delta\models^{c/g}\alpha\iff\Delta\vdash\alpha.$

#### 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 $\Delta\models^{c}\alpha$ iff $\Delta\models^{g}\alpha$, given by
Corollary 2.17. $\square$

##  5 Extensions of $\mathcal{CO}$

In this section, we study two extensions of $\mathcal{CO}$, namely
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ and
$\mathcal{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 $\approx$-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.

###  5.1 Expressive power of
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ and
$\mathcal{COD}$

In this subsection, we characterize the expressive power of
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ and
$\mathcal{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 $\mathcal{K}$ be a nonempty class of (generalized) causal teams over some
signature $\sigma$. Then the following are equivalent:

  1. (i)

$\mathcal{K}$ is causally downward closed and closed under equivalence (or in
other words, $\mathcal{K}$ is closed under $\succcurlyeq$).

  2. (ii)

$\mathcal{K}$ is definable by a
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$-formula.

  3. (iii)

$\mathcal{K}$ is definable by a $\mathcal{COD}[\sigma]$-formula.

Notice that any such class $\mathcal{K}$ is finite. By Theorems 2.15 and 3.3,
for every
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$\-
or $\mathcal{COD}[\sigma]$-formula $\varphi$, the set $\mathcal{K}_{\varphi}$
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 $=({\mathbf{X}};{Y})$ are definable in
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
(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 $\Xi^{T}$ that defines the complement of the
set of $\preccurlyeq$-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 $\Xi^{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^{-},\mathcal{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,\mathcal{F}),(s,\mathcal{G})\\}$. If $\mathcal{F}$ and $\mathcal{G}$
are not similar (i.e., $\mathcal{F}\not\sim\mathcal{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 $\mathcal{F}$ and $\mathcal{G}$ are similar (i.e.,
$\mathcal{F}\sim\mathcal{G}$, or $(s,\mathcal{F})\approx(s,\mathcal{G})$), the
two elements $(s,\mathcal{F})$ and $(s,\mathcal{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
$\approx$ between pairs $(s,\mathcal{F})\in T$, denoted as $T/_{\approx}$.

If $T$ is uniform, then clearly $|T/_{\approx}|=|T^{-}|$. In particular, if
$S=(S^{-},\mathcal{F})$ is a causal team, then for the generalized causal team
$S^{g}=\\{(s,\mathcal{F})\mid s\in S^{-}\\}$ it generates, we have that
$|S^{-}|=|S^{g}/_{\approx}|$.

In the next lemma, we introduce a formula $\chi$ that defines the property of
the quotient team $T/_{\approx}$ of having cardinality at most $1$.

######  Lemma 5.2.

Let $T$ be a generalized causal team over some vocabulary $\sigma$.

  1. (i)

If $|T^{-}|=1$, then $T\models\mu\iff$ $T$ is uniform , where

$\mu:=\bigwedge_{V\in\mathrm{Dom}}\bigwedge_{\mathbf{w}\in\mathrm{Ran}(\mathbf{W}_{V})}(\mathbf{W}_{V}=\mathbf{w}\boxright=({V}))~{}\text{
and }~{}\mathbf{W}_{V}=Dom\setminus\\{V\\}.$

  2. (ii)

$T\models\chi\iff|T/_{\approx}|\leq 1$, where

$\chi:=\mu\land\bigwedge_{V\in\mathrm{Dom}}=({V}).$

#### Proof.

(i) Let $T=\\{(s,\mathcal{F}_{1}),\dots,(s,\mathcal{F}_{n})\\}$. If
$\mathcal{F}_{1}\sim\dots\sim\mathcal{F}_{n}$, then
$T\approx\\{(s,\mathcal{F}_{1})\\}$. Clearly,
$\\{(s,\mathcal{F}_{1})\\}\models\mu$, thus we obtain $T\models\mu$ by Theorem
3.3.

For the converse direction, suppose $T$ is not uniform, i.e.,
$\mathcal{F}_{i}\not\sim\mathcal{F}_{j}$ for some $1\leq i<j\leq n$. If
(w.l.o.g.)
$\mathrm{En}(\mathcal{F}_{i})\setminus\mathrm{Cn}(\mathcal{F}_{i})\nsubseteq\mathrm{En}(\mathcal{F}_{j})\setminus\mathrm{Cn}(\mathcal{F}_{j})$,
then there exists $V$ such that
$V\in\mathrm{En}(\mathcal{F}_{i})\setminus\mathrm{Cn}(\mathcal{F}_{i})$ and
$V\notin\mathrm{En}(\mathcal{F}_{j})\setminus\mathrm{Cn}(\mathcal{F}_{j})$.
The former implies that there are
$\mathbf{p},\mathbf{p}^{\prime}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}_{i}})$ such
that
$(\mathcal{F}_{i})_{V}(\mathbf{p})\neq(\mathcal{F}_{i})_{V}(\mathbf{p}^{\prime})$.
Let $\mathbf{w},\mathbf{w}^{\prime}\in\mathrm{Ran}(\mathbf{W}_{V})$ be
extensions of the sequences $\mathbf{p},\mathbf{p}^{\prime}$ respectively.
Clearly, $s^{\mathcal{F}_{i}}_{\mathbf{W}_{V}=\mathbf{w}}\neq
s^{\mathcal{F}_{i}}_{\mathbf{W}_{V}=\mathbf{w}^{\prime}}$. Meanwhile, the
second assumption implies that
$s^{\mathcal{F}_{j}}_{\mathbf{W}_{V}=\mathbf{w}}=s^{\mathcal{F}_{j}}_{\mathbf{W}_{V}=\mathbf{w}^{\prime}}$.
Therefore, either
$s^{\mathcal{F}_{j}}_{\mathbf{W}_{V}=\mathbf{w}}(V)=s^{\mathcal{F}_{j}}_{\mathbf{W}_{V}=\mathbf{w}^{\prime}}(V)\neq
s^{\mathcal{F}_{i}}_{\mathbf{W}_{V}=\mathbf{w}}(V)$ or
$s^{\mathcal{F}_{j}}_{\mathbf{W}_{V}=\mathbf{w}}(V)=s^{\mathcal{F}_{j}}_{\mathbf{W}_{V}=\mathbf{w}^{\prime}}(V)\neq
s^{\mathcal{F}_{i}}_{\mathbf{W}_{V}=\mathbf{w}^{\prime}}(V)$. But then
$T\not\models W_{V}=\mathbf{w}\boxright=({V})$, which implies
$T\not\models\mu$.

In the second case we have that, for some
$V\in\mathrm{En}(\mathcal{F}_{i})\setminus\mathrm{Cn}(\mathcal{F}_{i})=\mathrm{En}(\mathcal{F}_{j})\setminus\mathrm{Cn}(\mathcal{F}_{j})$,
there are $\mathbf{x}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}_{i}}\cap
PA_{V}^{\mathcal{F}_{j}})$,
$\mathbf{y}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}_{i}}\setminus
PA_{V}^{\mathcal{F}_{j}})$ and
$\mathbf{z}\in\mathrm{Ran}(PA_{V}^{\mathcal{F}_{j}}\setminus
PA_{V}^{\mathcal{F}_{i}})$ such that
$(\mathcal{F}_{i})_{V}(\mathbf{xy})\neq(\mathcal{F}_{j})_{V}(\mathbf{xz})$.
Then, for any extension $\mathbf{w}\in\mathrm{Ran}(\mathbf{W}_{V})$ of the
sequence $\mathbf{xyz}$, we have
$s^{\mathcal{F}_{i}}_{\mathbf{W}_{V}=\mathbf{w}}(V)\neq
s^{\mathcal{F}_{j}}_{\mathbf{W}_{V}=\mathbf{w}}(V)$, which again implies
$T\not\models\mu$.

(ii) It is easy to see that $T\models\bigwedge_{V\in\mathrm{Dom}}=({V})$ iff
$|T^{-}|\leq 1$. If $T=\emptyset$, then $\emptyset\models\chi$. If
$T\neq\emptyset$, then by item (i), we have that

$T\models\chi\iff|T^{-}|=1\text{ and $T$ is
uniform}\iff|T/_{\approx}|=|T^{-}|=1.$

$\square$

A causal team $T$ can be identified with a (uniform) generalized causal team
$T^{g}$, and, as pointed out already, $|T^{-}|=|T^{g}/_{\approx}|$. 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 $\mu$ that defines uniformity in item (i) above becomes trivial over
singleton causal teams. Therefore:

######  Corollary 5.3.

For causal teams the formula $\chi$ defined above can be simplified as
follows:

$\displaystyle\chi\equiv^{c}\bigwedge_{V\in\mathrm{Dom}}=({V}).$

#### Proof.

For any causal team $S$, we have that

$\displaystyle S\models^{c}\chi$ $\displaystyle\iff S^{g}\models^{g}\chi$ (by
Lemma 2.16(i)) $\displaystyle\iff|S^{g}/_{\approx}|\leq 1$ (by Lemma 5.2)
$\displaystyle\iff|(S^{g})^{-}|\leq 1\iff|S^{-}|\leq 1\iff
S\models^{c}\bigwedge_{V\in\mathrm{Dom}}=({V}).$

$\square$

We now introduce $\mathcal{COD}[\sigma]$-formulas that characterize the
cardinality of $T/_{\approx}$. For every natural number $k$, define a formula
$\chi_{k}$ as

$\chi_{0}=\bot~{}~{}\text{ and
}~{}~{}\chi_{k}:=\underbrace{\chi\lor\cdots\lor\chi}_{k}\text{ for }k\geq 1$

######  Proposition 5.4.

Let $\sigma$ be a vocabulary and $k$ a natural number.

  1. (i)

For any generalized causal team $T$ over $\sigma$,
$T\models^{g}\chi_{k}\iff|T/_{\approx}|\leq k$.

  2. (ii)

For any causal team $T$ over $\sigma$, $T\models^{c}\chi_{k}\iff|T^{-}|\leq
k$.

#### Proof.

(i) Let $T$ be a generalized causal team. Clearly, $T\models\chi_{0}$ iff
$T=\emptyset$ iff $|T/_{\approx}|=0$. For any $k\geq 1$, $T\models\chi_{k}$
iff there are $T_{1},\dots,T_{k}$ with $T=T_{1}\cup\dots\cup T_{k}$ and each
$T_{i}\models\chi$ (i.e., by Lemma 5.2, $|T_{i}/_{\approx}|\leq 1$), iff there
are pairwise non-$\approx$-equivalent teams $T_{i_{1}},\dots,T_{i_{m}}$ with
$m\leq k$, $T=T_{i_{1}}\cup\dots\cup T_{i_{m}}$ and each
$|T_{i_{j}}/_{\approx}|\leq 1$, iff $|T/_{\approx}|=m\leq k$ for some $m$.

(ii) For any causal team $T$, by item (i) we have that

$\displaystyle T\models^{c}\chi_{k}$ $\displaystyle\iff
T^{g}\models^{g}\chi_{k}$ (by Lemma 2.16(i))
$\displaystyle\iff|T^{-}|=|(T^{g})^{-}|=|T^{g}/_{\approx}|\leq k$ (since
$T^{g}$ is uniform)

$\square$

Now, we are ready to define the crucial formula $\Xi^{T}$ in
$\mathcal{COD}[\sigma]$. Let $T$ be a nonempty generalized causal team with
$|T/_{\approx}|=k+1$. Define

$\Xi^{T}:=\chi_{k}\vee\Theta^{\overline{T^{-}}}\vee\mathop{\bigvee_{s\in
T^{-},\hskip
2.0pt\mathcal{F}\in\mathbb{F}_{\sigma}}}_{\\{(s,\mathcal{F})\\}\not\preccurlyeq
T}(\Theta^{\\{s\\}}\wedge\Phi^{\mathcal{F}}),$

where $\overline{T^{-}}=\mathbb{A}_{\sigma}\setminus T^{-}$. If $T$ is a
causal team, define $\Xi^{T}:=\Xi^{T^{g}}$. We show in the next lemma the
desired characterization property of the formula $\Xi^{T}$. Recall from Lemma
4.6(i) that $T\not\preccurlyeq S$ iff there exists $(t,\mathcal{F})\in T$ such
that $\\{(t,\mathcal{F})\\}\not\preccurlyeq S$.

######  Lemma 5.5.

Let $S,T$ be two (generalized) causal teams over some signature $\sigma$ with
$T\neq\emptyset$. Then, $S\models\Xi^{T}\iff T\not\preccurlyeq S$.

#### Proof.

We first show the generalized causal team case. “$\Longrightarrow$”: Suppose
$S\models\Xi^{T}$. Then there exist $S_{0},S_{1},S_{2}\subseteq S$ such that
$S=S_{0}\cup S_{1}\cup S_{2}$, $S_{0}\models\chi_{k}$,
$S_{1}\models\Theta^{\overline{T^{-}}}$ and

$S_{2}\models\mathop{\bigvee_{s\in T^{-},\hskip
2.0pt\mathcal{F}\in\mathbb{F}_{\sigma}}}_{\\{(s,\mathcal{F})\\}\not\preccurlyeq
T}(\Theta^{\\{s\\}}\wedge\Phi^{\mathcal{F}}).$ (3)

The first clause implies that $|S_{0}/_{\approx}|\leq k$, by Proposition 5.4.
Since $|T/_{\approx}|=k+1$, there must exist a $(t,\mathcal{G})\in T$ such
that $\\{(t,\mathcal{G})\\}\not\preccurlyeq S_{0}$. Moreover, since
$S_{1}\models\Theta^{\overline{T^{-}}}$, we have by Lemma 4.7 that
$S_{1}^{-}\subseteq\overline{T^{-}}$. It then follows that $t\notin
S_{1}^{-}$, giving that $\\{(t,\mathcal{G})\\}\not\preccurlyeq S_{1}$ as well.
Finally, we show that $\\{(t,\mathcal{G})\\}\not\preccurlyeq S_{2}$, which
would then imply $\\{(t,\mathcal{G})\\}\not\preccurlyeq S_{0}\cup S_{1}\cup
S_{2}=S$, thereby $T\not\preccurlyeq S$.

Suppose towards a contradiction that $\\{(t,\mathcal{G})\\}\preccurlyeq
S_{2}$. Then $(t,\mathcal{H})\in S_{2}$ for some $\mathcal{H}\sim\mathcal{G}$.
Now, since (3) holds, we have that
$\\{(t,\mathcal{H})\\}\models\Theta^{\\{s\\}}\wedge\Phi^{\mathcal{F}}$ for
some $s\in T^{-}$ and $\mathcal{F}\in\mathbb{F}_{\sigma}$ with
$\\{(s,\mathcal{F})\\}\not\preccurlyeq T$. This means, by Lemma 4.7 and
Theorem 3.4, that $t=s\in T^{-}$ and
$\mathcal{F}\sim\mathcal{H}\sim\mathcal{G}$. But since $(t,\mathcal{G})\in T$,
we must have that $\\{(s,\mathcal{F})\\}\preccurlyeq T$, which is a
contradiction. Hence, we conclude that $\\{(t,\mathcal{G})\\}\not\preccurlyeq
S_{2}$.

“$\Longleftarrow$”: Suppose $T\not\preccurlyeq S$. Let

$S_{0}=\\{(s,\mathcal{F})\in S\mid\\{(s,\mathcal{F})\\}\preccurlyeq T\\}.$

Then obviously $|S_{0}/_{\approx}|\leq|T/_{\approx}|$. Since
$T\not\preccurlyeq S$, we must have that $T\not\preccurlyeq S_{0}\subseteq S$.
Thus, there exists $(s,\mathcal{G})\in T$ such that
$\\{(s,\mathcal{G})\\}\not\preccurlyeq S_{0}$. But then
$|S_{0}/_{\approx}|<|T/_{\approx}|=k+1$, i.e., $|S_{0}/_{\approx}|\leq k$. By
Proposition 5.4, we conclude that $S_{0}\models\chi_{k}$.

Let

$S_{1}=\\{(s,\mathcal{F})\in S\mid s\notin T^{-}\\}.$

Since $S_{1}^{-}\subseteq\overline{T^{-}}$, by Lemma 4.7 we obtain
$S_{1}\models\Theta^{\overline{T^{-}}}$.

Let $S_{2}=S\setminus(S_{0}\cup S_{1})$. Observe that

$S_{2}=\\{(s,\mathcal{F})\in S\mid s\in T^{-}\text{ and
}\\{(s,\mathcal{F})\\}\not\preccurlyeq T\\}.$

For each $(s,\mathcal{F})\in S_{2}$, we have that
$\\{(s,\mathcal{F})\\}\models\Theta^{\\{s\\}}\wedge\Phi^{\mathcal{F}}$ by
Lemma 4.7 and Theorem 3.4. Thus (using also the empty team property) (3)
holds. Altogether, we conclude that $S\models\varphi$.

Next, observe that the causal team case follows from the generalized causal
team case, since for any causal teams $S,T$, we have that
$\Xi^{T}=\Xi^{T^{g}}$ and

$S\models^{c}\Xi^{T}\iff S^{g}\models^{g}\Xi^{T^{g}}\iff T^{g}\not\preccurlyeq
S^{g}\iff T\not\preccurlyeq S$

by Lemma 2.16(i) and Lemma 4.6(iv). $\square$

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 $\mathcal{K}$ be a nonempty
class of (generalized) causal teams as described in item (i). Since
$\mathcal{K}$ is nonempty and causally downward closed, the empty team belongs
to $\mathcal{K}$. Thus, every (generalized) causal team
$T\in\mathbb{C}_{\sigma}\setminus\mathcal{K}$ is nonempty, where
$\mathbb{C}_{\sigma}$ denotes the (finite) set of all (generalized) causal
teams over $\sigma$. Now, define
$\displaystyle\varphi=\bigwedge_{T\in\mathbb{C}_{\sigma}\setminus\mathcal{K}}\Xi^{T}.$
We show that $\mathcal{K}=\mathcal{K}_{\varphi}$.

For any $S\notin\mathcal{K}$, i.e.,
$S\in\mathbb{C}_{\sigma}\setminus\mathcal{K}$, since $S\preccurlyeq S$ and
$S^{-}\neq\emptyset$, by Lemma 5.5 we have that $S\not\models\Xi^{S}$. Thus
$S\not\models\varphi$, i.e., $S\notin\mathcal{K}_{\varphi}$. Conversely,
suppose $S\in\mathcal{K}$. Take any
$T\in\mathbb{C}_{\sigma}\setminus\mathcal{K}$. If $T\preccurlyeq S$, then
since $\mathcal{K}$ is closed under $\succcurlyeq$ we must conclude that
$T\in\mathcal{K}$; a contradiction. Thus, by Lemma 5.5, $S\models\Xi^{T}$.
Hence $S\models\varphi$, i.e., $S\in\mathcal{K}_{\varphi}$. $\square$

###  5.2 Axiomatizing
$\mathcal{CO}_{\footnotesize{\setminus}\mspace{-5.0mu}{\setminus}/}$ over
generalized causal teams

In this section, we introduce a sound and complete system of natural deduction
for
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$,
which extends the system for $\mathcal{CO}[\sigma]$, and can also be seen as a
variant of the systems for propositional dependence logics introduced in [30].

######  Definition 5.6.

The system of natural deduction for
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
over generalized causal teams consists of all rules of the system for
$\mathcal{CO}[\sigma]$ (see Definition 4.12) together with the following
rules, where note that in the rules $\vee\textsf{E}$, $\neg\textsf{I}$,
$\neg\textsf{E}$, RAA and $\neg\\!\ \\!\\!\boxright\\!\\!\textsf{E}$ from
Definition 4.12 the formula $\alpha$ ranges over
$\mathcal{CO}[\sigma]$-formulas only:

  * -

Additional rules for $\vee$:
$\varphi\vee\psi$ $\vee\textsf{Com}$ $\psi\vee\varphi$
$(\varphi\vee\psi)\vee\chi$ $\vee\textsf{Ass}$ $\varphi\vee(\psi\vee\chi)$
$\varphi\vee\psi$ [$\varphi$] $\vdots$ $\chi$ $\vee\textsf{Rpl}$
$\chi\vee\psi$ $\mathbf{X}=\mathbf{x}\boxright\varphi\vee\psi$
$\boxright\\!\\!\vee\textsf{Dst}$
$(\mathbf{X}=\mathbf{x}\boxright\varphi)\vee(\mathbf{X}=\mathbf{x}\boxright\psi)$

  * -

Rules for $\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$:
$\varphi$ $\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$I
$\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$
$\varphi$ $\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$I
$\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\varphi$
$\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi$
[$\varphi$] $\vdots$ $\chi$ [$\psi$] $\vdots$ $\chi$
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$E $\chi$
$\varphi\vee(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)$
$\vee\\!\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\\!\textsf{Dst}$
$(\varphi\vee\psi)\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}(\varphi\vee\chi)$
$\mathbf{X}=\mathbf{x}\boxright\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi$
$\boxright\\!\\!\\!\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}$Dst
$(\mathbf{X}=\mathbf{x}\boxright\psi)\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}(\mathbf{X}=\mathbf{x}\boxright\chi)$

The double line in rule $\boxright\\!\\!\vee\textsf{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
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$
is an extension of that for $\mathcal{CO}[\sigma]$, the clauses in Proposition
4.13 are still derivable (assuming that the formula $\alpha$ that appears in
some of the clauses ranges over $\mathcal{CO}[\sigma]$-formulas only) by the
same derivations, except for item (vi) whose proof uses the rule
$\vee\mathsf{E}$ and the rules for negation which are not sound for arbitrary
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$-formulas.
This item is thus now directly included in the system for
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$as
rule $\boxright\\!\\!\vee\textsf{Dst}$. We now derive some additional useful
clauses.

######  Proposition 5.7.

The following are derivable in the system of
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$:

  1. (i)

$\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi\vdash\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\varphi$
and
$(\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\psi)\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi\vdash\varphi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)$

  2. (ii)

$\varphi\wedge(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)\dashv\vdash(\varphi\wedge\psi)\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}(\varphi\wedge\chi)$

  3. (iii)

$\varphi\wedge(\psi\vee\chi)\vdash(\varphi\wedge\psi)\vee(\varphi\wedge\chi)$

  4. (iv)

$\varphi\vee(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)\dashv\vdash(\varphi\vee\psi)\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}(\varphi\vee\chi)$

  5. (v)

$\mathbf{X}=\mathbf{x}\boxright\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi\dashv\vdash(\mathbf{X}=\mathbf{x}\boxright\psi)\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}(\mathbf{X}=\mathbf{x}\boxright\chi)$

#### Proof.

Items (i),(ii) follow from the standard argument using
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$I and
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$E. Item (iii)
is proved easily by applying $\vee\textsf{Rpl}$ and $\lor$Com; we remark that
it cannot be proved by the usual natural deduction arguments, as rule
$\lor\textsf{E}$ is available only for $\mathcal{CO}[\sigma]$ formulas. For
item (iv), the left to right direction follows from
$\vee\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\textsf{Dst}$.
For the right to left direction, we first derive
$\varphi\vee\psi\vdash\varphi\vee(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)$
and
$\varphi\vee\chi\vdash\varphi\vee(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)$
by applying $\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$I
and $\vee\textsf{Rpl}$. Then
$(\varphi\vee\psi)\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}(\varphi\vee\chi)\vdash\varphi\vee(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)$
follows from
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$E. For item
(v), the left to right direction follows from
$\boxright\\!\\!\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}$Dst,
and the other direction is proved by using
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$I,
$\boxright\\!\textsf{Rpl}_{C}$ and
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$E. $\square$

An important lemma towards the completeness theorem states that every
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$-formula
$\varphi$ is provably equivalent to the
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$-disjunction
of a (finite) set of $\mathcal{CO}[\sigma]$-formulas. Formulas of this type
are called _resolutions_ of $\varphi$ in [9].

######  Definition 5.8.

Let $\varphi$ be a
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$-formula.
Define the set $\mathcal{R}(\varphi)$ of its resolutions inductively as
follows:

  * -

$\mathcal{R}(X=x)=\\{X=x\\}$,

  * -

$\mathcal{R}(\neg\alpha)=\\{\neg\alpha\\}$,

  * -

$\mathcal{R}(\psi\land\chi)=\\{\alpha\land\beta\ |\
\alpha\in\mathcal{R}(\psi),\beta\in\mathcal{R}(\chi)\\}$,

  * -

$\mathcal{R}(\psi\lor\chi)=\\{\alpha\lor\beta\ |\
\alpha\in\mathcal{R}(\psi),\beta\in\mathcal{R}(\chi)\\}$,

  * -

$\mathcal{R}(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi)=\mathcal{R}(\psi)\cup\mathcal{R}(\chi)$,

  * -

$\mathcal{R}(\mathbf{X}=\mathbf{x}\boxright\varphi)=\\{\mathbf{X}=\mathbf{x}\boxright\alpha\
|\ \alpha\in\mathcal{R}(\varphi)\\}$.

The set $\mathcal{R}(\varphi)$ is clearly a finite set of
$\mathcal{CO}[\sigma]$-formulas.

######  Lemma 5.9.

For any formula
$\varphi\in\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$,
we have that
$\varphi\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\varphi).$

#### Proof.

We prove the lemma by induction on $\varphi$. If $\varphi$ is $X=x$ or
$\neg\alpha$ for some $\mathcal{CO}[\sigma]$-formula $\alpha$, then
$\mathcal{R}(\varphi)=\\{\varphi\\}$, and
$\varphi\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\varphi)$
holds trivially.

Now, suppose
$\psi\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\psi)$
and
$\chi\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\chi)$.
If $\varphi=\psi\wedge\chi$, we derive by applying Proposition 5.7((ii)),
$\land\textsf{I}$ and $\land\textsf{E}$ that

$\psi\wedge\chi\dashv\vdash\big{(}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\psi)\big{)}\wedge\big{(}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\chi)\big{)}\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\\{\alpha\wedge\beta\mid\alpha\in\mathcal{R}(\psi),\beta\in\mathcal{R}(\chi)\\}\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\psi\wedge\chi).$

If $\varphi=\psi\vee\chi$, we have analogous derivations using Proposition
5.7(iv), $\lor\textsf{I}$ and $\lor\textsf{Rpl}$.

If
$\varphi=\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi$,
then by the rules
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$I and
$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$E together
with Proposition 5.7(i) we have that

$\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi\dashv\vdash\big{(}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\psi)\big{)}\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\big{(}\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\chi)\big{)}\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\big{(}\mathcal{R}(\psi)\cup\mathcal{R}(\chi)\big{)}\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\psi\raisebox{1.0pt}{$\mathop{\,{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}\,}$}\chi).$

If $\varphi=\mathbf{X}=\mathbf{x}\boxright\psi$, then

$\displaystyle\mathbf{X}=\mathbf{x}\boxright\psi$
$\displaystyle\dashv\vdash\mathbf{X}=\mathbf{x}\boxright\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\psi)$
($\boxright\\!\\!\textsf{Rpl}_{C}$)
$\displaystyle\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\\{\mathbf{X}=\mathbf{x}\boxright\alpha\mid\alpha\in\mathcal{R}(\psi)\\}$
(Proposition 5.7(v))
$\displaystyle\dashv\vdash\mathop{{{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}}\mathcal{R}(\mathbf{X}=\mathbf{x}\boxright\psi).$

$\square$

######  Theorem 5.10 (Completeness).

For any set $\Gamma\cup\\{\psi\\}$ of
$\mathcal{CO}_{\footnotesize{\mathbin{{\setminus}\mspace{-5.0mu}{\setminus}}/}}[\sigma]$-formulas,
we have that $\Gamma\models^{g}\psi\iff\Gamma\vdash\psi.$

#### Proof.

We prove the “$\Longrightarrow$” direction. Observe that there are only