However, dependence logic differs from these logics in that it separates the notions of dependence and independence from the notion of quantification.
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.
For a fixed signature σ, the set of all formulas
of dependence logic and their respective sets of free variables
are defined as follows: Nothing is a dependence logic formula unless it can be obtained through a finite number of applications of these four rules.
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.
[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.
It may be helpful to visualize such a team as a database relation with attributes
and with only one data type, corresponding to the domain A of the structure: for example, if the team X consists of four assignments
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.
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.
need to be performed simultaneously: Dependence logic is a conservative extension of first-order logic:[4] in other words, for every first-order sentence
if and only if the domain of this model is infinite, even though no first-order formula
[7] 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 is equivalent to the dependence logic sentence
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.
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
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
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
hold in the same model, then there exists a first-order sentence
then 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
Its expressive power is equivalent to that of full second-order logic.
[20] The dependence atom, or a suitable variant thereof, can be added to the language of modal logic, thus obtaining modal dependence logic.
The semantics of these atoms is defined as follows: 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.
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.