Dependence logic

The syntax of dependence logic is an extension of that of first-order logic. For a fixed signature σ = (S_func, S_rel, ar), the set of all well-formed dependence logic formulas is defined according to the following rules:

Terms in dependence logic are defined precisely as in first-order logic.

There are three types of atomic formulas in dependence logic:

1. A relational atom is an expression of the form $Rt\_1\; \backslash ldots\; t\_n$ for any n-ary relation $R$ in our signature and for any n-tuple of terms $(t\_1,\; \backslash ldots,\; t\_n)$;
2. An equality atom is an expression of the form $t\_1\; =\; t\_2$, for any two terms $t\_1$ and $t\_2$;
3. A dependence atom is an expression of the form $=\backslash !\backslash !(t\_1\; \backslash ldots\; t\_n)$, for any $n\; \backslash in\; \backslash mathbb\; N$ and for any n-tuple of terms $(t\_1,\; \backslash ldots,\; t\_n)$.

Nothing else is an atomic formula of dependence logic.

Relational and equality atoms are also called first-order atoms.

For a fixed signature σ, the set of all formulas $\backslash phi$ of dependence logic and their respective sets of free variables $\backslash mbox\{Free\}(\backslash phi)$ are defined as follows:

1. Any atomic formula $\backslash phi$ is a formula, and $\backslash mbox\{Free\}(\backslash phi)$ is the set of all variables occurring in it;
2. If $\backslash phi$ is a formula, so is $\backslash lnot\; \backslash phi$ and $\backslash mbox\{Free\}(\backslash lnot\backslash phi)\; =\; \backslash mbox\{Free\}(\backslash phi)$;
3. If $\backslash phi$ and $\backslash psi$ are formulas, so is $\backslash phi\; \backslash vee\; \backslash psi$ and $\backslash mbox\{Free\}(\backslash phi\; \backslash vee\; \backslash psi)\; =\; \backslash mbox\{Free\}(\backslash phi)\; \backslash cup\; \backslash mbox\{Free\}(\backslash psi)$;
4. If $\backslash phi$ is a formula and $x$ is a variable, $\backslash exists\; x\; \backslash phi$ is also a formula and $\backslash mbox\{Free\}(\backslash exists\; v\; \backslash phi)\; =\; \backslash mbox\{Free\}(\backslash phi)\; \backslash backslash\; \backslash \{v\backslash \}$.

Nothing is a dependence logic formula unless it can be obtained through a finite number of applications of these four rules.

A formula $\backslash phi$ such that $\backslash mbox\{Free\}(\backslash phi)\; =\; \backslash emptyset$ is a sentence of dependence logic.

In the above presentation of the syntax of dependence logic, conjunction and universal quantification are not treated as primitive operators; rather, they are defined in terms of negation and, respectively, disjunction and existential quantification, by means of De Morgan's Laws.

Therefore, $\backslash phi\; \backslash wedge\; \backslash psi$ is taken as a shorthand for $\backslash lnot\; (\backslash lnot\; \backslash phi\; \backslash vee\; \backslash lnot\; \backslash psi)$, and $\backslash forall\; x\; \backslash phi$ is taken as a shorthand for $\backslash lnot(\backslash exists\; x\; (\backslash lnot\; \backslash phi))$.

The team semantics for dependence logic is a variant of Wilfrid Hodges' compositional semantics for IF logic.Hodges 1997Väänänen 2007, §3.2 There exist equivalent game-theoretic semantics for dependence logic, both in terms of imperfect information games and in terms of perfect information games.

Let $\backslash mathcal\; A\; =\; (A,\; \backslash sigma,\; I)$ be a first-order structure and let $V\; =\; \backslash \{v\_1,\; \backslash ldots,\; v\_n\backslash \}$ be a finite set of variables. Then a team over {{mathcal|A}} with domain {{mvar|V}} is a set of assignments over {{mathcal|A}} with domain {{mvar|V}}, that is, a set of functions {{mvar|μ}} from {{mvar|V}} to {{mvar|A}}.

It may be helpful to visualize such a team as a database relation with attributes $v\_1,\; \backslash ldots,\; v\_n$ and with only one data type, corresponding to the domain {{mvar|A}} of the structure: for example, if the team {{mvar|X}} consists of four assignments $\backslash mu\_1,\; \backslash ldots,\; \backslash mu\_4$ with domain $\backslash \{v\_1,\; v\_2,\; v\_3\backslash \}$ then one may represent it as the relation

:$\backslash begin\{array\}\{c|ccc\}$

& v_1

& v_2

& v_3

\\

\hline

\mu_1 &

\mu_1(v_1) & \mu_1(v_2) & \mu_1(v_3)

\\

\mu_2 &

\mu_2(v_1) & \mu_2(v_2) & \mu_2(v_3)

\\

\mu_3 &

\mu_3(v_1) & \mu_3(v_2) & \mu_3(v_3)

\\

\mu_4 &

\mu_4(v_1) & \mu_4(v_2) & \mu_4(v_3)

\end{array}

Team semantics can be defined in terms of two relations $\backslash mathcal\; T$ and $\backslash mathcal\; C$ between structures, teams and formulas.

Given a structure $\backslash mathcal\; A$, a team $X$ over it and a dependence logic formula $\backslash phi$ whose free variables are contained in the domain of $X$, if $(\backslash mathcal\; A,\; X,\; \backslash phi)\; \backslash in\; \backslash mathcal\; T$ we say that $X$ is a trump for $\backslash phi$ in $\backslash mathcal\; A$, and we write that $\backslash mathcal\; A\; \backslash models\_X^+\; \backslash phi$; and analogously, if $(\backslash mathcal\; A,\; X,\; \backslash phi)\; \backslash in\; \backslash mathcal\; C$ we say that $X$ is a cotrump for $\backslash phi$ in $\backslash mathcal\; A$, and we write that $\backslash mathcal\; A\; \backslash models\_X^-\; \backslash phi$.

If $\backslash mathcal\; A\; \backslash models\_X^+\; \backslash phi$ one can also say that $\backslash phi$ is positively satisfied by $X$ in $\backslash mathcal\; A$, and if instead $\backslash mathcal\; A\; \backslash models\_X^-\; \backslash phi$ one can say that $\backslash phi$ is negatively satisfied by $X$ in $\backslash mathcal\; A$.

The necessity of considering positive and negative satisfaction separately is a consequence of the fact that in dependence logic, as in the logic of branching quantifiers or in IF logic, the law of the excluded middle does not hold; alternatively, one may assume that all formulas are in negation normal form, using De Morgan's relations in order to define universal quantification and conjunction from existential quantification and disjunction respectively, and consider positive satisfaction alone.

Given a sentence $\backslash phi$, we say that $\backslash phi$ is true in $\backslash mathcal\; A$ if and only if $\backslash mathcal\; A\; \backslash models\_\{\backslash \{\backslash emptyset\backslash \}\}^+\; \backslash phi$, and we say that $\backslash phi$ is false in $\backslash mathcal\; A$ if and only if $\backslash mathcal\; A\; \backslash models\_\{\backslash \{\backslash emptyset\backslash \}\}^-\; \backslash phi$.

As for the case of Alfred Tarski's satisfiability relation for first-order formulas, the positive and negative satisfiability relations of the team semantics for dependence logic are defined by structural induction over the formulas of the language. Since the negation operator interchanges positive and negative satisfiability, the two inductions corresponding to $\backslash models^+$ and $\backslash models^-$ need to be performed simultaneously:

1. $\backslash mathcal\; A\; \backslash models\_X^+\; R\; t\_1\; \backslash ldots\; t\_n$ if and only if
2. $R$ is a n-ary symbol in the signature of $\backslash mathcal\; A$;
3. All variables occurring in the terms $t\_1,\; \backslash ldots,\; t\_n$ are in the domain of $X$;
4. For every assignment $\backslash mu\; \backslash in\; X$, the evaluation of the tuple $(t\_1,\; \backslash ldots,\; t\_n)$ according to $\backslash mu$ is in the interpretation of $R$ in $\backslash mathcal\; A$;
5. $\backslash mathcal\; A\; \backslash models\_X^+\; t\_1\; =\; t\_2$ if and only if
6. All variables occurring in the terms $t\_1$ and $t\_2$ are in the domain of $X$;
7. For every assignment $\backslash mu\; \backslash in\; X$, the evaluations of $t\_1$ and $t\_2$ according to $\backslash mathcal\; A$ are the same;
8. $\backslash mathcal\; A\; \backslash models\_X^+\; =\backslash !\backslash !(t\_1\; \backslash ldots\; t\_n)$ if and only if any two assignments $\backslash mu,\; \backslash mu\text{'}\; \backslash in\; X$ whose evaluations of the tuple $(t\_1,\; \backslash ldots,\; t\_\{n-1\})$ coincide assign the same value to $t\_n$;
9. $\backslash mathcal\; A\; \backslash models\_X^+\; \backslash lnot\; \backslash phi$ if and only if $\backslash mathcal\; A\; \backslash models\_X^-\; \backslash phi$;
10. $\backslash mathcal\; A\; \backslash models\_X^+\; \backslash phi\; \backslash vee\; \backslash psi$ if and only if there exist teams $Y$ and $Z$ such that
11. $X\; =\; Y\; \backslash cup\; Z\text{'}$
12. $\backslash mathcal\; A\; \backslash models\_Y^+\; \backslash phi$;
13. $\backslash mathcal\; A\; \backslash models\_Z^+\; \backslash psi$;
14. $\backslash mathcal\; A\; \backslash models\_X^+\; \backslash exists\; x\; \backslash phi$ if and only if there exists a function $F$ from $X$ to the domain of $\backslash mathcal\; A$ such that $\backslash mathcal\; A\; \backslash models\_\{X[F/x]\}^+\; \backslash phi$, where $X[F/x]\; =\; \backslash \{\; \backslash mu[F(\backslash mu)/x]\; :\; \backslash mu\; \backslash in\; X\backslash \}$.

1. $\backslash mathcal\; A\; \backslash models\_X^-\; R\; t\_1\; \backslash ldots\; t\_n$ if and only if
2. $R$ is a n-ary symbol in the signature of $\backslash mathcal\; A$;
3. All variables occurring in the terms $t\_1,\; \backslash ldots,\; t\_n$ are in the domain of $X$;
4. For every assignment $\backslash mu\; \backslash in\; X$, the evaluation of the tuple $(t\_1,\; \backslash ldots,\; t\_n)$ according to $\backslash mu$ is not in the interpretation of $R$ in $\backslash mathcal\; A$;
5. $\backslash mathcal\; A\; \backslash models\_X^-\; t\_1\; =\; t\_2$ if and only if
6. All variables occurring in the terms $t\_1$ and $t\_2$ are in the domain of $X$;
7. For every assignment $\backslash mu\; \backslash in\; X$, the evaluations of $t\_1$ and $t\_2$ according to $\backslash mathcal\; A$ are different;
8. $\backslash mathcal\; A\; \backslash models\_X^-\; =\backslash !\backslash !(t\_1\; \backslash ldots\; t\_n)$ if and only if $X$ is the empty team;
9. $\backslash mathcal\; A\; \backslash models\_X^-\; \backslash lnot\; \backslash phi$ if and only if $\backslash mathcal\; A\; \backslash models\_X^+\; \backslash phi$;
10. $\backslash mathcal\; A\; \backslash models\_X^-\; \backslash phi\; \backslash vee\; \backslash psi$ if and only if $\backslash mathcal\; A\; \backslash models\_X^-\; \backslash phi$ and $\backslash mathcal\; A\; \backslash models\_X^-\; \backslash psi$;
11. $\backslash mathcal\; A\; \backslash models\_X^-\; \backslash exists\; x\; \backslash phi$ if and only if $\backslash mathcal\; A\; \backslash models\_\{X[A/x]\}^-\; \backslash phi$, where $X[A/x]\; =\; \backslash \{\; \backslash mu[a/x]\; :\; a\; \backslash in\; A\backslash \}$ and $A$ is the domain of $\backslash mathcal\; A$.

Dependence logic is a conservative extension of first-order logic:Väänänen 2007, §3.2 in other words, for every first-order sentence $\backslash phi$ and structure $\backslash mathcal\; A$ we have that $\backslash mathcal\; A\; \backslash models\_\{\backslash \{\backslash emptyset\backslash \}\}^+\; \backslash phi$ if and only if $\backslash phi$ is true in $\backslash mathcal\; A$ according to the usual first-order semantics. Furthermore, for any first-order formula $\backslash phi$, $\backslash mathcal\; A\; \backslash models\_\{X\}^+\; \backslash phi$ if and only if all assignments $\backslash mu\; \backslash in\; X$ satisfy $\backslash phi$ in $\backslash mathcal\; A$ according to the usual first-order semantics.

However, dependence logic is strictly more expressive than first-order logic:Väänänen 2007, §4 for example, the sentence

:$\backslash exists\; z\; \backslash forall\; x\_1\; \backslash forall\; x\_2\; \backslash exists\; y\_1\; \backslash exists\; y\_2\; (=\backslash !\backslash !(x\_1,\; y\_1)\; \backslash wedge\; =\backslash !\backslash !(x\_2,\; y\_2)\; \backslash wedge\; (x\_1\; =\; x\_2\; \backslash leftrightarrow\; y\_1\; =\; y\_2)\; \backslash wedge\; y\_1\; \backslash not\; =\; z)$

is true in a model $\backslash mathcal\; A$ if and only if the domain of this model is infinite, even though no first-order formula $\backslash phi$ has this property.

Every dependence logic sentence is equivalent to some sentence in the existential fragment of second-order logic,Väänänen 2007, §6.1 that is, to some second-order sentence of the form

:$\backslash exists\; R\_1\; \backslash ldots\; \backslash exists\; R\_n\; \backslash psi(R\_1,\; \backslash ldots,\; R\_n)$

where $\backslash psi(R\_1,\; \backslash ldots,\; R\_n)$ does not contain second-order quantifiers.

Conversely, every second-order sentence in the above form is equivalent to some dependence logic sentence.Väänänen 2007, §6.3

As for open formulas, dependence logic corresponds to the downwards monotone fragment of existential second-order logic, in the sense that a nonempty class of teams is definable by a dependence logic formula if and only if the corresponding class of relations is downwards monotone and definable by an existential second-order formula.Kontinen and Väänänen 2009

Branching quantifiers are expressible in terms of dependence atoms: for example, the expression

: $(Q\_Hx\_1,x\_2,y\_1,y\_2)\backslash phi(x\_1,x\_2,y\_1,y\_2)\backslash equiv\backslash begin\{pmatrix\}\backslash forall\; x\_1\; \backslash exists\; y\_1\backslash \backslash \; \backslash forall\; x\_2\; \backslash exists\; y\_2\backslash end\{pmatrix\}\backslash phi(x\_1,x\_2,y\_1,y\_2)$

is equivalent to the dependence logic sentence $\backslash forall\; x\_1\; \backslash exists\; y\_1\; \backslash forall\; x\_2\; \backslash exists\; y\_2\; (=\backslash !\backslash !(x\_1,\; y\_1)\; \backslash wedge\; =\backslash !\backslash !(x\_2,\; y\_2)\; \backslash wedge\; \backslash phi)$, in the sense that the former expression is true in a model if and only if the latter expression is true.

Conversely, any dependence logic sentence is equivalent to some sentence in the logic of branching quantifiers, since all existential second-order sentences are expressible in branching quantifier logic.Enderton 1970Walkoe 1970

Any dependence logic sentence is logically equivalent to some IF logic sentence, and vice versa.Väänänen 2007, §3.6

However, the issue is subtler when it comes to open formulas. Translations between IF logic and dependence logic formulas, and vice versa, exist as long as the domain of the team is fixed: in other words, for all sets of variables $V\; =\; \backslash \{v\_1\; \backslash ldots\; v\_n\backslash \}$ and all IF logic formulas $\backslash phi$ with free variables in $V$ there exists a dependence logic formula $\backslash phi^D$ such that

:$\backslash mathcal\; A\; \backslash models\_X^+\; \backslash phi\; \backslash Leftrightarrow\; \backslash mathcal\; A\; \backslash models\_X^+\; \backslash phi^D$

for all structures $\backslash mathcal\; A$ and for all teams $X$ with domain $V$, and conversely, for every dependence logic formula $\backslash psi$ with free variables in $V$ there exists an IF logic formula $\backslash psi^I$ such that

:$\backslash mathcal\; A\; \backslash models\_X^+\; \backslash psi\; \backslash Leftrightarrow\; \backslash mathcal\; A\; \backslash models\_X^+\; \backslash psi^I$

for all structures $\backslash mathcal\; A$ and for all teams $X$ with domain $V$. These translations cannot be compositional.Kontinen and Väänänen 2009 bis

Dependence logic formulas are downwards closed: if $\backslash mathcal\; A\; \backslash models\_X\; \backslash phi$ and $Y\; \backslash subseteq\; X$ then $\backslash mathcal\; A\; \backslash models\_Y\; \backslash psi$. Furthermore, the empty team (but not the team containing the empty assignment) satisfies all formulas of dependence logic, both positively and negatively.

The law of the excluded middle fails in dependence logic: for example, the formula $\backslash exists\; y\; (=\backslash !\backslash !(y)\; \backslash wedge\; y\; =\; x)$ is neither positively nor negatively satisfied by the team $X\; =\; \backslash \{(x:0),\; (x:1)\backslash \}$. Furthermore, disjunction is not idempotent and does not distribute over conjunction.Väänänen 2007, §3

Both the compactness theorem and the Löwenheim–Skolem theorem are true for dependence logic. Craig's interpolation theorem also holds, but, due to the nature of negation in dependence logic, in a slightly modified formulation: if two dependence logic formulas $\backslash phi$ and $\backslash psi$ are contradictory, that is, it is never the case that both $\backslash phi$ and $\backslash psi$ hold in the same model, then there exists a first-order sentence $\backslash theta$ in the common language of the two sentences such that $\backslash phi$ implies $\backslash theta$ and $\backslash theta$ is contradictory with $\backslash psi$.Väänänen 2007, §6.2

As for IF logic,Hintikka 2002 dependence logic can define its own truth operator:Väänänen 2007, §6.4 more precisely, there exists a formula $\backslash tau(x)$ such that for every sentence $\backslash phi$ of dependence logic and all models $\backslash mathcal\; M\_\backslash omega$ which satisfy Peano's axioms, if $\text{'}\backslash phi\text{'}$ is the Gödel number of $\backslash phi$ then

: $\backslash mathcal\; M\_\backslash omega\; \backslash models^+\_\{\backslash \{\backslash emptyset\backslash \}\}\; \backslash !\backslash phi$ if and only if $\backslash mathcal\; M\_\backslash omega\; \backslash models^+\_\{\backslash \{\backslash emptyset\backslash \}\}\; \backslash tau(\text{'}\backslash phi\text{'}).$

This does not contradict Tarski's undefinability theorem, since the negation of dependence logic is not the usual contradictory one.

As a consequence of Fagin's theorem, the properties of finite structures definable by a

dependence logic sentence correspond exactly to NP properties. Furthermore, Durand and Kontinen showed that restricting the number of universal quantifiers or the arity of dependence atoms in

sentences gives rise to hierarchy theorems with respect to expressive power.Durand and Kontinen

The inconsistency problem of dependence logic is semidecidable, and in fact equivalent to the inconsistency problem for first-order logic.

However, the decision problem for dependence logic is non-arithmetical, and is in fact complete with respect to the $\backslash Pi\_2$ class of the Lévy hierarchy.Väänänen 2007, §7

Team logicVäänänen 2007, §8 extends dependence logic with a contradictory negation $\backslash sim\backslash !\backslash !\backslash phi$. Its expressive power is equivalent to that of full second-order logic.Kontinen and Nurmi 2009

The dependence atom, or a suitable variant thereof, can be added to the language of modal logic, thus obtaining modal dependence logic.Sevenster 2009Väänänen 2008Lohmann and Vollmer 2010

As it is, dependence logic lacks an implication. The intuitionistic implication $\backslash phi\; \backslash rightarrow\; \backslash psi$, whose name derives from the similarity between its definition and that of the implication of intuitionistic logic, can be defined as follows:Abramsky and Väänänen 2009

: $\backslash mathcal\; A\; \backslash models\_X\; \backslash phi\; \backslash rightarrow\; \backslash psi$ if and only if for all $Y\; \backslash subseteq\; X$ such that $\backslash mathcal\; A\; \backslash models\_Y\; \backslash phi$ it holds that $\backslash mathcal\; A\; \backslash models\_Y\; \backslash psi$.

Intuitionistic dependence logic, that is, dependence logic supplemented with the intuitionistic implication, is equivalent to second-order logic.Yang 2010

Instead of dependence atoms, independence logic adds to the language of first-order logic independence atoms $\backslash vec\{t\_1\}\backslash bot\_\{\backslash vec\{t\_3\}\}\; \backslash vec\{t\_2\}$ where $\backslash vec\{t\_1\}$, $\backslash vec\{t\_2\}$ and $\backslash vec\{t\_3\}$ are tuples of terms. The semantics of these atoms is defined as follows:

: $\backslash mathcal\; A\; \backslash models\_X\; \backslash vec\{t\_1\}\backslash bot\_\{\backslash vec\{t\_3\}\}\; \backslash vec\{t\_2\}$ if and only if for all $s,s\text{'}\; \backslash in\; X$ with $\backslash vec\{t\_3\}\backslash langle\; s\backslash rangle=\backslash vec\{t\_3\}\backslash langle\; s\text{'}\backslash rangle$ there exists $s$\in X such that $\backslash vec\{t\_3\}\backslash langle\; s$\rangle=\vec{t_3}\langle s\rangle, $\backslash vec\{t\_1\}\backslash langle\; s$\rangle=\vec{t_1}\langle s\rangle and $\backslash vec\{t\_2\}\backslash langle\; s$\rangle=\vec{t_2}\langle s'\rangle.

Independence logic corresponds to existential second-order logic, in the sense that a non-empty class of teams is definable by an independence logic formula if and only if the corresponding class of relations is definable by an existential second-order formula.Galliani 2012 Therefore, on the level of open formulas, independence logic is strictly stronger in expressive power than dependence logic. However, on the level of sentences these logics are equivalent.Grädel and Väänänen

Inclusion/exclusion logic extends first-order logic with inclusion atoms $\backslash vec\{t\_1\}\; \backslash subseteq\; \backslash vec\{t\_2\}$ and exclusion atoms $\backslash vec\{t\_1\}\; \backslash mid\; \backslash vec\{t\_2\}$ where in both formulas $\backslash vec\{t\_1\}$ and $\backslash vec\{t\_2\}$ are term tuples of the same length. The semantics of these atoms is defined as follows:

• $\backslash mathcal\; A\; \backslash models\_X\; \backslash vec\{t\_1\}\; \backslash subseteq\; \backslash vec\{t\_2\}$ if and only if for all $s\backslash in\; X$ there exists $s\text{'}\backslash in\; X$ such that $\backslash vec\{t\_1\}\backslash langle\; s\backslash rangle\; =\backslash vec\{t\_2\}\backslash langle\; s\text{'}\backslash rangle$;
• $\backslash mathcal\; A\; \backslash models\_X\; \backslash vec\{t\_1\}\; \backslash mid\; \backslash vec\{t\_2\}$ if and only if for all $s,s\text{'}\backslash in\; X$ it holds that $\backslash vec\{t\_1\}\backslash langle\; s\backslash rangle\; \backslash neq\; \backslash vec\{t\_2\}\backslash langle\; s\text{'}\backslash rangle$.

Inclusion/exclusion logic has the same expressive power as independence logic, already on the level of open formulas.Galliani 2012 Inclusion logic and exclusion logic are obtained by adding only inclusion atoms or exclusion atoms to first-order logic, respectively. Inclusion logic sentences correspond in expressive power to greatest fixed-point logic sentences; hence inclusion logic captures (least) fixed-point logic on finite models, and PTIME over finite ordered models.Galliani and Hella 2013 Exclusion logic in turn corresponds to dependence logic in expressive power.Galliani 2012

Another way of extending dependence logic is to add some generalized quantifiers to the language of dependence logic. Very recently there has been some study of dependence logic with monotone generalized quantifiersEngström and dependence logic with a certain majority quantifier, the latter leading to a new descriptive complexity characterization of the counting hierarchy.Durand, Ebbing, Kontinen, Vollmer 2011

• Game semantics
• Branching quantifier
• Independence-friendly logic

{{reflist|3}}

{{refbegin}}

• {{wikicite |ref=refAbrVaan09 |reference=Abramsky, Samson and Väänänen, Jouko (2009), 'From IF to BI'. Synthese 167(2): 207–230.}}
• {{wikicite |ref=refDurEbb11 |reference= Durand, Arnaud; Ebbing Johannes; Kontinen, Juha and Vollmer Heribert (2011), '[http://drops.dagstuhl.de/opus/volltexte/2011/3346/pdf/28.pdf Dependence logic with a majority quantifier]'. FSTTCS 2011: 252-263.}}
• {{wikicite |ref=refDurKon12 |reference= Durand, Arnaud and Kontinen, Juha, '[https://www.academia.edu/18703455/Hierarchies_in_Dependence_Logic Hierarchies in Dependence Logic]'. ACM Transactions on Computational Logic, 2012.}}
• {{wikicite |ref=refEnderton70 |reference=Enderton, Herbert B. (1970), 'Finite {{sic|hide=y|partially|-}}ordered quantifiers'. Z. Math. Logik Grundlagen Math., 16: 393–397.}}
• {{wikicite |ref=refEng12 |reference= Engström, Fredrik, '[https://arxiv.org/abs/1103.0396 Generalized quantifiers in dependence logic]'. Journal of Logic, Language and Information, to appear.}}
• {{wikicite |ref=refGal12 |reference= Galliani, Pietro (2012), '[https://www.sciencedirect.com/science/article/pii/S0168007211001217/pdf?md5=13f28c1160e72f36688687744f6dc76d&pid=1-s2.0-S0168007211001217-main.pdf&_valck=1 Inclusion and Exclusion in Team Semantics - On some logics of imperfect information]'. Annals of Pure and Applied Logic 163(1): 68-84.}}
• {{wikicite |ref=refGalHella13 |reference= Galliani, Pietro and Hella, Lauri (2013), '[http://drops.dagstuhl.de/opus/volltexte/2013/4203/pdf/23.pdf Inclusion Logic and Fixed Point Logic]'. Proceedings of Computer Science Logic 2013 (CSL 2013), Leibniz International Proceedings in Informatics (LIPIcs) 23, 281-295.}}
• {{wikicite |ref=refGrVaan12 |reference= Grädel, Erich and Väänänen, Jouko, '[http://www.math.helsinki.fi/logic/people/jouko.vaananen/Graedel_Vaananen_final.pdf Dependence and independence]'. Studia Logica, to appear.}}
• {{wikicite |ref=refHintikka02 |reference=Hintikka, Jaakko (2002), '[http://www.cambridge.org/gb/knowledge/isbn/item1158300/?site_locale=en_GB The Principles of Mathematics Revisited]', {{isbn|978-0-521-62498-5}}.}}
• {{wikicite |ref=refHodges97 |reference=Hodges, Wilfrid (1997), '[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.37.5740&rep=rep1&type=ps Compositional semantics for a language of imperfect information]'. Logic Journal of the IGPL 5: 539–563.}}
• {{wikicite |ref=refKontNurmi09 |reference= Kontinen, Juha and Nurmi, Ville (2009), 'Team Logic and Second-Order Logic'. In [https://doi.org/10.1007%2F978-3-642-02261-6 Logic, Language, Information and Computation], pp. 230–241.}}
• {{wikicite |ref=refKontVaan09 |reference= Kontinen, Juha and Väänänen, Jouko (2009), 'On definability in dependence logic'. Journal of Logic, Language and Information 18(3): 317–332.}}
• {{wikicite |ref=refKontVaan09b|reference= Kontinen, Juha and Väänänen, Jouko (2009), '[http://www.ml.kva.se/preprints/files/IML-0910f-22.pdf A Remark on Negation of Dependence Logic]'. Notre Dame Journal of Formal Logic, 52(1):55-65, 2011.}}
• {{wikicite |ref=refLohmVoll10 |reference= Lohmann, Peter and Vollmer, Heribert (2010), 'Complexity Results for Modal Dependence Logic'. In Lecture Notes in Computer Science, pp. 411–425.}}
• {{wikicite |ref=refSevenster09|reference= Sevenster, Merlijn (2009), '[https://ieeexplore.ieee.org/abstract/document/8133055/ Model-theoretic and Computational Properties of Modal Dependence Logic]'. Journal of Logic and Computation 19(6): 1157–1173.}}
• {{wikicite |ref=refVaananen07 |reference=Väänänen, Jouko (2007), '[https://web.archive.org/web/20150822235254/http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521876599 Dependence Logic -- A New Approach to Independence Friendly Logic]', {{isbn|978-0-521-87659-9}}.}}
• {{wikicite |ref=refVaananen08 | reference= Väänänen, Jouko (2008), '[http://www.math.helsinki.fi/logic/people/jouko.vaananen/modaldependencelogic.pdf Modal dependence logic]'. New Perspectives in Logic and Interaction, pp. 237–254.}}
• {{wikicite |ref=refWalkoe70 | reference= Walkoe, Wilbur J. (1970), [https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/finite-partiallyordered-quantification/115E0CF95F881AF1B95A9D72DE54D6FF 'Finite {{sic|hide=y|partially|-}}ordered quantification]'. Journal of Symbolic Logic, 35: 535–575.}}
• {{wikicite |ref=refYang10 | reference= Yang, Fan (2010), 'Expressing Second-order Sentences in Intuitionistic Dependence Logic'. Dependence and Independence in Logic proceedings, pp. 118–132.}}

{{refend}}

• {{cite SEP |url-id=logic-dependence |title=Dependence Logic|last=Galliani |first=Pietro}}
• Special issue of Studia Logica on [https://link.springer.com/journal/11225/101/2/page/1 "Dependence and Independence in Logic"], containing a number of articles on Dependence Logic
• [https://www.knaw.nl/en/news/calendar/dependence-logic?set_language=en Presentations in Academy Colloquium Dependence Logic, Amsterdam, 2014]

Category:Systems of formal logic