Expressivity and Complexity of Dependence Logic

Abstract

In this article we review recent results on expressivity and complexity of first-order, modal, and propositional dependence logic and some of its variants such as independence and inclusion logic. Dependence logic was introduced by Jouko Väänänen in [56]. On the syntactic side, it extends usual first-order logic by the so-called dependence atoms the meaning of which is that the value of x _n is functionally determined by the values of x ₁, …, x _n−1. The semantics of dependence logic is defined using sets of assignments, teams, rather than single assignments as in first-order logic. Since the introduction of dependence logic in 2007, the area of team semantics has evolved into a general framework for logics in which various notions of dependence and independence can be formalized and studied. In this paper we mainly consider variants of dependence logic arising by replacing/supplementing dependence atoms with further dependency notions, and we also study propositional and modal variants.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In this article we review recent results on expressivity and complexity of first-order, modal, and propositional dependence logic and some of its variants such as independence and inclusion logic. Dependence logic was introduced by Jouko Väänänen in [56]. On the syntactic side, it extends usual first-order logic by the so-called dependence atoms

$$\displaystyle{=\left (x_{1},\ldots,x_{n}\right ),}$$

the meaning of which is that the value of x _n is functionally determined by the values of x ₁, …, x _n−1. The semantics of dependence logic is defined using sets of assignments, teams, rather than single assignments as in first-order logic. Since the introduction of dependence logic in 2007, the area of team semantics has evolved into a general framework for logics in which various notions of dependence and independence can be formalized and studied. In this paper we mainly consider variants of dependence logic arising by replacing/supplementing dependence atoms with further dependency notions, and we also study propositional and modal variants.

In Section 2 we review the basic definitions and results on first-order dependence logic and its variants (extensions and fragments). It is divided into three subsections of which the two first ones deal with results related to expressive power and definability. In particular, results charting the expressive power of certain natural syntactic fragments of dependence logic and its variants will be discussed in Section 2.4. Section 2.5 reviews results on the complexity of satisfiability and model checking in the (first-order) dependence logic context. In Section 3 we turn to modal and propositional versions of dependence logic. After introducing the basic notions and logics, we will again first touch expressivity questions and then turn to the complexity of algorithmic problems arising in this context, mostly the complexity of satisfiability and model checking. The paper concludes in Section 4 with a list of open questions.

2 First-order Dependence Logic

2.1 Team semantics

In this section we define the basics of the team semantics as presented in the monograph [56] by Väänänen. The origins of this definition go back to a paper by Wilfrid Hodges [35], in which he gave a Tarski-style semantics for Hintikka and Sandu’s independence-friendly logic $\mathcal{I}\mathcal{F}$ [34]. Hodges originally used the term “trump semantics”, somewhat reflecting the game-theoretic nature of the previously only known non-compositional semantics for $\mathcal{I}\mathcal{F}$.

Definition 1.

Let $\mathcal{M}$ be a structure with domain M, and V a finite set of variables. Then

• A team X over $\mathcal{M}$ with domain Dom(X) = V is a finite set of assignments $s: V \rightarrow M$.

• For a tuple $\mathbf{v} = (v_{1},\ldots,v_{n})$, where v _i  ∈ V, $X(\mathbf{v}):=\{ s(\mathbf{v}): s \in X\}$ is an n-ary relation of M, where $s(\mathbf{v}):= (s(v_{1}),\ldots,s(v_{n}))$.

• For $W \subseteq V$, $X \upharpoonright W$ denotes the team obtained by restricting all assignments of X to W.

• The set of free variables of a formula ϕ is defined analogously as in first-order logic, and is denoted by Fr(ϕ). In particular, all non-first-order atoms considered in this article (see Definition 3) are treated as atomic formulas, and hence all variable occurrences in them are considered to be free.

With the above notions defined, we are now ready to present the semantics of dependence logic. In this article we consider two variants of the semantics called the strict and the lax semantics introduced in [16]. The original semantics given in [56] is a combination of these variants (with the lax disjunction and the strict existential quantifier). For any logic, e.g., dependence logic, whose formulas have the downwards closure property of Proposition 4, the two variants of the semantics are easily seen to be equivalent. On the other hand, for inclusion and independence logic the semantics are not equivalent [16]. A serious disadvantage of the strict semantics is the failure of the locality property in the case of inclusion and independence logic (see Proposition 1).

We will first define the lax version of the team semantics for first-order formulas in negation normal form. For an assignment s, $\mathcal{M}\models _{s}\alpha$ below refers to satisfaction in first-order logic. We denote by s[m∕v] the assignment such that $s[m/v](x) = m$ if x = v, and $s[m/v](x) = s(x)$ otherwise.

Definition 2 (Lax Semantics).

Let $\mathcal{M}$ be a structure, X a team over $\mathcal{M}$, and ϕ a formula such that $\text{Fr}(\phi ) \subseteq \text{Dom}(X)$. Then X satisfies ϕ in $\mathcal{M}$, $\mathcal{M}\models _{X}\phi$, if

lit::

For a first-order literal α, $\mathcal{M}\models _{X}\alpha$ if and only if for all s ∈ X, $\mathcal{M}\models _{s}\alpha$.

∨::

$\mathcal{M}\models _{X}\psi \vee \theta$ if and only if there are Y and Z such that $Y \cup Z = X$, $\mathcal{M}\models _{Y }\psi$ and $\mathcal{M}\models _{Z}\theta$.

∧::

$\mathcal{M}\models _{X}\psi \wedge \theta$ if and only if $\mathcal{M}\models _{X}\psi$ and $\mathcal{M}\models _{X}\theta$.

$\exists$::

$\mathcal{M}\models _{X}\exists v\psi$ if and only if there exists a function $F: X \rightarrow \mathcal{P}(M)\setminus \{\emptyset \}$ such that $\mathcal{M}\models _{X[F/v]}\psi$, where $X[F/v] =\{ s[m/v]: s \in X,m \in F(s)\}$.

$\forall$::

$\mathcal{M}\models _{X}\forall v\psi$ if and only if $\mathcal{M}\models _{X[M/v]}\psi$, where $X[M/v] =\{ s[m/v]:$ s ∈ X, m ∈ M}.

A sentence is a formula without free variables. A sentence ϕ is true in $\mathcal{M}$ (abbreviated $\mathcal{M}\models \phi$) if $\mathcal{M}\models _{\{\emptyset \}}\phi$. Sentences ϕ and ϕ′ are equivalent, ϕ ≡ ϕ′, if for all models $\mathcal{M}$, $\mathcal{M}\models \phi \Leftrightarrow \mathcal{M}\models \phi '$.

In the strict semantics, the semantic rule for disjunction is replaced by

• $\mathcal{M}\models _{X}\psi \vee \theta$ if and only if, there are Y and Z such that $Y \cap Z =\emptyset$, $Y \cup Z = X$, $\mathcal{M}\models _{Y }\psi$ and $\mathcal{M}\models _{Z}\theta$,

and the semantic rule for existential quantifier by

• $\mathcal{M}\models _{X}\exists v\psi$ if and only if, there exists a function $F: X \rightarrow \mathcal{P}(M)\setminus \{\emptyset \}$ such that | F(s) | = 1 for all s ∈ X, and $\mathcal{M}\models _{X[F/v]}\psi$.

It is worth noting that functions quantified in the strict semantics version of the existential quantifier correspond exactly to functions $F: X \rightarrow M$. Hence the notation X[F∕v] can be naturally extended to cover also functions $F: X \rightarrow M$.

The meaning of first-order formulas is invariant under the choice between the strict and the lax semantics. Furthermore, first-order formulas have the following flatness property:

Theorem 1 (Flatness).

Let $\mathcal{M}$ be a structure and X a team of $\mathcal{M}$ . Then for a first-order formula ϕ the following are equivalent:

• 1. $\mathcal{M}\models _{X}\phi$ ,

• 2. For all s ∈ X, $\mathcal{M}\models _{s}\phi$ .

It is worth noting that in [56] also a general notion of flatness of a formula is defined by replacing the second item above by “For all s ∈ X, $\mathcal{M}\models _{\{s\}}\phi$”.

Next we will give the semantic clauses for the non-first-order atoms and connectives considered in this paper. We begin with the new atomic formulas:

Definition 3.

• Let $\mathbf{x}$ be a tuple of variables and let y be another variable. Then $=\left (\mathbf{x},y\right )$ is a dependence atom, with the following semantic rule:

  • $\mathcal{M}\models _{X}=\left (\mathbf{x},y\right )$ if and only if for all s, s′ ∈ X, if $s(\mathbf{x}) = s'(\mathbf{x})$, then s(y) = s′(y).

• Let $\mathbf{x}$, $\mathbf{y}$, and $\mathbf{z}$ be tuples of variables (not necessarily of the same length). Then $\mathbf{y}\ \perp _{\mathbf{x}}\ \mathbf{z}$ is a conditional independence atom, with the semantic rule

  • $\mathcal{M}\models _{X}\mathbf{y}\ \perp _{\mathbf{x}}\ \mathbf{z}$ if and only if for all s, s′ ∈ X such that $s(\mathbf{x}) = s'(\mathbf{x})$, there exists a s″ ∈ X such that $s''(\mathbf{x}\mathbf{y}\mathbf{z}) = s(\mathbf{x}\mathbf{y})s'(\mathbf{z})$.

  Furthermore, we will write $\mathbf{x}\ \perp \ \mathbf{y}$ as a shorthand for $\mathbf{x}\ \perp _{\emptyset }\ \mathbf{y}$, and call it a pure independence atom.

• Let $\mathbf{x}$ and $\mathbf{y}$ be two tuples of variables of the same length. Then $\mathbf{x} \subseteq \mathbf{ y}$ is an inclusion atom, with the semantic rule

  • $\mathcal{M}\models _{X}\mathbf{x} \subseteq \mathbf{ y}$ if and only if $X(\mathbf{x}) \subseteq X(\mathbf{y})$.

• Let $\mathbf{x}$ and $\mathbf{y}$ be two tuples of variables of the same length. Then $\mathbf{x}\mid \mathbf{y}$ is an exclusion atom, with the semantic rule

  • $\mathcal{M}\models _{X}\mathbf{x}\mid \mathbf{y}$ if and only if $X(\mathbf{x}) \cap X(\mathbf{y}) =\emptyset$.

We denote the set of all dependence atoms by = ​​ (…). Analogously, all independence, inclusion and exclusion atoms are denoted by ⊥ _c, $\subseteq$, and ∣, respectively. For a collection $\mathcal{C}\subseteq \{=\!\! (\ldots ),\perp _{\mathrm{c}},\subseteq,\mid \}$, we write $\mathcal{F}\mathcal{O}(\mathcal{C})$ (omitting the set parenthesis of $\mathcal{C}$) for the logic obtained by adding all atoms listed in $\mathcal{C}$ to the syntax of first-order logic. Independence atoms (or independence logic) were first considered in [21], and inclusion atoms go back to [16]. In our notation, dependence logic, independence logic, and inclusion logic are denoted by $\mathcal{F}\mathcal{O}(=\!\left (\ldots \right ))$, $\mathcal{F}\mathcal{O}(\perp _{\mathrm{c}})$, and $\mathcal{F}\mathcal{O}(\subseteq )$, respectively. We also use the notation $\mathcal{D}$ as a shortcut for $\mathcal{F}\mathcal{O}(=\!\left (\ldots \right ))$. The fragment of independence logic containing only pure independence atoms in denoted $\mathcal{F}\mathcal{O}(\perp )$.

Under the lax semantics, all of the above logics satisfy the following locality property [16]:

Proposition 1.

Let $\phi \in \mathcal{F}\mathcal{O}(=\!\! (\ldots ),\perp _{\mathrm{c}},\subseteq,\mid )$ . Then for all models $\mathcal{M}$ and teams X,

$$\displaystyle{\mathcal{M}\models _{X}\phi \Leftrightarrow \mathcal{M}\models _{X\upharpoonright \text{Fr}(\phi )}\phi.}$$

On the other hand, under the strict semantics Proposition 1 fails for inclusion and independence logic [16].

The aforementioned atoms are particular instances of a general notion of generalized dependence atom [44]. The semantics of a generalized dependence atom A _Q is determined (essentially) by a class Q of structures and teams over which the atomic formula $A_{Q}(\mathbf{x}_{1},\ldots,\mathbf{x}_{n})$ is satisfied (see [44] for details; we will consider $\mathcal{F}\mathcal{O}$-definable generalized dependence atoms as depicted in Table 1

Table 1 Definitions of some generalized dependence atoms

).

Next we will define connectives and quantifiers that will also be discussed in the next section. One of the most natural extensions of dependence logic is obtained by the classical negation ($\sim$) with the usual interpretation:

$$\displaystyle{\mathcal{M}\models _{X} \sim \phi \text{ iff }\mathcal{M}\nvDash _{X}\phi.}$$

This extension was introduced in [57], and the logic obtained was called Team Logic ($\mathcal{T}\mathcal{L}$). The classical disjunction (also sometimes referred to as intuitionistic disjunction) has also been considered especially in the modal team semantics context, see Section 3. The connective has the expected interpretation

In [1] two new connectives called the intuitionistic ($\rightarrow$) and the linear implication ($\multimap$) were introduced giving rise to an extension of dependence logic called BID:

$$\displaystyle\begin{array}{rcl} \mathcal{M}\models _{X}\phi \rightarrow \psi & \text{ iff }& \text{ for all }Y \subseteq X,\text{ if }\mathcal{M}\models _{Y }\phi \text{ then }\mathcal{M}\models _{Y }\psi. {}\\ \mathcal{M}\models _{X}\phi \multimap \psi & \text{ iff }& \text{ for all }Y,\text{ if }\mathcal{M}\models _{Y }\phi \text{ then }\mathcal{M}\models _{X\cup Y }\psi. {}\\ \end{array}$$

Quantifiers, other than the familiar $\exists$ and $\forall$, have also been studied in the team semantics setting [12, 13]. From the complexity theoretic point of view, the following majority quantifier introduced in [7] is interesting:

$$\displaystyle\begin{array}{rcl} & \mbox{ $\mathcal{M}\models _{X}\mathsf{M}x\phi (x)$ iff for at least $\vert M\vert ^{\vert X\vert }/2$ many functions $F: X \rightarrow M$, we have}& {}\\ & \mathcal{M}\models _{X[F/x]}\phi (x). & {}\\ \end{array}$$

2.2 Normal forms

In order to analyse the expressive power of dependence logic and to compare it with other formalisms, it is useful to obtain normal forms such as this one proved in [56].

Theorem 2.

Every dependence logic sentence is equivalent to some sentence of the form:

$$\displaystyle{\phi:= \forall \mathbf{x}\exists \mathbf{y}\ (\bigwedge _{i\in I}=\!\left ({\boldsymbol x_{i}},y_{i}\right )\wedge \theta )}$$

where $I \subseteq \mathbb{N}$ , ${\boldsymbol x_{i}}$ is a subsequence of $\mathbf{x}$ , and y _i is a member of $\mathbf{y}$ .

Such a result is an analogue of Skolem normal form for first-order logic. It separates clearly the functional dependencies introduced between subsets of variables from the regular part of the formula. It also makes intuitively clear that to be translated into an extension of first-order logic one would need second-order quantification to express these dependencies between variables. Refinements of such a normalization result are at the heart of various characterizations of dependence-like logics and their fragments. For example, the analogue of Theorem 2 for independence logic (with dependence atoms replaced by independence atoms) was shown in [23]. Furthermore, a prenex normal form theorem for formulas of $\mathcal{F}\mathcal{O}(=\!\! (\ldots ),\perp _{\mathrm{c}},\subseteq )$ was shown for the strict and the lax semantics in [18] and [26], respectively.

2.3 Expressive Power

In this section we review results on the expressive power of the variants of dependence logic of the previous subsections.

As it turns out, the expressive power of sentences of dependence logic corresponds to that of existential second-order logic [56], and hence to the complexity class non-deterministic polynomial time (NP) via the well-known theorem of Fagin [14]. In the following, we will not distinguish in notation between a logic and the classes of models defined by its sentences, and we will use the equality symbol to denote that logics are equivalent for sentences, and we will use equality for logics and complexity classes in the same vein.

Theorem 3.

$\mathcal{D} = \mathsf{NP} = \mathcal{E}\mathcal{S}\mathcal{O}$

The direction $\mathcal{E}\mathcal{S}\mathcal{O}\leq \mathcal{D}$ is proved by utilizing the fact that every $\mathcal{E}\mathcal{S}\mathcal{O}$-sentence can be transformed to the so-called Skolem normal form. On the other hand, the direction $\mathcal{D}\leq \mathcal{E}\mathcal{S}\mathcal{O}$ is proved by essentially simulating the team semantics of dependence logic in $\mathcal{E}\mathcal{S}\mathcal{O}$ with an extra relation symbol interpreting the team.

An interesting consequence of the team semantics of dependence logic is that Theorem 3 does not immediately settle the question also for open formulas. In fact, all $\mathcal{D}$-formulas have the following Downwards Closure property:

Theorem 4 (Downwards Closure).

Let ϕ be a $\mathcal{D}$ -formula. Then for all structures $\mathcal{M}$ and teams X, if $\mathcal{M}\models _{X}\phi$ and $Y \subseteq X$ , then $\mathcal{M}\models _{Y }\phi$ .

It was shown in [39] that the open formulas of dependence logic can define exactly the downward closed properties of teams expressible in $\mathcal{E}\mathcal{S}\mathcal{O}$ (again with an extra relation symbol for the team). Furthermore, already dependence atoms combined with disjunction give rise to NP-complete decision problems [37]. Define the formulas ϕ ₁ and ϕ ₂ as follows:

• $\phi _{1}:=\ =\!\left (x,y\right ) \vee =\!\left (u,v\right )$,

• $\phi _{2}:=\ =\!\left (x,y\right ) \vee =\!\left (u,v\right ) \vee =\!\left (u,v\right )$.

Then the question of deciding whether a finite team X satisfies ϕ ₁ is NL-complete, and for ϕ ₂, already NP-complete.

As one might expect, the expressive power of dependence logic with the classical negation ($\mathcal{T}\mathcal{L}$) increases to full second-order logic, and hence to the complexity class Polynomial Hierarchy (PH).

Theorem 5.

$\mathcal{T}\mathcal{L} = \mathcal{S}\mathcal{O} = \mathsf{PH}$

This result is already shown in [56], but a direct translation of $\mathcal{S}\mathcal{O}$ sentences into $\mathcal{T}\mathcal{L}$-sentences was later given in [48]. Furthermore, in [38] it was shown that any property of teams definable in second-order logic can be expressed in team logic. It is worth noting that, for example, in general $\mathcal{T}\mathcal{L}$-formulas are not closed downwards, e.g., the formula

$$\displaystyle{ \sim =\!\left (x\right ) }$$

(1)

expresses that x has at least two distinct values.

Interestingly, the two new connectives (implications) introduced in [1] preserve downwards closure when added to dependence logic. It was observed in [1] that any sentence of BID-logic can be translated into second-order logic. In fact, by the result of [62], already the intuitionistic implication alone increases the expressive power of dependence logic to full second-order logic.

Theorem 6.

$\mathcal{D}(\rightarrow ) = \mathcal{S}\mathcal{O} = \mathsf{PH}$

This result utilizes the universal quantification implicit in the semantic rule of the intuitionistic implication. On the other hand, in [7, 8] the extension $\mathcal{D}(\mathsf{M})$ of dependence logic by the majority quantifier M was defined and studied. The main result of that paper is stated as follows:

Theorem 7.

$\mathcal{D}(\mathsf{M}) = \mathsf{CH}$ .

Above CH refers to the complexity class the counting hierarchy $\mathsf{CH} \supseteq \mathsf{PH}$. Theorems 7 and 5 imply that, for sentences, $\mathcal{D}(\mathsf{M})$ is at least as expressive as $\mathcal{T}\mathcal{L}$ over finite structures. On the other hand, this result does not extend to open formulas since $\mathcal{D}(\mathsf{M})$-formulas have the downward closure property unlike $\mathcal{T}\mathcal{L}$-formulas (see, e.g., formula (1)).

The aforementioned results show that dependence logic and its extensions allow us to logically characterize NP and some of its super classes. In [11] the question whether PTIME corresponds to a natural fragment of dependence logic was considered. For $\mathcal{E}\mathcal{S}\mathcal{O}$ (also $\mathcal{S}\mathcal{O}$) it is known that the so-called Horn fragment $\mathcal{S}\mathcal{O}\exists \text{-Horn}$ of $\mathcal{E}\mathcal{S}\mathcal{O}$ captures PTIME over successor structures [19]. In [11] a fragment $\mathcal{D}^{{\ast}}\text{-Horn}$ equivalent to $\mathcal{S}\mathcal{O}\exists \text{-Horn}$ was identified. The formulas of $\mathcal{D}^{{\ast}}\text{-Horn}$ have the form

$$\displaystyle{\forall \mathbf{x}\exists \mathbf{y}(\bigwedge _{i}=\!\left (\mathbf{z}_{i},y_{i}\right ) \wedge \bigwedge _{j}C_{j}),}$$

where $\mathbf{z}_{i}$ is subsequence of $\mathbf{x}$, the clauses C _j (i.e. disjunctions of $\mathcal{F}\mathcal{O}$-literals) are assumed to satisfy a certain Horn condition, and the existentially quantified variables y _i are only allowed to appear in certain identity atoms of C _j (see [11] for the exact definition). The main result of [11] shows that

Theorem 8.

Over finite successor structures, $\mathcal{D}^{{\ast}}\text{-Horn} = \mathcal{S}\mathcal{O}\exists \text{-Horn}$ .

Theorem 8 implies that

$$\displaystyle{\mathcal{D}^{{\ast}}\text{-Horn} = \mathsf{PTIME}}$$

over finite successor structures. In the article [11] the expressive power of open formulas of $\mathcal{D}^{{\ast}}\text{-Horn}$ is also characterized.

All of the results discussed in this section use the original semantics of dependence logic. It is easy to check that the results hold also for both variants of the semantics. Next we will consider the expressive power of inclusion logic. It turns out that the expressive power of inclusion logic is not invariant under the choice between the strict and the lax semantics.

The expressive power of inclusion logic under the lax semantics was studied in [17]. The main result of that paper shows that

Theorem 9.

Over the lax semantics,

$$\displaystyle{\mathcal{F}\mathcal{O}(\subseteq ) = \mathrm{GFP}^{+},}$$

where GFP⁺ is the so-called Positive Greatest Fixed Point Logic. It is known that over finite structures GFP⁺ is equi-expressive with Least Fixed Point Logic (LFP), and furthermore for ordered finite structures LFP = PTIME by the famous result of Immerman [36] and Vardi [60]. Therefore, it follows that

$$\displaystyle{\mathcal{F}\mathcal{O}(\subseteq ) = \mathsf{PTIME}}$$

over ordered finite structures. In drastic contract with Theorem 9, it was observed in [18] that, over the strict semantics, inclusion logic is equivalent to $\mathcal{E}\mathcal{S}\mathcal{O}$ and hence captures NP.

Theorem 10.

Over the strict semantics,

$$\displaystyle{\mathcal{F}\mathcal{O}(\subseteq ) = \mathcal{E}\mathcal{S}\mathcal{O}.}$$

This result is based on a simulation of dependence atoms in a dependence logic sentence (in the $\forall ^{{\ast}}\exists ^{{\ast}}$-normal form) by certain inclusion logic formulas. This simulation is not possible in general but only over teams that are generated by evaluating a $\forall ^{{\ast}}\exists ^{{\ast}}$-block of quantifiers with the strict semantics.

2.4 Refining the correspondence with $\mathcal{E}\mathcal{S}\mathcal{O}$

In this part we investigate how the correspondence between existential second-order logic and $\mathcal{F}\mathcal{O}(\mathcal{C})$ for subsets $\mathcal{C}$ of dependence-like atoms can be refined. In particular we examine what is the effect of bounding the number of variables and the so-called arity of atoms which roughly concerns the number of distinct variables involved in them.

By relating fragments of $\mathcal{F}\mathcal{O}(\mathcal{C})$ to fragments of existential second-order logic, one may hope to obtain separation results in dependence logics through hierarchy theorems in complexity or to give evidence that such results would have non-trivial consequences in complexity theory. In either way, this provides interesting insight on the expressive power of these logics.

Let us first define the notion of arity of an atom.

Definition 1.

Let $k \in \mathbb{N}$.

• A dependence atom $=\left (\mathbf{x},y\right )$ is of arity k if the length of $\mathbf{x}$ is k.

• An independence atom $\mathbf{y}\ \perp _{\mathbf{x}}\ \mathbf{z}$ is of arity k if $\mathbf{x}\mathbf{y}\mathbf{z}$ contains k + 1 distinct variables.

• An inclusion atom $\mathbf{x} \subseteq \mathbf{ y}$ is of arity k if the length of $\mathbf{x}$ and $\mathbf{y}$ is k.

We now define the corresponding fragments of $\mathcal{F}\mathcal{O}(\mathcal{C})$ and existential second-order logic.

Definition 2.

Let $\mathcal{C}$ be a subset of $\{= (\ldots ),\perp _{\mathrm{c}},\subseteq,\mid \}$. Let $k \in \mathbb{N}$. Then:

• $\mathcal{F}\mathcal{O}(\mathcal{C})(k\mathrm{-ary})$ is the class of sentences of $\mathcal{F}\mathcal{O}(\mathcal{C})$ in which all atoms of $\mathcal{C}$ are of arity bounded by k.

• $\mathcal{F}\mathcal{O}(\mathcal{C})(k\forall )$ is the class of sentences of $\mathcal{F}\mathcal{O}(\mathcal{C})$ in which every variable is quantified exactly once and at most k universal quantifiers occur.

• For convenience, we set by $\mathcal{D}(k\mathrm{-ary})$ the class $\mathcal{F}\mathcal{O}(=\!\! (\ldots ))(k\mathrm{-ary})$ and by $\mathcal{D}(k\mathrm{-ary})$ the class $\mathcal{F}\mathcal{O}(=\!\! (\ldots ))(k\forall )$.

Definition 3.

Let $k \in \mathbb{N}$.

• $\mathcal{E}\mathcal{S}\mathcal{O}(k\mathrm{-ary})$ is the class of $\mathcal{E}\mathcal{S}\mathcal{O}$-sentences

  $$\displaystyle{ \exists X_{1}\ldots \exists X_{n}\psi, }$$

  in which the relation symbols X _i are at most k-ary and ψ is a first-order formula.

• $\mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\mathrm{-ary})$ is the class of $\mathcal{E}\mathcal{S}\mathcal{O}$-sentences

  $$\displaystyle{ \exists f_{1}\ldots \exists f_{n}\psi, }$$

  in which the function symbols f _i are at most k-ary and ψ is a first-order formula.

• $\mathcal{E}\mathcal{S}\mathcal{O}_{f}(m\forall )$ is the class of $\mathcal{E}\mathcal{S}\mathcal{O}$-sentences in Skolem normal form

  $$\displaystyle{ \exists f_{1}\ldots \exists f_{n}\forall x_{1}\ldots \forall x_{r}\psi, }$$

  where r ≤ m.

Such fragments of $\mathcal{E}\mathcal{S}\mathcal{O}$ have been widely studied and in particular their relationship with complexity classes. Roughly speaking, controlling the number of first-order variables in existential second-order logic amounts to control the polynomial degree in non-deterministic polynomial-time computations. To be more precise, it is known (see[22]) that, for k ≥ 1:

$$\displaystyle{\mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\mbox{ -ary},k\forall ) = \mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\forall ) = \mathsf{NTIME}_{\mathrm{RAM}}(n^{k}).}$$

where NTIME _RAM(n ^k) is the class of problems decidable by a non-deterministic random access machine in time O(n ^k). We can now relate the expressive power of these various fragments.

First, reusing of variables is a key issue in team semantics. It turns out that the following result is true (see [6]).

Proposition 2.

Any sentence of dependence logic is logically equivalent to a sentence in which at most one variable is universally quantified (possibly several times).

For what concerns dependence logic, the correspondence with existential second-order logic for the fragments with bounded arity and bounded number of universal variables is as follows [6]:

Theorem 11.

For all integers k ≥ 1,

• $\mathcal{D}(k\mathrm{-ary}) = \mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\mathrm{-ary})$ ,

• $\mathcal{D}(k\forall ) \leq \mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\forall ) \leq \mathcal{D}(2k\forall )$ .

Roughly speaking, dependence logic can be seen as existential second-order logic with functions (dependence atoms) but “without proper names” for these functions. Hence composition of functions, that can be done freely in existential second-order logic, can be simulated only by using intermediate variables in dependence logic. So, as long as, only the arity of dependence atoms is fixed, one can obtain an exact correspondence between the fragments (as stated in Theorem 11). By contrast an exact correspondence between the fragments $\mathcal{D}(k\forall )$ and $\mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\forall )$ seems unlikely (see the second item of Theorem 11). However, it is possible to establish an exact correspondence between $\mathcal{D}(k\forall )$ and some syntactically restricted fragment of $\mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\forall )$ (see [6]).

Because inclusion and independence logic do not have the downward closure property, the situation is drastically different depending on whether the lax or the strict semantics are used (see [18, 24–26]).

Theorem 12.

Let k ≥ 1. The following holds in the lax semantics:

• $\mathcal{F}\mathcal{O}(\subseteq )(k\mathrm{-ary}) <\mathcal{F}\mathcal{O}(\subseteq )(k + 1\mathrm{-ary})$ ,

• $\mathcal{F}\mathcal{O}(\subseteq )(k\mathrm{-ary}) \leq \mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\mathrm{-ary}) = \mathcal{F}\mathcal{O}(\perp _{\mathrm{c}})(k\mathrm{-ary})$ ,

• $\mathcal{F}\mathcal{O}(\perp )(2\forall ) = \mathcal{F}\mathcal{O}(\perp )$ ,

• $\mathcal{F}\mathcal{O}(\subseteq )(1\forall ) = \mathcal{F}\mathcal{O}(\subseteq )$ .

For the strict semantics, the following results are true:

• $\mathcal{F}\mathcal{O}(\subseteq )(k\forall ) = \mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\forall ) = \mathsf{NTIME}_{\mathrm{RAM}}(n^{k})$ ,

• $\mathcal{F}\mathcal{O}(\perp _{\mathrm{c}})(k\forall ) \leq \mathcal{E}\mathcal{S}\mathcal{O}_{f}((k + 1)\forall )$ ,

• $\mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\forall ) \leq \mathcal{F}\mathcal{O}(\perp _{\mathrm{c}})(2k\forall )$ .

The results above imply that there is an infinite expressivity hierarchy for $\mathcal{D}(k\forall )$, $\mathcal{F}\mathcal{O}(\subseteq )(k\forall )$, and $\mathcal{F}\mathcal{O}(\perp _{\mathrm{c}})(k\forall )$. Indeed, it is well known (by a slight adaptation of classical non-deterministic time hierarchy [5]) that, for any integer k ≥ 1, NTIME _RAM(n ^k) is strictly included in NTIME _RAM(n ^k+1). Hence, for example, $\mathcal{D}(k\forall )$ is strictly less expressive than $\mathcal{D}((k + 1)\forall )$.

Similarly, one might ask whether there is a strict hierarchy based on arity for $\mathcal{D}$ or $\mathcal{F}\mathcal{O}(\perp _{c})$. For example, is $\mathcal{D}(k + 1\mathrm{-ary})$ strictly more expressive than $\mathcal{D}(k\mathrm{-ary})$ for all (or some) k ≥ 1. Such a hierarchy would imply the existence of a similar hierarchy for $\mathcal{E}\mathcal{S}\mathcal{O}_{f}(k\mathrm{-ary})$ which is a long-standing open question (for empty signature, this is known as the Spectrum Arity Hierarchy Conjecture [15]).

Finally, let us examine the situation when exclusion atoms are allowed in the syntax. It turns out that none of the approach above helps to control the arity correspondence between the corresponding fragments. By introducing mainly two new concepts, namely inclusion quantifier (an adaptation of the idea of quantifier relativization applied to inclusion atoms) and term value preserving disjunction, the following result is obtained in [51]:

Theorem 13.

For all integers k ≥ 1, $\mathcal{F}\mathcal{O}(\subseteq,\mid )(k\mathrm{-ary}) = \mathcal{E}\mathcal{S}\mathcal{O}(k\mathrm{-ary})$ .

Note that in this result the correspondence is with the relational fragment of existential second-order logic: no quantification on functions is allowed.

2.5 Satisfiability and Model Checking

In this section we briefly review results on satisfiability and model checking in the first-order dependence logic context.

We begin by recalling these problems for a logic $\mathcal{L}$:

• The Satisfiability Problem $\mathrm{SAT}[\mathcal{L}]$ is defined as

  $$\displaystyle{\mathrm{SAT}[\mathcal{L}]:=\{\phi \in \mathcal{L}\mid \mbox{ there is a structure $\mathcal{M}$ such that $\mathcal{M}\models \phi $}\}.}$$

• The Model-Checking Problem is defined as

  $$\displaystyle{\mathrm{MC}[\mathcal{L}]:=\{ (\phi, \mathbb{M})\mid \mathbb{M}\models \phi \}.}$$

Since, for sentences, dependence logic is equivalent to $\mathcal{E}\mathcal{S}\mathcal{O}$ the classical results [4, 55] on the Decision Problem (Entscheidungsproblem) of $\mathcal{F}\mathcal{O}$ imply that $\mathrm{SAT}[\mathcal{D}]$ is undecidable (Π ₁ ⁰-complete). In the case of first-order logic, these negative results spurred an extensive investigation of decidable fragments of $\mathcal{F}\mathcal{O}$. Henkin [33] was the first to consider fragments of first-order logic with a fixed number of variables. Satisfiability for the fragments with three or more variables is easily seen to be undecidable, but for two variables, it is decidable (see, e.g., [3]). The two-variable fragment of $\mathcal{F}\mathcal{O}$ is denoted by $\mathcal{F}\mathcal{O}^{2}$.

In [40], the two-variable fragment $\mathcal{D}^{2}$ (i.e. the sentences of $\mathcal{D}$ in which only variables x and y appear) of dependence logic was studied and the following result was obtained:

Theorem 14.

$\mathrm{SAT}[\mathcal{D}^{2}]$ is $\mathsf{NEXPTIME}$ -complete.

The complexity of the problem remains the same also for finite satisfiability, although there are sentences of $\mathcal{D}^{2}$ having only infinite models (the so-called infinity axioms). The proof of Theorem 14 is based on a polynomially bounded translation of sentences of $\mathcal{D}^{2}$ to $\varSigma _{1}^{1}(\mathcal{F}\mathcal{O}\mathcal{C}^{2})$- sentences, i.e., sentences of the form

$$\displaystyle{\exists R_{1}\ldots \exists R_{m}\phi,}$$

where ϕ is a $\mathcal{F}\mathcal{O}\mathcal{C}^{2}$-sentence. The logic $\mathcal{F}\mathcal{O}\mathcal{C}^{2}$ extends $\mathcal{F}\mathcal{O}^{2}$ by counting quantifiers $\exists ^{\geq i}x\phi (x)$ expressing that ϕ(x) is satisfied by at least i distinct elements. Theorem 14 then follows from the fact that satisfiability is NEXPTIME-complete for $\mathcal{F}\mathcal{O}\mathcal{C}^{2}$ [50]. It is worth noting that since $\mathcal{D}^{2}$ is not closed under classical negation, Theorem 14 does not solve the complexity of the validity problem for $\mathcal{D}^{2}$. In fact, this problem is still open.

Recently Theorem 14 has been generalized to logics of the form $\mathcal{F}\mathcal{O}^{2}(\mathcal{A})$ that replace dependence atoms of $\mathcal{D}^{2}$ by a certain collections $\mathcal{A}$ of generalized dependence atoms [41]. The result therein shows that $\mathrm{SAT}[\mathcal{F}\mathcal{O}^{2}(\mathcal{A})]$ is NEXPTIME-complete if the atoms in $\mathcal{A}$ are themselves $\varSigma _{1}^{1}(\mathcal{F}\mathcal{O}\mathcal{C}^{2})$-definable. This result can be used to show, e.g., that the satisfiability and finite satisfiability problems of the two-variable fragments of inclusion, exclusion, and independence logic are all NEXPTIME-complete.

The complexity of model checking of dependence logic and its variants has been studied in [20]. The paper introduces a general model-checking game for logics with team semantics, and by analyzing the corresponding games, shows several results on the complexity of model checking in the team semantics framework.

Theorem 15.

The model-checking problem for $\mathcal{D}$ is $\mathsf{NEXPTIME}$ -complete.

In [20] it is also showed that NEXPTIME is an upper bound for the complexity of model checking for any variant $\mathcal{F}\mathcal{O}(\mathcal{C})$ of $\mathcal{D}$ such that the atoms in $\mathcal{C}$ are PTIME-computable.

3 Propositional and Modal Dependence Logic

This section will be devoted to the study of team-based logics over Kripke structures, such as modal dependence logic and, as a special case thereof, propositional dependence logic. Again, we will survey results on expressiveness of the most important logics and on the complexity of the satisfiability and model-checking problems. We will first turn to modal logics and later mention briefly some results for the purely propositional case.

3.1 Preliminaries

We start by introducing team semantics for usual modal logic. The central semantic concept here is the Kripke model, which is a tuple K = (W, R, π) where W is a nonempty set of worlds, $R \subseteq W \times W$, and $\pi: P \rightarrow 2^{W}$, where P is a set of propositional variables. The idea here is that π determines which variables hold (are set to true) in each world. So every world carries a propositional assignment. In analogy to first-order logic, we want to express dependencies among the values of certain variables; so we have to evaluate formulas relative to a set of assignments, hence in our case a set of worlds. A team of a model K is thus defined to be a set $T \subseteq W$. The central basic concept underlying Väänänen’s modal dependence logic and all its variants, that modal formulas are evaluated not in a world but in a team, is made precise in the definitions to follow below.

Before that, we would like to point out that another formalism, independence-friendly modal logic, has also be considered. In analogy to Hintikka and Sandu’s independence-friendly logic $\mathcal{I}\mathcal{F}$ [34], the so-called slash modalities are introduced. Consider the example formula $\square _{1}(\Diamond_{2}/\square _{1})p$. It is evaluated like $\square\Diamond p$, but now the witness for ◊ has to be chosen independently of the witnesses for □ ; hence the formula states, when evaluated at w, that there is a world u accessible from all worlds v that are accessible from w, a kind of “confluence property”. There are several competing formalisms for modal independence-friendly logic, cf., e.g., [54].

Väänänen [58] when introducing modal dependence logic $\mathcal{M}\mathcal{D}\mathcal{L}$ made a step analogous to the introduction of dependencies in first-order dependence logic by extending the logical language with atoms $=\left (p_{1},\ldots,p_{n}\right )$ to express dependencies among propositional variables. Caveat: In modal dependencies we can express dependencies among variables, not among worlds, as one might first expect when thinking of the standard translation of modal logic into first-order logic.

In the following, we will define the syntax of the modal logics we consider by grammars in extended Backus-Naur form (EBNF).

Definition 4 (Syntax of $\mathcal{M}\mathcal{L}$).

$$\displaystyle{\varphi \mathop{\mathop{:}\mathop{:}}= p\mid \neg p\mid (\varphi \wedge \varphi )\mid (\varphi \vee \varphi )\mid\Diamond\varphi \mid \square \varphi,}$$

where p is an atomic proposition.

Definition 5 (Semantics of $\mathcal{M}\mathcal{L}$).

Let K = (W, R, π) be a Kripke model, let $T \subseteq W$ be a team, and let $\varphi$ be an $\mathcal{M}\mathcal{L}$-formula. We define when $K,T\models \varphi$ holds inductively:

• If $\varphi = p$, then $K,T\models \varphi$ if and only if $T \subseteq \pi (p)$.

• If $\varphi = \neg p$, then $K,T\models \varphi$ if and only if $T \cap \pi (p) =\emptyset$.

• If $\varphi =\psi \vee \chi$ for some formulas ψ and χ, then $K,T\models \varphi$ if and only if $T = T_{1} \cup T_{2}$ with $K,T_{1}\models \psi$ and $K,T_{2}\models \chi$.

• If $\varphi =\psi \wedge \chi$ for some formulas ψ and χ, then $K,T\models \varphi$ if and only if $K,T\models \psi$ and $K,T\models \chi$.

• If $\varphi =?\Diamond\psi$ for some formula ψ, then $K,T\models \varphi$ if and only if there is some team T′ of K such that $K,T'\models \psi$, for each w ∈ T, there is some w′ ∈ T′ with (w, w′) ∈ R, and for each w′ ∈ T′, there is some w ∈ T with (w, w′) ∈ R.

• If $\varphi = \square \psi$ for some formula ψ, then $K,T\models \varphi$ if and only if $K,T'\models \psi$, where T′ is the set $\left \{w' \in W\ \vert \ (w,w') \in R\text{ for some }w \in T\right \}$.

Team semantics for $\mathcal{M}\mathcal{L}$ shares the so-called flatness property, see also Theorem 1:

Lemma 1 (Flatness of $\mathcal{M}\mathcal{L}$).

For all $K,T,\varphi$ , $K,T\models \varphi$ if and only if for all w ∈ T, we have $K,w\models \varphi$ .

So there is no essential semantic effect of team semantics compared to the usual semantics for modal logic. This changes when enriching the language with dependence atoms.

Definition 6 (Syntax of $\mathcal{M}\mathcal{D}\mathcal{L}$).

$$\displaystyle{\varphi \mathop{\mathop{:}\mathop{:}}= p\mid \neg p\mid =\!\left (\{p,\}\,p\right )\mid (\varphi \wedge \varphi )\mid (\varphi \vee \varphi )\mid\Diamond\varphi \mid \square \varphi,}$$

where p is an atomic proposition.

Before defining the semantics of dependence atoms, we introduce a useful shorthand notation.

Definition 7.

Let $\mathbf{p} = (p_{1},\ldots,p_{n})$ be a sequence of atomic propositions and w, w′ be worlds of a Kripke model K = (W, R, π). Then w and w′ are equivalent under π over $\mathbf{p}$, denoted by $w \equiv _{\pi,\mathbf{p}}w'$, if the following holds:

$$\displaystyle{\pi (w) \cap \{ p_{1},\ldots,p_{n}\} =\pi (w') \cap \{ p_{1},\ldots,p_{n}\}.}$$

Definition 8 (Semantics of $\mathcal{M}\mathcal{D}\mathcal{L}$).

We extend Definition 5 by the following clause:

• $K,T\models =\left (\mathbf{p},q\right )$ if and only if for all w ₁, w ₂ ∈ T: if $w_{1} \equiv _{\pi,\mathbf{p}}w_{2}$, then $w_{1} \equiv _{\pi,q}w_{2}$.

Theorem 16 (Downwards Closure).

Let ϕ be a $\mathcal{M}\mathcal{D}\mathcal{L}$ -formula. Then for all Kripke model K and teams T, if $K,T\models \phi$ and $T' \subseteq T$ , then $K,T'\models \phi$ .

As in the first-order case, also the independence atom has been introduced into modal logic, thus leading to modal independence logic [42].

Definition 9 (Syntax of $\mathcal{M}\mathcal{I}\mathcal{L}$).

$$\displaystyle{\varphi \mathop{\mathop{:}\mathop{:}}= p\mid \neg p\mid \{p\}\,p\perp _{\{p\}}\,\{p\}\,p\mid (\varphi \wedge \varphi )\mid (\varphi \vee \varphi )\mid?\Diamond\varphi \mid \square \varphi,}$$

where p is an atomic proposition.

Definition 10 (Semantics of $\mathcal{M}\mathcal{I}\mathcal{L}$).

We extend Definition 5 by the following clause, where $\mathbf{p},\mathbf{q},\mathbf{r}$ are sequences of atomic propositions:

• $K,T\models \mathbf{p}\perp _{\mathbf{r}}\,\mathbf{q}$ if and only if for all w ₁, w ₂ ∈ T such that $w_{1} \equiv _{\pi,\mathbf{r}}w_{2}$ there exists w ₃ ∈ T such that $w_{1} \equiv _{\pi,\mathbf{r}}w_{3}$, $w_{1} \equiv _{\pi,\mathbf{p}}w_{3}$, and $w_{2} \equiv _{\pi,\mathbf{q}}w_{3}$.

We note that one motivation behind the introduction of $\mathcal{M}\mathcal{I}\mathcal{L}$ was that it can be used to express security of cryptographic protocols, see [42].

At this point, where we have extended basic modal logic by a dependence as well as an independence atom, we would like to point out that there is a general way to introduce such so-called generalized dependence atoms, expressing further $\mathcal{F}\mathcal{O}$-definable properties on teams. To make this precise, consider an $\mathcal{F}\mathcal{O}$-formula $\varphi$. We say that $\varphi$ defines the atom D if

$$\displaystyle{K,T\models D(p_{1},\ldots,p_{n})\;\Longleftrightarrow\;\mathfrak{A}\models \varphi,}$$

where the structure $\mathfrak{A}$ has universe T and unary relations $A_{p_{i}}^{\mathfrak{A}}$ with $w \in A_{p_{i}}^{\mathfrak{A}}$ iff p _i  ∈ π(w).

$\mathcal{F}\mathcal{O}$-definitions of dependence, independence, and some further team properties can be found in Table 1. There, boldface symbols denote sequences of propositional variables.

A further possible extension of the so far considered modal logics is by introducing additional propositional connectives. In Section 2.1, different forms of implication and negation have been defined. Here we just define $\mathcal{M}\mathcal{T}\mathcal{L}$, modal team logic, to extend $\mathcal{M}\mathcal{L}$ by a second type of negation, denoted by $\sim$ and interpreted just as classical negation.

Definition 11 (Syntax of $\mathcal{M}\mathcal{T}\mathcal{L}$).

$$\displaystyle{\varphi \mathop{\mathop{:}\mathop{:}}= p\mid \neg p\mid \sim \varphi \mid (\varphi \wedge \varphi )\mid (\varphi \vee \varphi )\mid\Diamond\varphi \mid \square \varphi,}$$

where p is a propositional variable.

Definition 12 (Semantics of $\mathcal{M}\mathcal{T}\mathcal{L}$).

We extend Definition 5 by the following clause:

• If $\varphi = \sim \psi$ for some formula ψ, then $K,T\models \varphi$ if and only if $K,T\nvDash \psi$.

We note that usually (see [47]), $\mathcal{M}\mathcal{T}\mathcal{L}$ also contains dependence atoms; however, since these atoms can be expressed in $\mathcal{M}\mathcal{T}\mathcal{L}$ we omit them in the syntax. To make clear what the power of classical negation in this context is, we discuss the definition of dependence as well as some additional propositional connectives in $\mathcal{M}\mathcal{T}\mathcal{L}$.

First, the classical disjunction is readily expressed in $\mathcal{M}\mathcal{T}\mathcal{L}$: is logically equivalent to $\sim (\sim \varphi \wedge \sim \psi )$. Next we note that, analogously to the first-order case [1], the atom $=\left (p_{1},\ldots,p_{n}\right )$ is logically equivalent with

$$\displaystyle{(\bigwedge _{1\leq i\leq n-1}=\!\left (p_{i}\right )) \rightarrow =\!\left (p_{n}\right ),}$$

where $\rightarrow$ is the modal version of the intuitionistic implication with the semantics

$$\displaystyle{K,T\models \varphi \rightarrow \psi \mbox{ iff for all $T' \subseteq T$: if $K,T'\models \varphi $ then $K,T'\models \psi $}.}$$

The connective $\rightarrow$ has a short logically equivalent definition in $\mathcal{M}\mathcal{T}\mathcal{L}$ (see [47]), hence so does the atom $=\left (p_{1},\ldots,p_{n}\right )$. The intuitionistic implication has been studied in the modal team semantics context in [63].

We want to mention one final extension of modal dependence logic in this section, the so-called extended modal dependence logic, $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$. It allows $\mathcal{M}\mathcal{L}$-formulas instead of atoms inside the dependence atom [10].

Definition 13 (Syntax of $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$).

$$\displaystyle{\varphi \mathop{\mathop{:}\mathop{:}}= p\mid \neg p\mid =\!\left (\{\psi,\}\,\psi \right )\mid (\varphi \wedge \varphi )\mid (\varphi \vee \varphi )\mid?\Diamond\varphi \mid \square \varphi,}$$

where p is an atomic proposition and ψ is an $\mathcal{M}\mathcal{L}$-formula.

Definition 14 (Semantics of $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$).

We extend Definition 5 by the following clause:

• $K,T\models =\!\left (\psi _{1},\ldots,\psi _{n}\right )$ if for all w ₁, w ₂ ∈ T, if $K,\{w_{1}\}\models \psi _{i} \Leftrightarrow K,\{w_{2}\}\models \psi _{i}$ for 1 ≤ i ≤ n − 1, then $K,\{w_{1}\}\models \psi _{n} \Leftrightarrow K,\{w_{2}\}\models \psi _{n}$.

The interest in $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ stems mainly from the fact, that it allows us to formulate some basic temporal dependencies. We give only one very simple example: The formula

$$\displaystyle{=\!\left (\Diamond p,\Diamond^{2}p,\ldots,\Diamond^{n}p,p\right )}$$

expresses that “truth of p at this moment only depends on the truth of p in the previous n time steps” (on frame classes where the relation R denotes a backwards-oriented time-relation). So in a sense, $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ can be seen as a basic temporal dependence logic.

We would like to point out that $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ shares the downwards closure property of $\mathcal{M}\mathcal{D}\mathcal{L}$, but analogously to the first-order case, neither $\mathcal{M}\mathcal{I}\mathcal{L}$ nor $\mathcal{M}\mathcal{T}\mathcal{L}$ has this property.

3.2 Expressivity

The first results on expressive power of modal team-based logics are due to Sevenster [53]:

Theorem 17.

• 1. $\mathcal{M}\mathcal{D}\mathcal{L}$ is strictly more expressive than $\mathcal{M}\mathcal{L}$ .

• 2. On singleton teams of evaluation, $\mathcal{M}\mathcal{D}\mathcal{L}$ is as expressive as $\mathcal{M}\mathcal{L}$ .

While the first result simply follows from the fact that $\mathcal{M}\mathcal{L}$ is closed under union (of teams) but $\mathcal{M}\mathcal{D}\mathcal{L}$ is not, the second result requires an interesting proof that we would like to sketch. Given an $\mathcal{M}\mathcal{D}\mathcal{L}$-formula $\varphi$, we first use existentially quantified (Boolean) Skolem functions to replace dependence atoms. Next, we replace the existential quantifier by a big classical disjunction over all possibilities for such functions. The result now follows since over singleton teams, the interpretations of the connectives and ∨ agree.

This proof sketch points out the importance of classical disjunction. If we add to $\mathcal{M}\mathcal{L}$ or $\mathcal{M}\mathcal{D}\mathcal{L}$ we obtain the same expressive power, namely that of $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ [10, 29]:

Theorem 18.

Concerning modal independence logic, the following is known [42]:

Theorem 19.

• 1. $\mathcal{M}\mathcal{L} <\mathcal{M}\mathcal{D}\mathcal{L} <\mathcal{M}\mathcal{I}\mathcal{L}$ .

• 2. On singleton teams of evaluation, $\mathcal{M}\mathcal{I}\mathcal{L}$ is as expressive as $\mathcal{M}\mathcal{L}$ .

Again, the first result follows from simple closure properties. We will sketch the proof of the second result, since it will lead us to an important topic. Given an $\mathcal{M}\mathcal{I}\mathcal{L}$-formula $\varphi$, it is clear that on singleton teams it captures a property of Kripke models that

• is invariant under modal bisimulation (more on that in the next paragraph),

• only depends on the worlds that can be reached in a number of steps bounded by the modal depth of the formula.

These observations allow us to construct an $\mathcal{M}\mathcal{L}$-formula that describes (by a big disjunction) all possibilities for satisfying Kripke models.

The just given proof can be extended to show that on singleton teams, $\mathcal{M}\mathcal{L}$ extended by any $\mathcal{F}\mathcal{O}$-definable dependence atoms (see Table 1) is as expressive as $\mathcal{M}\mathcal{L}$.

The ideas used in the just sketched proof go back to a fundamental result by Johan van Benthem [59], characterizing exactly the properties of Kripke structures that modal logic $\mathcal{M}\mathcal{L}$ can define in terms of the so-called bisimilarity. His results can be generalized to modal team logic, as we describe next.

Definition 15 (k-bisimulation).

Let K ₁ = (W ₁, R ₁, π ₁) and K ₂ = (W ₂, R ₂, π ₂) be Kripke models. We define inductively what it means for worlds w ₁ ∈ W ₁ and w ₂ ∈ W ₂ to be k-bisimilar, for some $k \in \mathbb{N}$, written as $(K_{1},w_{1})\rightleftharpoons _{k}(K_{2},w_{2})$.

• $(K_{1},w_{1})\rightleftharpoons _{0}(K_{2},w_{2})$ holds if for each propositional variable p, we have that $K_{1},w_{1}\models p$ if and only if $K_{2},w_{2}\models p$.

• $(K_{1},w_{1})\rightleftharpoons _{k+1}(K_{2},w_{2})$ holds if the following three conditions are satisfied:

  • 1. $(K_{1},w_{1})\rightleftharpoons _{0}(K_{2},w_{2})$,

  • 2. for each successor w ₁′ of w ₁ in K ₁, there is a successor w ₂′ of w ₂ in K ₂ such that $(K_{1},w_{1}')\rightleftharpoons _{k}(K_{2},w_{2}')$ (forward condition),

  • 3. for each successor w ₂′ of w ₂ in K ₂, there is a successor w ₁′ of w ₁ in K ₁ such that $(K_{1},w_{1}')\rightleftharpoons _{k}(K_{2},w_{2}')$ (backward condition).

Full bisimulation is defined analogously as follows:

Definition 16 (full bisimulation).

Let $K_{1} = (W_{1},R_{1},\pi _{1}),K_{2} = (W_{2},R_{2},\pi _{2})$ be Kripke models and let w ₁ and w ₂ be worlds of K ₁ and K ₂. Then (K ₁, w ₁) and (K ₂, w ₂) are bisimilar, written as $(K_{1},w_{1})\rightleftharpoons _{}(K_{2},w_{2})$, if there is a relation $Z \subseteq W_{1} \times W_{2}$ such that (w ₁, w ₂) ∈ Z, and Z fulfils the following closure property:

• $(K_{1},w_{1})\rightleftharpoons _{0}(K_{2},w_{2})$, for all (w ₁, w ₂) ∈ Z,

• for each successor w ₁′ of w ₁ in K ₁, there is a successor w ₂′ of w ₂ in K ₂ with (w ₁′, w ₂′) ∈ Z (forward condition),

• for each successor w ₂′ of w ₂ in K ₂, there is a successor w ₁′ of w ₁ in K ₁ with (w ₁′, w ₂′) ∈ Z (backward condition).

The famous theorem by van Benthem characterizing the expressive power of modal logics can now be stated as follows:

A property of pointed models is a class of pairs (K, w), where K is a Kripke model and w a world of K. For a formula $\varphi$ we say that $\varphi$ expresses the property $\left \{(K,w)\ \vert \ K,w\models \varphi \right \}$ (under the usual Kripke semantics). A team property is bisimulation-invariant if it is closed under bisimulation.

Theorem 20 (van Benthem’s Theorem [59]).

Let P be a property of pointed Kripke structures. There is an $\mathcal{M}\mathcal{L}$ -formula which expresses P if and only if there is a first-order formula which expresses P and P is bisimulation-invariant.

The result of van Benthem has been transferred into the field of modal logics with team semantics, as we want to explain next. First, the notion of bisimulation can very naturally be lifted to teams.

Definition 17 (team bisimulation).

Let K ₁ = (W ₁, R ₁, π ₁), K ₂ = (W ₂, R ₂, π ₂) be Kripke models, let T ₁ and T ₂ be teams of K ₁ and K ₂. Then (K ₁, T ₁) and (K ₂, T ₂) are k-bisimilar, written as $K_{1},T_{1}\rightleftharpoons _{k}K_{2},T_{2}$ if the following holds:

• for each w ₁ ∈ T ₁, there is some w ₂ ∈ T ₂ such that $(K_{1},w_{1})\rightleftharpoons _{k}(K_{2},w_{2})$,

• for each w ₂ ∈ T ₂, there is some w ₁ ∈ T ₁ such that $(K_{1},w_{1})\rightleftharpoons _{k}(K_{2},w_{2})$.

Analogously, we say that (K ₁, T ₁) and (K ₂, T ₂) are (fully) bisimilar, written as $K_{1},T_{1}\rightleftharpoons _{}K_{2},T_{2}$ if the following holds:

• for each w ₁ ∈ T ₁, there is some w ₂ ∈ T ₂ such that $(K_{1},w_{1})\rightleftharpoons _{}(K_{2},w_{2})$,

• for each w ₂ ∈ T ₂, there is some w ₁ ∈ T ₁ such that $(K_{1},w_{1})\rightleftharpoons _{}(K_{2},w_{2})$.

Now we can characterize the expressive power of some of our modal logics. The expressive power of a logic here is defined to be the set of properties expressible in it. More precisely, a team property is a class of pairs (K, T), where K is a Kripke model and T a team of K. For a formula $\varphi$ we say that $\varphi$ expresses the property $\left \{(K,T)\ \vert \ K,T\models \varphi \right \}$. A team property is bisimulation-invariant if it is closed under bisimulation.

The following characterizations of the expressive power of $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ and $\mathcal{M}\mathcal{T}\mathcal{L}$ were obtained in [29, 43]:

Theorem 21.

Let P be a team property.

• 1. There is an $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ -formula which expresses P if and only if P is invariant under k-bisimulation for some k and downwards-closed.

• 2. There is an $\mathcal{M}\mathcal{T}\mathcal{L}$ -formula which expresses P if and only if P is invariant unter k-bisimulation for some k.

While the just given result already completely settles the question of expressivity of $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ and $\mathcal{M}\mathcal{T}\mathcal{L}$ in terms of bisimulation, the following complete analogue of van Benthem’s Theorem was finally obtained in [43]:

Theorem 22.

Let P be a team property. There is an $\mathcal{M}\mathcal{T}\mathcal{L}$ -formula which expresses P if and only if there is a first-order formula which expresses P and P is bisimulation-invariant.

It is worth to note that all our extensions of modal logic by further connectives or generalized dependence atoms define only team properties that are bisimulation-invariant. Hence the just given theorem implies that modal team logic $\mathcal{M}\mathcal{T}\mathcal{L}$ gives an upper bound with respect to expressivity for all these logics. In particular, modal logic with team semantics and classical negation is sufficient to express all FO-definable generalized dependence atoms. This observation can be strengthened as follows [43]:

Let ML ^FO denote the extension of $\mathcal{M}\mathcal{L}$ by all generalized dependence atoms D that are $\mathcal{F}\mathcal{O}$-definable without identity, in the extended setting, i.e., dependence atoms are applied not only to propositions but $\mathcal{M}\mathcal{L}$-formulae.

Theorem 23.

$\mathsf{ML}^{\mathsf{FO}}$ is equally expressive as $\mathcal{M}\mathcal{T}\mathcal{L}$ .

3.3 Complexity

The starting point for complexity studies of modal logic is a paper by Ladner from 1977 [45] in which he proved the following theorem:

Theorem 24.

Satisfiability for modal logic $\mathcal{M}\mathcal{L}$ is $\mathsf{PSPACE}$ -complete.

His result easily carries over from the usual modal semantics to team semantics. The upper bound follows from Ladner’s so-called witness algorithm, which is not so important for us here. The lower bound is given by a reduction from the standard PSPACE-complete problem QBF, the evaluation problem for quantified Boolean formulas, where alternations of modalities are used to force a satisfying Kripke model to imitate the evaluation tree of the given formula [2].

In a very clever way this was extended by Sevenster [53] as follows:

Theorem 25.

Satisfiability for $\mathcal{M}\mathcal{D}\mathcal{L}$ is $\mathsf{NEXPTIME}$ -complete.

To prove the upper bound, one has to express the dependencies by Boolean Skolem functions, similar as in the proof of Theorem 17. Then we can use nondeterminism to guess those functions in exponential time, and check satisfiability. For the lower bound, Sevenster presents a reduction from Dependence-QBF, a variant of the above-mentioned QBF extended by dependencies among variables [49], a problem which is NEXPTIME-complete. This reduction is essentially Ladner’s reduction extended by dependence atoms.

Lohmann and Vollmer [46] extended Sevenster’s result by determining the complexity of every fragment of $\mathcal{M}\mathcal{D}\mathcal{L}$, given by any subset of the modalities □ and ◊ , by restricting the allowed propositional connectives to any subset of and by considering fragments with and without dependence atoms. Their results can be summarized as in Table 2. An entry “+” in the table means that the syntactic element is allowed, “−” means it is forbidden, and “∗” means that the complexity does not depend on whether the element is present or not. All rows in the table denote completeness results for the respective complexity class under polynomial-time many-one reductions, except those for PTIME.

Table 2 Complexity of satisfiability for fragments of modal dependence logic

In a similar way, the complexity of the model-checking problem for fragments of modal dependence logic has been classified in [9]. For some fragments, model checking is NP-complete, for others it is solvable in polynomial time.

Theorem 26.

Model checking for $\mathcal{M}\mathcal{D}\mathcal{L}$ is $\mathsf{NP}$ -complete.

We want to turn to the explanation of one special case in Table 2, the complexity of Poor Man’s Logic. In the context of modal logic, poor man’s formulas are just formulas that do not contain ∨. Hemaspaandra [31, 32] showed that poor man’s modal logic is PSPACE-complete over the class of Kripke structures in which every world has at most two successors. The proof is again by a reduction from QBF, where we express the QBF-tree by alternations of modalities. Important now is that without disjunction, we cannot express the tree-structure. In fact, satisfiability for poor man’s modal logic over K (the class of all Kripke structures) is only coNP-complete. The requirement that in every model each world has at most two successors is essential for the complexity. Lohmann and Vollmer [46] showed:

Theorem 27.

Poor man’s modal dependence logic, i.e., the fragment of modal dependence logic allowing only the propositional connectives ∧ and $\neg$ (besides the two modalites and dependence atoms), is $\mathsf{NEXPTIME}$ -complete.

The proof relies as before on a reduction from Dependence-QBF. We express the QBF-tree by alternations of modalities. As in the case of Hemaspaandra’s proof we cannot enforce tree-structure of the Kripke model without disjunction. In this case, however, we can use dependence atoms to ensure that everything in the model that does not belong to the tree is essentially nothing else than a copy of a subtree; hence, in difference to Hemaspaandra, we do not need the requirement about the number of successors of a world.

Next, we turn to modal independence logic. The following has been proven in [42]:

Theorem 28.

Satisfiability for $\mathcal{M}\mathcal{I}\mathcal{L}$ is $\mathsf{NEXPTIME}$ -complete.

While the lower bound follows trivially from the complexity result for $\mathcal{M}\mathcal{D}\mathcal{L}$, the upper bound is proven by an embedding of $\mathcal{M}\mathcal{I}\mathcal{L}$ into the Gödel-Kalmár-Schütte fragment of all $\mathcal{F}\mathcal{O}$-sentences with prefix $\exists ^{{\ast}}\forall ^{2}\exists ^{{\ast}}$ (without function symbols, without equality) in a satisfiability preserving way. This fragment is decidable in NEXPTIME [3]. This proof thus is different from the one given by Sevenster (and it is not clear how to extend his ideas to include the independence atom), but it yields Sevenster’s result as a corollary.

The embedding into the $\mathcal{F}\mathcal{O}$-fragment is even possible in a much more general context [42]:

Theorem 29.

Satisfiability for $\mathcal{M}\mathcal{L}$ extended by dependence atoms that can be defined in $\exists ^{{\ast}}\forall ^{2}\exists ^{{\ast}}$ is in $\mathsf{NEXPTIME}$ .

For a large class of generalized dependence atoms, satisfiability can thus be placed into the class NEXPTIME, while for a few particular atoms, we have completeness—above we already mentioned this for dependence and independence, and in [30], satisfiability for modal inclusion logic $\mathcal{M}\mathcal{I}\mathcal{N}\mathcal{C}\mathcal{L}$, i.e., $\mathcal{M}\mathcal{L}$ extended by the inclusion atom (see Table 1), was shown to be NEXPTIME-complete as well.

Also the model-checking problem for modal logic extended by generalized dependence atoms was studied in [42].

Theorem 30.

Model checking for $\mathcal{M}\mathcal{L}$ extended by $\mathcal{F}\mathcal{O}$ -definable dependence atoms is in $\mathsf{NP}$ .

Recall that by Theorem 26 model checking for $\mathcal{M}\mathcal{D}\mathcal{L}$ (and also for $\mathcal{M}\mathcal{I}\mathcal{L}$) is NP-complete.

3.4 Propositional Logic

Propositional logic with team semantics is nothing else than modal logic with team semantics but without connections between the team members (worlds). The syntax is the following:

Definition 18 (Syntax of $\mathcal{P}\mathcal{L}$).

$$\displaystyle{\varphi \mathop{\mathop{:}\mathop{:}}= p\mid \neg p\mid (\varphi \wedge \varphi )\mid (\varphi \vee \varphi ),\quad \mbox{ where $p \in \varPhi $}.}$$

The semantics is exactly the same as for the modal case. Propositional logic can now be extended by different generalized dependence atoms (such as those given in Table 1) as well as different propositional connectives (intuitionistic implication, classical disjunction, etc.) The expressive power of some of these logics (i.e. the classes of teams that are definable) has been studied by Yang [63]; in particular, propositional dependence logic ($\mathcal{P}\mathcal{L}$ plus dependence atoms) can define all nonempty downwards-closed team properties, and propositional team logic ($\mathcal{P}\mathcal{L}$ plus classical negation) can define all team properties.

Concerning complexity questions, the following results are known:

Theorem 31.

• 1. The satisfiability and the model-checking problems for propositional dependence logic and propositional independence logic are $\mathsf{NP}$ -complete [9, 27, 46] .

• 2. The satisfiability problem for propositional inclusion logic is $\mathsf{EXPTIME}$ -complete [30] , while its model-checking problem is in $\mathsf{PTIME}$ (Lauri Hella, personal communication).

• 3. The model-checking problem for propositional dependence logic extended by classical negation is $\mathsf{PSPACE}$ -complete [47] .

• 4. The satisfiability problem for propositional inclusion logic extended by classical negation as well as for propositional independence logic extended by classical negation is complete for the class $\mathsf{AEXPTIME(poly)}$ of all problems solvable by alternating Turing machines in exponential time making only a polynomial number of alternations; the model-checking problem for both logics is $\mathsf{PSPACE}$ -complete [30] .

Besides the above-summarized results, also the validity problem for propositional logic and some of its extensions have been studied. It is worth noting that, unlike for classical logics closed under the classical negation, the satisfiability problem and the validity problem for most of the logics discussed in this article are not dual to each other. Partial results for axiomatizability have also been obtained [27, 52, 61, 64].

4 Conclusion

• 1. A number of complexity questions for fragments of first-order dependence logic or variants remain unsettled. The complexity of the validity problem for $\mathcal{D}^{2}$ is one example. More generally, one might ask what decidability results for first-order logic, e.g., for formula classes defined by restricted quantifier prefixes, transfer into the context of team-based logics.

• 2. While many expressivity results of modal and propositional logic have been stated in this survey and this issue is more or less settled in the first-order case, it has to be mentioned that some very basic cases in modal logic still remain unsettled. In particular, what is the expressive power of propositional or modal independence logic? It is worth noting that very recently a version of Theorem 21 for (extended) modal inclusion logic has been shown in [28].

• 3. In Section 3.2 we stated equal expressivity for many dialects of modal logics. However, we did not touch the topic of succinctness. As an example, while on singleton teams of evaluation, $\mathcal{M}\mathcal{I}\mathcal{L}$ equally expressive than $\mathcal{M}\mathcal{L}$, it can be proven that it is exponentially more succinct [42]. Also, in Theorem 18 we stated that $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ and $\mathcal{M}\mathcal{L}$ plus classical disjunction have the same expressive power. In [29] it was shown that any translation from $\mathcal{E}\mathcal{M}\mathcal{D}\mathcal{L}$ to $\mathcal{M}\mathcal{L}$ with disjunction necessarily leads to an exponential blow-up in formula size. In most other cases, the question of succinctness remains unsettled so far.

• 4. The question of axiomatizability has not been covered in detail in this survey. We mention that axiomatizability of some sublogics of $\mathcal{M}\mathcal{T}\mathcal{L}$ has been studied, e.g., in [63] and [52], but remains open for many logics. Related to this is the complexity of the tautology problem. In particular it remains open if we can axiomatize $\mathcal{M}\mathcal{T}\mathcal{L}$.

• 5. While we mentioned a number of complexity results on modal dependence logic and some of its extensions, this issue remains unsettled for full $\mathcal{M}\mathcal{T}\mathcal{L}$. In particular, what is the complexity of satisfiability and validity of $\mathcal{M}\mathcal{T}\mathcal{L}$?