Dependence logic is a logical formalism, created by Jouko Väänänen,[1] which adds dependence atoms to the language of first-order logic. A dependence atom is an expression of the form
=(t1\ldotstn)
t1\ldotstn
tn
t1,\ldots,tn-1
Dependence logic is a logic of imperfect information, like branching quantifier logic or independence-friendly logic (IF logic): in other words, its game-theoretic semantics can be obtained from that of first-order logic by restricting the availability of information to the players, thus allowing for non-linearly ordered patterns of dependence and independence between variables. However, dependence logic differs from these logics in that it separates the notions of dependence and independence from the notion of quantification.
The syntax of dependence logic is an extension of that of first-order logic. For a fixed signature σ = (Sfunc, Srel, 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:
Rt1\ldotstn
R
(t1,\ldots,tn)
t1=t2
t1
t2
=(t1\ldotstn)
n\inN
(t1,\ldots,tn)
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
\phi
Free(\phi)
\phi
Free(\phi)
\phi
lnot\phi
Free(lnot\phi)=Free(\phi)
\phi
\psi
\phi\vee\psi
Free(\phi\vee\psi)=Free(\phi)\cupFree(\psi)
\phi
x
\existsx\phi
Free(\existsv\phi)=Free(\phi)\backslash\{v\}
Nothing is a dependence logic formula unless it can be obtained through a finite number of applications of these four rules.
A formula
\phi
Free(\phi)=\emptyset
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,
\phi\wedge\psi
lnot(lnot\phi\veelnot\psi)
\forallx\phi
lnot(\existsx(lnot\phi))
The team semantics for dependence logic is a variant of Wilfrid Hodges' compositional semantics for IF logic.[2] [3] There exist equivalent game-theoretic semantics for dependence logic, both in terms of imperfect information games and in terms of perfect information games.
Let
lA=(A,\sigma,I)
V=\{v1,\ldots,vn\}
It may be helpful to visualize such a team as a database relation with attributes
v1,\ldots,vn
\mu1,\ldots,\mu4
\{v1,v2,v3\}
\begin{array}{c|ccc} &v1&v2 &v3 \\ \hline \mu1& \mu1(v1)&\mu1(v2)&\mu1(v3) \\ \mu2& \mu2(v1)&\mu2(v2)&\mu2(v3) \\ \mu3& \mu3(v1)&\mu3(v2)&\mu3(v3) \\ \mu4& \mu4(v1)&\mu4(v2)&\mu4(v3) \end{array}
Team semantics can be defined in terms of two relations
lT
lC
Given a structure
lA
X
\phi
X
(lA,X,\phi)\inlT
X
\phi
lA
lA
+ | |
\models | |
X |
\phi
(lA,X,\phi)\inlC
X
\phi
lA
lA
- | |
\models | |
X |
\phi
If
lA
+ | |
\models | |
X |
\phi
\phi
X
lA
lA
- | |
\models | |
X |
\phi
\phi
X
lA
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
\phi
\phi
lA
lA\models\{\emptyset\
\phi
lA
lA\models\{\emptyset\
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
\models+
\models-
lA
+ | |
\models | |
X |
Rt1\ldotstn
R
lA
t1,\ldots,tn
X
\mu\inX
(t1,\ldots,tn)
\mu
R
lA
lA
+ | |
\models | |
X |
t1=t2
t1
t2
X
\mu\inX
t1
t2
lA
lA
+ | |
\models | |
X |
=(t1\ldotstn)
\mu,\mu'\inX
(t1,\ldots,tn-1)
tn
lA
+ | |
\models | |
X |
lnot\phi
lA
- | |
\models | |
X |
\phi
lA
+ | |
\models | |
X |
\phi\vee\psi
Y
Z
X=Y\cupZ'
lA
+ | |
\models | |
Y |
\phi
lA
+ | |
\models | |
Z |
\psi
lA
+ | |
\models | |
X |
\existsx\phi
F
X
lA
lA
+ | |
\models | |
X[F/x] |
\phi
X[F/x]=\{\mu[F(\mu)/x]:\mu\inX\}
lA
- | |
\models | |
X |
Rt1\ldotstn
R
lA
t1,\ldots,tn
X
\mu\inX
(t1,\ldots,tn)
\mu
R
lA
lA
- | |
\models | |
X |
t1=t2
t1
t2
X
\mu\inX
t1
t2
lA
lA
- | |
\models | |
X |
=(t1\ldotstn)
X
lA
- | |
\models | |
X |
lnot\phi
lA
+ | |
\models | |
X |
\phi
lA
- | |
\models | |
X |
\phi\vee\psi
lA
- | |
\models | |
X |
\phi
lA
- | |
\models | |
X |
\psi
lA
- | |
\models | |
X |
\existsx\phi
lA
- | |
\models | |
X[A/x] |
\phi
X[A/x]=\{\mu[a/x]:a\inA\}
A
lA
Dependence logic is a conservative extension of first-order logic:[4] in other words, for every first-order sentence
\phi
lA
lA\models\{\emptyset\
\phi
lA
\phi
lA
+ | |
\models | |
X |
\phi
\mu\inX
\phi
lA
However, dependence logic is strictly more expressive than first-order logic:[5] for example, the sentence
\existsz\forallx1\forallx2\existsy1\existsy2(=(x1,y1)\wedge=(x2,y2)\wedge(x1=x2\leftrightarrowy1=y2)\wedgey1\not=z)
lA
\phi
Every dependence logic sentence is equivalent to some sentence in the existential fragment of second-order logic,[6] that is, to some second-order sentence of the form
\existsR1\ldots\existsRn\psi(R1,\ldots,Rn)
where
\psi(R1,\ldots,Rn)
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.[8]
Branching quantifiers are expressible in terms of dependence atoms: for example, the expression
(QHx1,x2,y1,y2)\phi(x1,x2,y1,y2)\equiv\begin{pmatrix}\forallx1\existsy1\ \forallx2\existsy2\end{pmatrix}\phi(x1,x2,y1,y2)
\forallx1\existsy1\forallx2\existsy2(=(x1,y1)\wedge=(x2,y2)\wedge\phi)
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.[9] [10]
Any dependence logic sentence is logically equivalent to some IF logic sentence, and vice versa.[11]
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=\{v1\ldotsvn\}
\phi
V
\phiD
lA
+ | |
\models | |
X |
\phi\LeftrightarrowlA
+ | |
\models | |
X |
\phiD
lA
X
V
\psi
V
\psiI
lA
+ | |
\models | |
X |
\psi\LeftrightarrowlA
+ | |
\models | |
X |
\psiI
lA
X
V
Dependence logic formulas are downwards closed: if
lA\modelsX\phi
Y\subseteqX
lA\modelsY\psi
The law of the excluded middle fails in dependence logic: for example, the formula
\existsy(=(y)\wedgey=x)
X=\{(x:0),(x:1)\}
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
\phi
\psi
\phi
\psi
\theta
\phi
\theta
\theta
\psi
As for IF logic,[15] dependence logic can define its own truth operator:[16] more precisely, there exists a formula
\tau(x)
\phi
lM\omega
'\phi'
\phi
lM\omega
+ | |
\models | |
\{\emptyset\ |
lM\omega
+ | |
\models | |
\{\emptyset\ |
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.[17]
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
\Pi2
Team logic[19] extends dependence logic with a contradictory negation
\sim\phi
The dependence atom, or a suitable variant thereof, can be added to the language of modal logic, thus obtaining modal dependence logic.[21] [22] [23]
As it is, dependence logic lacks an implication. The intuitionistic implication
\phi → \psi
lA\modelsX\phi → \psi
Y\subseteqX
lA\modelsY\phi
lA\modelsY\psi
Intuitionistic dependence logic, that is, dependence logic supplemented with the intuitionistic implication, is equivalent to second-order logic.[25]
Instead of dependence atoms, independence logic adds to the language of first-order logic independence atoms
\vec{t1}\bot
\vec{t3 |
\vec{t1}
\vec{t2}
\vec{t3}
lA\modelsX\vec{t1}\bot
\vec{t3 |
s,s'\inX
\vec{t3}\langles\rangle=\vec{t3}\langles'\rangle
s''\inX
\vec{t3}\langles''\rangle=\vec{t3}\langles\rangle
\vec{t1}\langles''\rangle=\vec{t1}\langles\rangle
\vec{t2}\langles''\rangle=\vec{t2}\langles'\rangle
Inclusion/exclusion logic extends first-order logic with inclusion atoms
\vec{t1}\subseteq\vec{t2}
\vec{t1}\mid\vec{t2}
\vec{t1}
\vec{t2}
lA\modelsX\vec{t1}\subseteq\vec{t2}
s\inX
s'\inX
\vec{t1}\langles\rangle=\vec{t2}\langles'\rangle
lA\modelsX\vec{t1}\mid\vec{t2}
s,s'\inX
\vec{t1}\langles\rangle ≠ \vec{t2}\langles'\rangle
Inclusion/exclusion logic has the same expressive power as independence logic, already on the level of open formulas.[28] 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.[29] Exclusion logic in turn corresponds to dependence logic in expressive power.[30]
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 quantifiers[31] and dependence logic with a certain majority quantifier, the latter leading to a new descriptive complexity characterization of the counting hierarchy.[32]