On Dependence Logic

Abstract

Dependence logic extends the language of first order logic by means of dependence atoms and aims to establish a basic theory of dependence and independence underlying such seemingly unrelated subjects as causality, random variables, bound variables in logic, database theory, the theory of social choice, and even quantum physics. In this work we summarize the setting of dependence logic and recall the main results of this rapidly developing area of research.

J. Väänänen’s research partially supported by grant 40734 of the Academy of Finland and the EUROCORES LogICCC LINT programme.

P. Galliani’s research partially supported by the EUROCORES LogICCC LINT programme, by the Väisälä Foundation and by by Grant 264917 of the Academy of Finland.

1 Introduction

The goal of dependence logic is to establish a basic theory of dependence and independence underlying such seemingly unrelated subjects as causality, random variables, bound variables in logic, database theory, the theory of social choice, and even quantum physics. There is an avalanche of new results in this field demonstrating remarkable convergence. The concepts of (in)dependence in the different fields of humanities and sciences have surprisingly much in common and a common logic is starting to emerge.

Dependence logic [29] arose from the compositional semantics of Wilfrid Hodges [19] for the independence friendly logic [18, 25]. In dependence logic the basic semantic concept is not that of an assignment $s$ satisfying a formula $\phi$ in a model $\mathfrak {M}$,

$$ \mathfrak {M}\models _s\phi , $$

as in first order logic, but rather the concept of a set $S$ of assignments satisfying $\phi$ in $\mathfrak {M}$,

$$ \mathfrak {M}\models _S\phi . $$

Defining satisfaction relative to a set of assignments opens up the possibility to express dependence phenomena, roughly as passing in propositional logic from one valuation to a Kripke model leads to the possibility to express modality. The focus in dependence logic is not on truth values but on variable values. We are interested in dependencies between individuals rather than between propositions.

In [3] Johan van Benthem writes:

$$\begin{aligned} \begin{array}{l} ``\textit{Sets of assignments S encode several kinds of}\, `\textit{dependence}{\text {'}} \\ \textit{between variables. There may not be one single intuition.} \\ `\textit{Dependence}{\text {'}} \textit{may} \textit{mean functional dependence} \\ (\textit{if two assignments agree in S on} x, \textit{they also agree on} y),\\ \textit{but also other kinds of}\,`\textit{correlation}{\text {'}} \textit{among value ranges.} \\ ... \\ \textit{Different dependence relations may have different mathematical}\\ \textit{properties and suggest different logical formalisms.}{\text {''}} \end{array} \end{aligned}$$

(4.1)

This is actually how things have turned out. For a start, using the concept of functional dependence it is possible, as Wilfrid Hodges [19] demonstrated, to define compositionally¹ the semantics of independence friendly logic, the extension of first order logic by the quantifier

$$ \exists x/y\phi \quad \text{ i.e. } \text {``}\text{ there } \text{ is } \text{ an } \ x, \text{ independently } \text{ of } \ y, \text{ such } \text{ that } \ \phi \text {''}, $$

as follows: Suppose $S$ is a team of assignments, a “plural state”, in a model $\mathfrak {M}$. Then

$$ \mathfrak {M}\models _S\exists x/y\phi $$

if and only if there is another set $S{^\prime }$ such that

$$\mathfrak {M}\models _{S{^\prime }}\phi $$

and the following “transition”-conditions hold:

• If $s\in S$, then there is $s{^\prime }\in S{^\prime }$ such that if $z$ is a variable other than $x$, then $s(z)=s{^\prime }(z)$.

• If $s{^\prime }\in S{^\prime }$, then there is $s\in S$ such that if $z$ is a variable other than $x$, then $s(z)=s{^\prime }(z)$.

• If $s,s{^\prime }\in S{^\prime }$ and $s(z)=s{^\prime }(z)$ for all variables other than $y$ or $x$, then $s(x)=s{^\prime }(x)$.

In a sense, independence friendly logic is a logical formalism suggested by the functional dependence relation, but its origin is in game theoretical semantics, not in dependence relations. With dependence logic the situation is different. It was directly inspired by the functional dependence relation introduced by Wilfrid Hodges.

Peter van Emde Boas pointed out to the second author in the fall of 2005 that the functional dependence behind dependence logic is known in database theory [2]. This led the second author to realize—eventually—that the dependence we are talking about here is not just about variables in logic but a much more general phenomenon, covering such diverse areas as algebra, statistics, computer science, medicine, biology, social science, etc.

As Johan van Benthem points out in (4.1), there are different dependence intuitions. Of course the same is true of intuitions about independence. For some time it was not clear what would be the most natural concept of independence. There was the obvious but rather weak form of independence of $x$ from $y$ as dependence of $x$ on some variable $z$ other than $y$. Eventually a strong form of independence was introduced in [15], which has led to a breakthrough in our understanding of dependence relations and their role.

We give an overview of some developments in dependence logic (Sect. 4.2) and independence logic (Sect. 4.3). This is a tiny selection, intended for a newcomer, from a rapidly growing literature on the topic. Furthermore, in Sect. 4.4 we discuss conditional independence atoms and we prove a novel result—that is, that conditional and non-conditional independence logic are equivalent. Finally, in Sect. 4.6 we briefly discuss an application of our logics to belief representation.

2 Functional Dependence

The approach of [29] is that one should look for the strongest concept of dependence and use it to define weaker versions. Conceivably one could do the opposite, start from the weakest and use it to define stronger and strong concepts. The weakest dependence concept—whatever it is—did not offer itself immediately, so the strongest was more natural to start with. The wisdom of focusing in the extremes lies in the hope that the extremes are most likely to manifest simplicity and robustness, which would make them susceptible to a theoretical study.

Let us start with the strongest form of dependence, functional dependence. We use the vector notation $\vec {x}$ for finite sequences $x_1,\ldots ,x_n$ of variables.² We add to first order logic³ new atomic formulas

$$\begin{aligned} =(\vec {y},\vec {x}), \end{aligned}$$

(4.2)

with the intuitive meaning

$$\text{ the } \ \vec {y}\ \text{ totally } \text{ determine } \text{ the } \ \vec {x}. $$

In other words, the meaning of (4.2) is that the values of the variables $\vec {y}$ functionally determine the values of the variables $\vec {x}$. We think of the atomic formulas (4.2) on a par with the atomic formula $x=y$. In particular, the idea is that the formula (4.2) is a purely logical expression, not involving any non-logical symbols, in particular no function symbol for the purported function manifesting the functional dependence.

The best way to understand the concept (4.2) is to give it exact semantics: To this end, suppose $\mathfrak {M}$ is a model. Suppose $S$ is a set of assignments into $M$ (or a team as such sets are called). We define:

Definition 4.1

The team $S$ satisfies $=(\vec {y},\vec {x})$ in $\mathfrak {M}$, in symbols

$$ \mathfrak {M}\models _S \ =(\vec {y},\vec {x}) $$

if

$$\begin{aligned} \forall s,s{^\prime }\in S(s(\vec {y})=s{^\prime }(\vec {y})\rightarrow s(\vec {x})=s{^\prime }(\vec {x})).\end{aligned}$$

(4.3)

One may ask, why not define the meaning of $=\!(y,x)$ as “there is a function which maps $y$ to $x$”? The answer is that if we look at the meaning of $=(y,x)$ under one assignment $s$, then there always is a function $f$ mapping $s(y)$ to $s(x)$, namely the function $\{(s(y),s(x))\}$, and if we look at the meaning of $=(y,x)$ under many assignments, a team, then (4.3) is indeed equivalent to the statement that there is a function mapping $s(y)$ to $s(x)$ for all $s$ in the team.

A special case of $=(\vec {y},\vec {x})$ is $=(\vec {x})$, the constancy atom. The intuitive meaning of this atom is that the value of $\vec {x}$ is constant in the team. It results from $=(\vec {y},\vec {x})$ when $\vec {y}$ is the empty sequence.

Functional dependence has been studied in database theory and some basic properties, called Armstrong’s Axioms have been isolated [2]. These axioms state the following properties of $=(\vec {y},\vec {x})$:  

(A1) :

 $=(\vec {x},\vec {x})$. Anything is functionally dependent of itself.

(A2) :

If $=(\vec {y},\vec {x})$ and $\vec {y}\subseteq \vec {z}$, then $=(\vec {z},\vec {x})$. Functional dependence is preserved by increasing input data.

(A3) :

If $\vec {y}$ is a permutation of $\vec {z}$, $\vec {u}$ is a permutation of $\vec {x}$, and $=(\vec {z},\vec {x})$, then $=(\vec {y},\vec {u})$. Functional dependence does not look at the order of the variables.

(A4) :

If $=\vec {y},\vec {z})$ and $=\vec {z},\vec {x})$, then $=\vec {y},\vec {x})$. Functional dependences can be transitively composed.

The following result is well-known in the database community and included in textbooks of database theory⁴:

Theorem 4.2

[2] The axioms (A1)–(A4) are complete in the sense that a relation $=(\vec {y},\vec {x})$ follows by the rules (A1)–(A4) from a set $\Sigma$ of relations of the same form if and only if every team which satisfies $\Sigma$ satisfies $=(\vec {y},\vec {x})$.

Proof

Suppose $=\vec {y},\vec {x})$ does not follow by the rules from a set $\Sigma$ of atoms. Let $V$ be the set of variables $z$ such that $=(\vec {y},z)$ follows by the rules from $\Sigma$. Let $W$ be the remaining variables in $\Sigma \cup \{=(\vec {y},\vec {x})\}$. Thus $\vec {x}\cap W\ne \emptyset$. Consider the model $\{0,1\}$ of the empty vocabulary and the team

The atom $=(\vec {y},\vec {x})$ is not true in this team, because $\vec {y}\subseteq V$ and $\vec {x}\cap W\ne \emptyset$. Suppose then $=(\vec {v},\vec {w})$ is one of the assumptions. If each $v$ is in $V$, then so is each $w$ so they all get value $0$. On the other hand, if some $v$ is in $W$, it gets in this team two values, so it cannot violate dependence. $\square$

We now extend the truth definition (Definition 4.1) to the full first order logic augmented by the dependence atoms $=\!(\vec {x},\vec {y})$. To this end, let $s(a/x)$ denote the assignment which agrees with $s$ except that it gives $x$ the value $a$. We define for formulas which have negation in front of atomic formulas only:

$$\begin{aligned} \left. \begin{array}{lcl} \mathfrak {M}\models _S x=y &{} \iff &{} \forall s\in S(s(x)=s(y)).\\ \mathfrak {M}\models _S \lnot x=y&{}\iff &{}\forall s\in S(s(x)\ne s(y)).\\ \mathfrak {M}\models _S R(x_1,\ldots ,x_n)&{}\iff &{}\forall s\in S((s(x_1),\ldots ,s(x_n))\in R^\mathfrak {M}).\\ \mathfrak {M}\models _S \lnot R(x_1,\ldots ,x_n)&{}\iff &{}\forall s\in S((s(x_1),\ldots ,s(x_n))\notin R^\mathfrak {M}).\\ \mathfrak {M}\models _S\phi \wedge \psi &{}\iff &{}\mathfrak {M}\models _S\phi \ \text{ and } \ \mathfrak {M}\models _S\psi .\\ \mathfrak {M}\models _S\phi \vee \psi &{}\iff &{} \ \text{ There } \text{ are } \ S_1 \ \text{ and } \ S_2 \ \text{ such } \text{ that } \\ &{}&{} S=S_1\cup S_2, \mathfrak {M}\models _{S_1}\phi , \ \text{ and } \ \mathfrak {M}\models _{S_2}\psi .\\ \mathfrak {M}\models _S\exists x\phi &{}\iff &{}\mathfrak {M}\models _{S{^\prime }}\phi \ \text{ for } \text{ some } \ S{^\prime } \ \text{ such } \text{ that } \\ &{}&{}\forall s\in S\ \exists a\in M(s(a/x)\in S{^\prime })\\ \mathfrak {M}\models _S\forall x\phi &{}\iff &{} \mathfrak {M}\models _{S{^\prime }}\phi \ \text{ for } \text{ some } \ S{^\prime } \ \text{ such } \text{ that } \\ &{}&{}\forall s\in S\ \forall a\in M(s(a/x)\in S{^\prime })\\ \end{array}\right\} \end{aligned}$$

(4.4)

It is easy to see that for formulas not containing any dependence atoms, that is, for pure first order formulas $\phi$,

$$ \mathfrak {M}\models _{\{s\}}\phi \iff \mathfrak {M}\models _s\phi $$

and

$$ \mathfrak {M}\models _S\phi \iff \forall s\in S(\mathfrak {M}\models _s\phi ), $$

where $\mathfrak {M}\models _s\phi$ has its usual meaning. This shows that the truth conditions (4.4) agree with the usual Tarski truth conditions for first order formulas. Thus considering the “plural state” $S$ rather than individual “states” $s$ makes no difference for first order logic, but it makes it possible to give the dependence atoms $=(\vec {x},\vec {y})$ their intended meaning.

What about axioms for non-atomic formulas of dependence logic? Should we adopt new axioms, apart from the Armstrong Axioms [A1–A4]? There is a problem! Consider the sentence

$$\begin{aligned} \exists x\forall y\exists z(=(z,y)\wedge \lnot z=x). \end{aligned}$$

(4.5)

It is easy to see that this sentence is satisfied by a team in a model $\mathfrak {M}$ if and only $M$ is infinite. As a result, by general considerations going back to Gödel’s Incompleteness Theorem, the semantic consequence relation

$$ \phi \models \psi \iff \forall \mathfrak {M}\forall S(\mathfrak {M}\models _S\phi \rightarrow \mathfrak {M}\models _S\psi ) $$

is non-arithmetical. Thus there cannot be any completeness theorem in the usual sense. However, this does not prevent us from trying to find axioms and rules which are as complete as possible. This is what is done in [24], where a complete axiomatization is given for first order consequences of dependence logic sentences. The axioms are a little weaker than standard first order axioms when applied to dependence formulas, but on the other hand there are two special axioms for the purpose of dealing with dependence atoms as parts of formulas in a deduction. Rather than giving all details (which can be found in [24]) we give just an example of the use of both new rules.

Suppose we are given $\epsilon ,x,y$ and $f$, and we have already concluded, in the middle of some argument, the following:

$$\begin{aligned}&\textit{ if } {\epsilon }>0, \textit{then there is}\ \delta >0\,\textit{depending only on}\,\epsilon \,\textit{such that} \\&\textit{if} \ |x-y|<\delta , \textit{then} \ |f(x)-f(y)|<\epsilon . \end{aligned}$$

By merely logical reasons we should be able to conclude

$$\begin{aligned}&\textit{There is}\,\delta >0\,\textit{depending only on}\,\epsilon \,\textit{such that}\\&\textit{if}\,\epsilon >0\,\textit{and}\, |x-y|<\delta , \textit{then}\,|f(x)-f(y)|<\epsilon . \end{aligned}$$

Note that “depending only on $\epsilon$” has moved from inside the implication to outside of it. The new rule of dependence logic, isolated in [24], which permits this, is called Dependence Distribution Rule. Neither first order rules nor Armstrong’s Axioms give this because neither of them gives any clue of how to deal with dependence atoms as parts of bigger formulas.

Here is another example of inference in dependence logic: Suppose we have arrived at the following formula in the middle of some argument:

$$\begin{aligned}&\textit{For every}\, x\,\textit{and every}\, \epsilon >0\, \textit{there is}\,\delta >0\,\textit{depending only on}\, \epsilon \\&\textit{such that for all}\,y,\textit{if}\, |x-y|<\delta , \textit{then}\,|f(x)-f(y)|<\epsilon . \end{aligned}$$

On merely logical grounds we should be able to make the following conclusion:

$$\begin{aligned}&\textit{For every}\, x\, \textit{and every}\, \epsilon >0\, \textit{there is}\, \delta >0 \\&\textit{such that for all}\, y, \textit{if} \ |x-y|<\delta ,\,\textit{then} \,|f(x)-f(y)|<\epsilon ,\\&\textit{and moreover},\,\textit{for any other}\, x{^\prime }\,\textit{and}\, \epsilon {^\prime }>0\,\textit{there is}\, \delta {^\prime }>0 \\&\textit{such that for all}\, y{^\prime },\, \textit{if}\,|x{^\prime }-y{^\prime }|<\delta ^{\prime },\,\textit{then}\,|f(x^{\prime })-f(y^{\prime })|<\epsilon \\&\textit{and if}\, \epsilon =\epsilon ^{\prime },\,\textit{then} \ \delta =\delta ^{\prime }. \end{aligned}$$

The new rule, isolated in [24] which permits this step is called Dependence Elimination Rule, because the dependence atom “depending only on $\epsilon$” has been entirely eliminated. The conclusion is actually first order, that is, without any occurrence of dependence atoms.

The first author [11] has given an alternative complete axiomatization, not for first order consequences of dependence sentences, but for dependence logic consequences of first order sentences. Clearly, more results about partial axiomatizations of the logical consequence relation in dependence logic can be expected in the near future.

An important property of dependence logic is the downward closure [20]: If  $\mathfrak {M}\models _S\phi$ and $S{^\prime }\subseteq S$, then $\mathfrak {M}\models _{S{^\prime }}\phi$. It is a trivial matter to prove this by induction on the length of the formula. Once the downward closure is established it is obvious that we are far from having a negation in the sense of classical logic. Intuitively, dependence is a restriction of freedom (of values of variables in assignments). When the team gets smaller there is even less freedom. This intuition about the nature of dependence prevails in all the logical operations of dependence logic. Since dependence formulas are easily seen to be representable in existential second order logic, the following result shows that downward closure is really the essential feature of dependence logic:

Theorem 4.3

[23] Let us fix a vocabulary $L$ and an $n$-ary predicate symbol $S\notin L$. Then:

• For every $L$-formula $\phi (x_1,...,x_n)$ of dependence logic there is an existential second order $L\cup \{S\}$-sentence $\Phi (S)$, closed downward with respect to $S$, such that for all $L$-structures $M$ and all teams $X$:

  $$\begin{aligned} \mathfrak {M}\models _X\phi (x_1,\ldots ,x_n)\iff \mathfrak {M}\models \Phi (X). \end{aligned}$$

  (4.6)

• For every existential second order $L\cup \{S\}$-sentence $\Phi (S)$, closed downward with respect to $S$, there exists an $L$-formula $\phi (x_1,\ldots ,x_n)$ of dependence logic such that (4.6) holds for all $L$-structures $M$ and all teams $X\ne \emptyset$.

This shows that dependence logic is maximal with respect to the properties of being expressible in existential second order logic and being downward closed. This theorem is also the source of the main model theoretical properties of dependence logic. The Downward Löwenheim-Skolem Theorem, the Compactness Theorem and the Interpolation Theorem are immediate corollaries. Also, when the above theorem is combined with the Interpolation Theorem of first order logic, we get the fact that dependence logic sentences $\phi$ for which there exists a dependence logic sentence $\psi$ such that for all $\mathfrak {M}$

$$ \mathfrak {M}\models \psi \iff \mathfrak {M}\not \models \phi $$

are first order definable. So not only does dependence logic not have the classical negation, the only sentences that have a classical negation are the first order sentences.

3 Independence Logic

Independence logic was introduced in [15]. Before going into the details, let us look at the following precedent:

In [3] Johan van Benthem suggested, as an example of an “other kind of correlation” than functional dependence, the following dependence relation for a team $S$ in a model $\mathfrak {M}$:

$$\begin{aligned} \exists a\in M\exists b\in M(\{s(x):s\in S, s(y)=a\}\ne \{s(x):s\in S, s(y)=b\}). \end{aligned}$$

(4.7)

The opposite of this would be

$$\begin{aligned} \forall a\in M\forall b\in M(\{s(x):s\in S, s(y)=a\}=\{s(x):s\in S, s(y)=b\}), \end{aligned}$$

(4.8)

which is a kind of independence of $x$ from $y$, for if we take $s\in S$ and we are told what $s(y)$ is, we have learnt nothing about $s(x)$, because for each $a\in M$ the set

$$\{s(x):s\in S, s(y)=a\}$$

is the same. This is the idea behind the independence atom $\vec {x}\ \bot \ \vec {y}$: the values of $\vec {x}$ should not reveal anything about the values of $\vec {y}$ and vice versa. More exactly, suppose $\mathfrak {M}$ is a model and $S$ is a team of assignments into $M$. We define:

Definition 4.4

A team $S$ satisfies the atomic formula $\vec {x}\ \bot \ \vec {y}$ in $\mathfrak {M}$ if

$$\begin{aligned} \forall s,s{^\prime }\in S\exists s{^{\prime \prime }}\in S(s{^{\prime \prime }}(\vec {y})=s(\vec {y})\wedge s{^{\prime \prime }}(\vec {x})=s{^\prime }(\vec {x})). \end{aligned}$$

(4.9)

We can immediately observe that a constant variable is independent of every variable, including itself. To see this, suppose $x$ is constant in $S$. Let $y$ be any variable, possibly $y=x$. If $s,s{^\prime }\in S$ are given, we need $s{^{\prime \prime }}\in S$ such that $s{^{\prime \prime }}(x)=s(x)$ and $s{^{\prime \prime }}(y)=s{^\prime }(y)$. We can simply take $s{^{\prime \prime }}=s{^\prime }$. Now $s{^{\prime \prime }}(x)=s(x)$, because $x$ is constant in $S$. Of course, $s{^{\prime \prime }}(y)=s{^\prime }(y)$. Conversely, if $x$ is independent of every variable, it is clearly constant, for it would have to be independent of itself, too. So we have

$$=(\vec {x})\iff \vec {x}\ \bot \ \vec {x}.$$

We can also immediately observe the symmetry of independence, because criterion (4.9) is symmetrical in $x$ and $y$. More exactly, $s{^{\prime \prime }}(y)=s(y)\wedge s{^{\prime \prime }}(x)=s{^\prime }(x)$ and $s{^{\prime \prime }}(x)=s{^\prime }(x)\wedge s{^{\prime \prime }}(y)=s(y)$ are trivially equivalent.

Dependence atoms were governed by Armstrong’s Axioms. Independence atoms have their own axioms introduced in the context of random variables in [14]:

Definition 4.5

The following rules are the Independence Axioms

• 1. $\vec {x}\ \bot \ \emptyset$ (Empty Set Rule).

• 2. If $\vec {x}\ \bot \ \vec {y}$, then $\vec {y}\ \bot \ \vec {x}$ (Symmetry Rule).

• 3. If $\vec {x}\ \bot \ \vec {y}\vec {z}$, then $\vec {x}\ \bot \ \vec {y}$ (Weakening Rule).

• 4. If $\vec {x}\ \bot \ \vec {x}$, then $\vec {x}\ \bot \ \vec {y}$ (Constancy Rule).

• 5. If $\vec {x}\ \bot \ \vec {y}$ and $\vec {x}\vec {y}\ \bot \ \vec {z}$, then $\vec {x}\ \bot \ \vec {y}\vec {z}$ (Exchange Rule).

Note that $xy\ \bot \ xy$ is derivable from $x\ \bot \ x$ and $y\ \bot \ y$, by means of the Empty Set Rule, the Constancy Rule and the Exchange Rule.

It may seem that independence must have much more content than what these four axioms express, but they are actually complete in the following sense⁵:

Theorem 4.6

(Completeness of the Independence Axioms, [14]) If $T$ is a finite set of independence atoms of the form $\vec {u}\ \bot \ \vec {v}$ for various $\vec {u}$ and $\vec {v}$, then $\vec {y}\ \bot \ \vec {x}$ follows from $T$ according to the above rules if and only if every team that satisfies $T$ also satisfies $\vec {y}\ \bot \ \vec {x}$.

Proof

We adapt the proof of [14] into our framework. Suppose $\vec {x}\ \bot \ \vec {y}$ follows semantically from $\Sigma$ but does not follow by the above rules. W.l.o.g. $\Sigma$ is closed under the rules. We may assume that $\vec {x}$ and $\vec {y}$ are minimal, that is, if $\vec {x}{^\prime }\subseteq \vec {x}$ and $\vec {y}{^\prime }\subseteq \vec {y}$ and at least one containment is proper, then if $\vec {x}{^\prime }\ \bot \ \vec {y}{^\prime }$ follows from $\Sigma$ semantically, it also follows by the rules. It is easy to see that if $\Sigma \models u\ \bot \ u$, then $\Sigma \vdash u\ \bot \ u$.

Suppose $\vec {x}=(x_1,\ldots ,x_l)$ and $\vec {y}=(y_1,\ldots ,y_m)$. Let $\vec {z}=(z_1,\ldots ,z_k)$ be the remaining variables. W.l.o.g., $l\ge 1$ and $m\ge 1$, $x_1\ \bot \ x_1\notin \Sigma$, and $x_1\notin \{y_1,\ldots ,y_m\}$.

We construct a team $S$ in a 2-element model $M=\{0,1\}$ of the empty vocabulary as follows: We take to $S$ every $s:\vec {x}\vec {y}\vec {z}\rightarrow M$, which satisfies $s(u)=0$ for $u$ such that $u\ \bot \ u\in \Sigma$ and in addition

$$ s(x_1)\,=\, \text{ the } \text{ number } \text{ of } \text{ ones } \text{ in } \ s[\{x_2,\ldots ,x_l,y_1,\ldots ,y_m\}]\,\text{ mod } \text{2 } $$

Claim 1 $\vec {x}\ \bot \ \vec {y}$ is not true in $S$. Suppose otherwise. Consider the following two assignments in $S$:

If $s''$ is such that $s''(\vec {x})=s(\vec {x})$ and $s''(\vec {y})=s'(\vec {y})$, then $s''\notin S$. Claim 1 is proved.

Claim 2 $S$ satisfies all the independence atoms in $\Sigma$. Suppose $\vec {v}\ \bot \ \vec {w}\in S$. If either $\vec {v}$ or $\vec {w}$ contains only variables in $Z$, then the claim is trivial, as then either $\vec {v}$ or $\vec {w}$ has in $S$ all possible binary sequences. So let us assume that both $\vec {v}$ and $\vec {w}$ meet $\vec {x}\vec {y}$. If $\vec {v}\vec {w}$ does not cover all of $\vec {x}\vec {y}$, then $S$ satisfies $\vec {v}\ \bot \ \vec {w}$, because we can fix parity on the variable in $\vec {x}\vec {y}$ which does not occur in $\vec {v}\vec {w}$. So let us assume $\vec {v}\vec {w}$ covers all of $\vec {x}\vec {y}$. Thus $\vec {v}=\vec {x}{^\prime }\vec {y}{^\prime }\vec {z}{^\prime }$ and $\vec {w}=\vec {x}{^{\prime \prime }}\vec {y}{^{\prime \prime }}\vec {z}{^{\prime \prime }}$, where $\vec {x}{^\prime }\vec {x}{^{\prime \prime }}=\vec {x}$ and $\vec {y}{^\prime }\vec {y}{^{\prime \prime }}=\vec {y}$. W.l.o.g., $\vec {x}{^\prime }\ne \emptyset$ and $\vec {x}{^\prime }\vec {y}{^\prime }\ne \vec {x}\vec {y}$. By minimality $\vec {x}{^\prime }\ \bot \ \vec {y}{^\prime }\in \Sigma$ and $\vec {x}{^{\prime \prime }}\ \bot \ \vec {y}\in \Sigma$. Since $\vec {v}\ \bot \ \vec {w}\in \Sigma$, a couple of applications of the Exchange and Weakening Rules gives $\vec {x}{^\prime }\vec {y}{^\prime }\ \bot \ \vec {x}{^{\prime \prime }}\vec {y}{^{\prime \prime }}\in \Sigma$. But then $\vec {x}{^\prime }\vec {x}{^{\prime \prime }}\ \bot \ \vec {y}{^\prime }\vec {y}{^{\prime \prime }}\in \Sigma$, contrary to the assumption. $\square$

We can use the conditions (4.4) to extend the truth definition to the entire independence logic, i.e. the extension of first order logic by the independence atoms. Can we axiomatize logical consequence in independence logic? The answer is again no, and for the same reason as for dependence logic: Recall that the sentence (4.5) characterizes infinity and ruins any hope to have a completeness theorem for dependence logic. We can do the same using independence atoms:

Lemma 4.7

The sentence

$$\begin{aligned} \exists z\forall x\exists y\forall u\exists v(xy\ \bot \ uv\wedge (x=u\leftrightarrow y=v)\wedge \lnot v=z) \end{aligned}$$

(4.10)

is true exactly in infinite models.

The conclusion is that the kind of dependence relation needed for expressing infinity can be realized either by the functional dependence relation or by the independence relation. Another such example is parity in finite models. The following two sentences, the first one with a dependence atom and the second with an independence atom, both express the evenness of the size of a finite model:

$$ \forall x\exists y\forall u\exists v(=(u,v)\wedge (x=v\leftrightarrow y=u)\wedge \lnot x=y) $$

$$ \forall x\exists y\forall u\exists v(xy\ \bot \ uv\wedge (x=v\leftrightarrow y=u)\wedge \lnot x=y) $$

The fact that we could express, at will, both infinity and evenness by means of either dependence atoms or independence atoms, is not an accident. Dependence logic and independence logic have overall the same expressive power:

Theorem 4.8

The following are equivalent:  

(1) :

$K$ is definable by a sentence of the extension of first order logic by the dependence atoms.

(2) :

$K$ is definable by a sentence of the extension of first order logic by the independence atoms.

(3) :

$K$ is definable in existential second order logic.

 

Proof

The equivalence of (1) and (3), a consequence of results in [8] and [31], as observed in [20], is proved in [29]. So it suffices to show that (1) implies (2). We give only the main idea. Sentences referred to in (1) have a normal form [29]. Here is an example of a sentence in such a normal form

$$ \forall x\forall y\exists v\exists w(=(x,v)\wedge =(y,w)\wedge \phi (x,y,v,w)), $$

where $\phi (x,y,v,w)$ is a quantifier free first order formula. This sentence can be expressed in terms of independence atoms as follows:

$$ \forall x\forall y\exists v\exists w(xv\bot y\wedge yw\bot xv\wedge \phi (x,y,v,w)). $$

$\square$

Note that independence, as we have defined it, is not the negation of dependence. It is rather a very strong denial of dependence. However, there are uses of the concepts of dependence and independence where the negation of dependence is the same as independence. An example is vector spaces.

There is an earlier common use of the concept of independence in logic, namely the independence of a set $\Sigma$ of axioms from each other. This is usually taken to mean that no axiom is provable from the remaining ones. By Gödel’s Completeness Theorem this means the same as having for each axiom $\phi \in \Sigma$ a model of the remaining ones $\Sigma {\setminus }\{\phi \}$ in which $\phi$ is false. This is not so far from the independence concept $\vec {y}\ \bot \ \vec {x}$. Again, the idea is that from the truth of $\Sigma {\setminus }\{\phi \}$ we can say nothing about the truth-value of $\phi$. This is the sense in which Continuum Hypothesis (CH) is independent of ZFC. Knowing the ZFC axioms gives us no clue as to the truth or falsity of CH. In a sense, our independence atom $\vec {y}\ \bot \ \vec {x}$ is the familiar concept of independence transferred from the world of formulas to the world of elements of models, from truth values to variable values.

4 Conditional Independence

The independence atom $\vec {y}\ \bot \ \vec {x}$ turns out to be a special case of the more general atom $\vec {y}\ \bot _{\vec {x}}\ \vec {z}$, the intuitive meaning of which is that the variables $\vec {y}$ are totally independent of the variables $\vec {z}$ when the variables $\vec {x}$ are kept fixed (see [15]). Formally,

Definition 4.9

A team $S$ satisfies the atomic formula $\vec {y}\ \bot _{\vec {x}}\ \vec {z}$ in $\mathfrak {M}$ if

$$ \forall s,s{^\prime }\in S ( s(\vec {x}) = s{^\prime }(\vec {x}) \rightarrow \exists s{^{\prime \prime }}\in S(s{^{\prime \prime }}(\vec {x}\vec {y})=s(\vec {x}\vec {y})\wedge s{^{\prime \prime }}(\vec {z})=s{^\prime }(\vec {z}))). $$

Some of the rules that this “conditional” independence notion obeys are [Second Transitivity:] 

Reflexivity: :

${\vec {x}}~\bot _{\vec {x}}~{\vec {y}}$,

Symmetry: :

If ${\vec {y}}~\bot _{\vec {x}}~{\vec {z}}$, then ${\vec {z}}~\bot _{\vec {x}}~{\vec {y}}$,

Weakening: :

If ${\vec {y}y'}~\bot _{\vec {x}}~{\vec {z}z'}$, then ${\vec {y}}~\bot _{\vec {x}}~{\vec {z}}$,

First Transitivity: :

If ${\vec {x}}~\bot _{\vec {z}}~{\vec {y}}$ and ${\vec {u}}~\bot _{\vec {z}\vec {x}}~{\vec {y}}$, then ${\vec {u}}~\bot _{\vec {z}}~{\vec {y}}$,

Second Transitivity: :

If ${\vec {y}}~\bot _{\vec {z}}~{\vec {y}}$ and ${\vec {z}\vec {x}}~\bot _{\vec {y}}~{\vec {u}}$, then ${\vec {x}}~\bot _{\vec {z}}~{\vec {u}}$,

Exchange: :

If ${\vec {x}}~\bot _{\vec {z}}~{\vec {y}}$ and ${\vec {x}\vec {y}}~\bot _{\vec {z}}~{\vec {u}}$, then ${\vec {x}}~\bot _{\vec {z}}~{\vec {y}\vec {u}}$.

 

Are these axioms complete? More in general, is it possible to find a finite, decidable axiomatization for the consequence relation between conditional independence atoms?

The answer is negative. Indeed, in [16, 17] Hermann proved that the consequence relation between conditional independence atoms is undecidable; and as proved by Parker and Parsaye-Ghomi in [28], it is not possible to find a finite and complete axiomatization for these atoms. However, the consequence relation is recursively enumerable, and in [27] Naumov and Nicholls developed a proof system for it.

The logic obtained by adding conditional independence atoms to first order logic will be called in this paper conditional independence logic. It is clear that it contains (nonconditional) independence logic; and furthermore, as discussed in [15], it also contains dependence logic, since a dependence atom $=(\vec {x}, \vec {y})$ can be seen to be equivalent to ${\vec {y}}~\bot _{\vec {x}}~{\vec {y}}$. It is also easy to see that every conditional independence logic sentence is equivalent to some $\Sigma _1^1$ sentence, and therefore that conditional independence logic is equivalent to independence logic and dependence logic with respect to sentences.

But this leaves open the question of whether every conditional independence logic formula is equivalent to some independence logic one. In what follows, building on the analysis of the expressive power of conditional independence logic of [10],⁶ we prove that independence logic and conditional independence logic are indeed equivalent.

In order to give our equivalence proof we first need to mention two other atoms, the inclusion atom $\vec {x}\subseteq \vec {y}$ and the exclusion atom $\vec {x}~|~ \vec {y}$. These atoms correspond to the database-theoretic inclusion [4, 9] and exclusion [5] dependencies, and hold in a team if and only if no possible value for $\vec {x}$ is also a possible value for $\vec {y}$ and if every possible value for $\vec {x}$ is a possible value for $\vec {y}$ respectively. More formally,

Definition 4.10

A team $S$ satisfies the atomic formula $\vec {x}\subseteq \vec {y}$ in $\mathfrak {M}$ if

$$ \forall s\in S \exists s{^\prime }\in S(s{^\prime }(\vec {y})=s(\vec {x})) $$

and it satisfies the atomic formula $\vec {x}~|~ \vec {y}$ in $\mathfrak {M}$ if

$$ \forall s, s{^\prime }\in S(s(\vec {x}) \not = s{^\prime }(\vec {y})). $$

As proved in [10],

• 1. Exclusion logic (that is, first order logic plus exclusion atoms) is equivalent to dependence logic;

• 2. Inclusion logic (that is, first order logic plus inclusion atoms) is not comparable with dependence logic, but is contained in (nonconditional) independence logic;

• 3. Inclusion/exclusion logic (that is, first-order logic plus inclusion and exclusion atoms) is equivalent to conditional independence logic (that is, first-order logic plus conditional independence atoms ${\vec {y}}~\bot _{\vec {x}}~{\vec {z}}$).

Thus, if we can show that exclusion atoms can be defined in terms of (nonconditional) independence atoms and of inclusion atoms, we can obtain at once that independence logic contains conditional independence logic (and, therefore, is equivalent to it). But this is not difficult: indeed, the exclusion atom $\vec {x}~|~ \vec {y}$ is equivalent to the expression

$$ \exists \vec {z}(\vec {x}\subseteq \vec {z}\wedge \vec {y}\ \bot \ \vec {z}\wedge \vec {y}\not = \vec {z}). $$

This can be verified by checking the satisfaction conditions of this formula. But more informally speaking, the reason why this expression is equivalent to $\vec {x}~|~ \vec {y}$ is that it states that that every possible value of $\vec {x}$ is also a possible value for $\vec {z}$, that $\vec {y}$ and $\vec {z}$ are independent (and therefore, any possible value of $\vec {y}$ must occur together with any possible value of $\vec {z}$), and that $\vec {y}$ is always different from $\vec {z}$. Such a $\vec {z}$ may exist if and only if no possible value of $\vec {x}$ is also a possible value of $\vec {y}$, that is, if and only if $\vec {x}~|~ \vec {y}$ holds.

Hence we may conclude at once that

Theorem 4.11

Every conditional independence logic formula is equivalent to some independence logic formula.

In [10] it was also shown the following analogue of Theorem 4.3:

Theorem 4.12

Let us fix a vocabulary $L$ and an $n$-ary predicate symbol $S\notin L$. Then:

• For every $L$-formula $\phi (x_1,\ldots ,x_n)$ of conditional independence logic there is an existential second order $L\cup \{S\}$-sentence $\Phi (S)$ such that for all $L$-structures $M$ and all teams $X$:

  $$\begin{aligned} \mathfrak {M}\models _X\phi (x_1,\ldots ,x_n)\iff \mathfrak {M}\models \Phi (X). \end{aligned}$$

  (4.11)

• For every existential second order $L\cup \{S\}$-sentence $\Phi (S)$ there exists an $L$-formula $\phi (x_1,\ldots ,x_n)$ of conditional independence logic such that (4.11) holds for all $L$-structures $M$ and all teams $X\ne \emptyset$.

Due to the equivalence between independence logic and conditional independence logic, the same result holds if we only allow nonconditional independence atoms. In particular, this implies that over finite models independence logic captures precisely the NP properties of teams.

5 Further Expressivity Results

The results mentioned in the above section left open the question of the precise expressive power of inclusion logic. This was answered in [14], in which a connection was found between inclusion logic and positive greatest fixed point logic GFP$^+$. In brief, GFP$^+$ is the logic obtained by adding to the language of first order logic the operator

$$ [\text{ gfp }_{R, \vec {x}}\psi (R, \vec {x})](\vec t), $$

which asserts that the value of $\vec t$  is in the greatest fixed point of the operator $O(R) = \{\vec a : \psi (R, \vec a)\}$,⁷ and further requiring that no such operator occurs negatively.

Over finite models, it is known by [21] that this logic is equivalent to the better-known least fixed point logic LFP, which captures PTIME over linearly ordered models [21, 30]. Thus, the same is true of inclusion logic: more precisely,

Theorem 4.13

A class of linearly ordered finite models is definable in inclusion logic if and only if it can be recognized in polynomial time.

As dependence logic is equivalent to existential second order logic over sentences, it follows at once that there exists a fragment of dependence logic which also captures PTIME. Which fragment may it be? This is answered—in a slightly different setting—by Ebbing, Kontinen, Müller and Vollmer in [7] by introducing the class of D $^*$ -Horn formulas and proving that they capture PTIME over successor structures.⁸

The complexity-theoretic properties of further fragments of these logics have been studied in the papers [6] and [13], in which hierarchy theorems are developed for the restrictions of these logics to dependencies of certain maximum lengths or to maximum numbers of quantifiers. We will not however present here a complete summary of these results, and we refer the interested readers to these papers for the details.

Finally, yet another direction of investigation consists in the search for weak dependency notions, which if added to the language of first order logic do not increase its expressive power (with respect to sentences). This problem in studied in [12], in which a fairly general class of such dependencies is found. One particularly interesting result along these lines is that the contradictory negations of functional dependence, inclusion, exclusion and (conditional or non-conditional) independence atoms are all weak and do not increase the expressive power of first order logic. This is somewhat surprising, since as we saw the corresponding non-negated atoms greatly increase the expressivity of first order logic instead; and the study of the manner in which applying the contradictory negation acts on dependence notions and on the logics they generate is an intriguing and largely unexplored avenue of research.

6 Belief Representation and Belief Dynamics

Given a model $\mathfrak {M}$, a variable assignment $s$ admits a natural interpretation as the representation of a possible state of things, where, for every variable $v$, the value $s(v)$ corresponds to a specific fact concerning the world. To use the example discussed in Chap. 7 of [11], let the elements of $\mathfrak {M}$ correspond to the participants to a competition: then the values of the variables $x_1$, $x_2$ and $x_3$ in an assignment $s$ may correspond respectively to the first-, second- and the third-placed players.

With respect to the usual semantics for first order logic, a first order formula represents a condition over assignments. For example, the formula

$$ \phi (x_1, x_2, x_3) := (\lnot x_1 = x_2) \wedge (\lnot x_2 = x_3) \wedge (\lnot x_1 = x_3) $$

represents the (very reasonable) assertion according to which the winner, the second-placed player and the third-placed player are all distinct.

Now, a team $S$, being a set of assignments, represents a set of states of things. Hence, a team may be interpreted as the belief set of an agent $\alpha$: $s \in S$ if and only if the agent $\alpha$ believes $s$ to be possible. Moving from assignments to teams, it is possible to associate to each formula $\phi$ and model $\mathfrak {M}$ the family of teams $\{ S : \mathfrak {M}\models _S \phi \}$, and this allows us to interpret formulas as conditions over belief sets: in our example, $\mathfrak {M}\models _S \phi (x_1, x_2, x_3)$ if and only if $\mathfrak {M}\models _s \phi (x_1, x_2, x_3)$ for all $s \in S$, that is, if and only if our agent $\alpha$ believes that the winner, the second-placed player and the third-placed player will all be distinct.

However, there is much that first order logic cannot express regarding the beliefs of our agent. For example, there is no way to represent the assertion that the agent $\alpha$ knows who the winner of the competition will be: indeed, suppose that a first order formula $\theta$ represents such a property, and let $s_1$ and $s_2$ be any two assignments with $s_1(x_1) \not = s_2(x_1)$, corresponding to two possible states of things which disagree with respect to the identity of the winner. Then, for $S_1 = \{s_1\}$ and $S_2 = \{s_2\}$, we should have that $\mathfrak {M}\models _{S_1} \theta$ and that $\mathfrak {M}\models _{S_2} \theta$: indeed, both $S_1$ and $S_2$ correspond to belief sets in which the winner is known to $\alpha$ (and is respectively $s_1(x_1)$ or $s_2(x_1)$). But since a team $S$ satisfies a first order formula if and only if all of its assignments satisfy it, this implies that $M \models _{S_1 \cup S_2} \theta$; and this is unacceptable, because if our agent $\alpha$ believes both $s_1$ and $s_2$ to be possible then she does not know whether the winner will be $s_1(x_1)$ or $s_2(x_1)$.

How to represent this notion of knowledge? The solution, it is easy to see, consists in adding constancy atoms to our language: indeed, ${\mathfrak {M}\models _S} =(x_1)$ if and only if for any two assignments $s, s{^\prime } \in S$ we have that $s(x_1) = s{^\prime }(x_1)$, that is, if and only if all states of things the agent $\alpha$ consider possible agree with respect to the identity of the winner of the competition. What if, instead, our agent could infer the identity of the winner from the identity of the second- and third-placed participants? Then we would have that ${\mathfrak {M}\models _S} =(x_2 x_3, x_1)$, since any two states of things which the agent considered possible and which agreed with respect to the identity of the second- and third-placed participants would also agree with respect to the identity of the winner. More in general, a dependence atom $=(\vec {y}, \vec {x})$ describes a form of conditional knowledge: ${\mathfrak {M}\models _S} =(\vec {y}, \vec {x})$ if and only if $S$ corresponds to the belief state of an agent who would be able to deduce the value of $\vec {x}$ from the value of $\vec {y}$.

On the other hand, independence atoms represent situations of informational independence: for example, if $\mathfrak {M}\models _S x_1 \ \bot \ x_3$ then, by learning the identity of the third-placed player, our agent could infer nothing at all about the identity of the winner. Indeed, suppose that, according to our agent, it is possible that $A$ will win (that is, there is a $s \in S$ with $s(x_1) = A$) and it is possible that $B$ will place third (that is, there is a $s{^\prime } \in S$ such that $s{^\prime }(x_3) = B$). Then, by the satisfaction conditions of the independence atom, there is also a $s{^{\prime \prime }} \in S$ such that $s{^{\prime \prime }}(x_1) = A$ and $s{^{\prime \prime }}(x_3) = B$: in other words, it is possible that $A$ will be the winner and $B$ will place third, and telling our agent that $B$ will indeed place third will not allow her to remove $A$ from her list of possible winners.

Thus, it seems that dependence and independence logic, or at least fragments thereof, may be interpreted as belief description languages. This line of investigation is pursued further in [11]: here it will suffice to discuss the interpretation of the linear implication ⁹ $\phi \multimap \psi$, a connective introduced in [1] whose semantics is given by

$$ \mathfrak {M}\models _S \phi \multimap \psi \Leftrightarrow \text{ for } \text{ all } S{^{\prime }} \text{ such } \text{ that } \mathfrak {M}\models _{S{^{\prime }}} \phi \text{ it } \text{ holds } \text{ that } \mathfrak {M}\models _{S \cup S{^{\prime }}} \psi . $$

How to understand this connective? Suppose that our agent $\alpha$, whose belief state is represented by the team $S$, interacts with another agent $\beta$, whose belief state is represented by the team $S{^\prime }$: one natural outcome of this interaction may be represented by the team $S \cup S{^{\prime }}$, corresponding to the set of all states of things that $\alpha$ or $\beta$ consider possible. Then stating that a team $S$ satisfies $\phi \multimap \psi$ corresponds to asserting that whenever our agent $\alpha$ interacts with another agent $\beta$ whose belief state satisfies $\phi$, the result of the interaction will be a belief state satisfying $\psi$: in other words, using the linear implication connective allows us to formulate predictions concerning the future evolution of the belief state of our agent.

One can, of course, consider other forms of interactions between agents and further connectives; and quantifiers can also be given natural interpretations in terms of belief updates (the universal quantifier $\forall v$, for example, can be understood in terms of the agent $\alpha$ doubting her beliefs about $v$). But what we want to emphasize here, beyond the interpretations of the specific connectives, is that team-based semantics offers a very general and powerful framework for the representation of beliefs and belief updates, and that notions of dependence and independence arise naturally under such an interpretation. This opens up some fascinating—and, so far, relatively unexplored—avenues of research, such as for example a more in-depth investigation of the relationship between dependence/independence logic and dynamic epistemic logic (DEL) and other logics of knowledge and belief; and, furthermore, it suggests that epistemic and doxastic ideas may offer some useful inspiration for the formulation and analysis of further notions of dependence and independence.

7 Concluding Remarks

We hope to have demonstrated that both dependence and independence can be given a logical analysis by moving in semantics from single states $s$ to plural states $S$. Future work will perhaps show that allowing limited transitions from one plural state to another may lead to decidability results concerning dependence and independence logic, a suggestion of Johan van Benthem.

Furthermore, we proved the equivalence between conditional independence logic and independence logic, thus giving a novel contribution to the problem of characterizing the relations between extensions of dependence logic.

Finally, we discussed how team-based semantics may be understood as a very general framework for the representation of beliefs and belief updates and how notions of dependence and independence may be understood under this interpretation. This suggests the existence of intriguing connections between dependence and independence logic and other formalisms for belief knowledge representation, as well as a possible application for this fascinating family of logics.