Dependence logic, introduced in Väänänen [11], cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized, and this is what we shall do in this paper. We give an explicit axiomatization and prove the respective Completeness Theorem.

Modal dependence logic was introduced recently by Väänänen. It enhances the basic modal language by an operator = (). For propositional variables p 1, . . . , p n , = (p 1, . . . , p n-1, p n ) intuitively states that the value of p n is determined by those of p 1, . . . , p n-1. Sevenster (J. Logic and Computation, 2009) showed that satisfiability for modal dependence logic is complete for nondeterministic (...) exponential time.In this paper we consider fragments of modal dependence logic obtained by restricting the set of allowed propositional connectives. We show that satisfiability for poor man’s dependence logic, the language consisting of formulas built from literals and dependence atoms using ${\wedge, \square, \lozenge}$ (i. e., disallowing disjunction), remains NEXPTIME-complete. If we only allow monotone formulas (without negation, but with disjunction), the complexity drops to PSPACE-completeness.We also extend Väänänen’s language by allowing classical disjunction besides dependence disjunction and show that the satisfiability problem remains NEXPTIME-complete. If we then disallow both negation and dependence disjunction, satisfiability is complete for the second level of the polynomial hierarchy. Additionally we consider the restriction of modal dependence logic where the length of each single dependence atom is bounded by a number that is fixed for the whole logic. We show that the satisfiability problem for this bounded arity dependence logic is PSPACE-complete and that the complexity drops to the third level of the polynomial hierarchy if we then disallow disjunction.In this way we completely classify the computational complexity of the satisfiability problem for all restrictions of propositional and dependence operators considered by Väänänen and Sevenster. (shrink)

We characterize the expressive power of extensions of Dependence Logic and Independence Logic by monotone generalized quanti ers in terms of quanti er extensions of existential second-order logic.

We introduce an atomic formula ${\vec{y} \bot_{\vec{x}}\vec{z}}$ intuitively saying that the variables ${\vec{y}}$ are independent from the variables ${\vec{z}}$ if the variables ${\vec{x}}$ are kept constant. We contrast this with dependence logic ${\mathcal{D}}$ based on the atomic formula = ${(\vec{x}, \vec{y})}$ , actually equivalent to ${\vec{y} \bot_{\vec{x}}\vec{y}}$ , saying that the variables ${\vec{y}}$ are totally determined by the variables ${\vec{x}}$ . We show that ${\vec{y} \bot_{\vec{x}}\vec{z}}$ gives rise to a natural logic capable of formalizing basic intuitions about independence and dependence. (...) We show that ${\vec{y} \bot_{\vec{x}}\vec{z}}$ can be used to give partially ordered quantifiers and IF-logic an alternative interpretation without some of the shortcomings related to so called signaling that interpretations using = ${(\vec{x}, \vec{y})}$ have. (shrink)

The properties of the ${\forall^{1}}$ quantifier defined by Kontinen and Väänänen in [13] are studied, and its definition is generalized to that of a family of quantifiers ${\forall^{n}}$ . Furthermore, some epistemic operators δ n for Dependence Logic are also introduced, and the relationship between these ${\forall^{n}}$ quantifiers and the δ n operators are investigated.The Game Theoretic Semantics for Dependence Logic and the corresponding Ehrenfeucht- Fraissé game are then adapted to these new connectives.Finally, it is proved that the ${\forall^{1}}$ quantifier (...) is not uniformly definable in Dependence Logic, thus answering a question posed by Kontinen and Väänänen in the above mentioned paper. (shrink)

We show that for any pair $\phi$ and $\psi$ of contradictory formulas of dependence logic there is a formula $\theta$ of the same logic such that $\phi\equiv\theta$ and $\psi\equiv\neg\theta$. This generalizes a result of Burgess.

We identify the computational complexity of the satisfiability problem for FO 2 , the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite (...) model. Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

Intuitionistic dependence logic was introduced by Abramsky and Väänänen [1] as a variant of dependence logic under a general construction of Hodges’ (trump) team semantics. It was proven that there is a translation from intuitionistic dependence logic sentences into second order logic sentences. In this paper, we prove that the other direction is also true, therefore intuitionistic dependence logic is equivalent to second order logic on the level of sentences.

We develop a semantics for independence logic with respect to what we will call general models. We then introduce a simpler entailment semantics for the same logic, and we reduce the validity problem in the former to the validity problem in the latter. Then we build a proof system for independence logic and prove its soundness and completeness with respect to entailment semantics.

We introduce generalized quantifiers, as defined in Tarskian semantics by Mostowski and Lindström, in logics whose semantics is based on teams instead of assignments, e.g., IF-logic and Dependence logic. Both the monotone and the non-monotone case is considered. It is argued that to handle quantifier scope dependencies of generalized quantifiers in a satisfying way the dependence atom in Dependence logic is not well suited and that the multivalued dependence atom is a better choice. This atom is in fact definably equivalent (...) to the independence atom recently introduced by Väänänen and Grädel. (shrink)

We study the expressive power of open formulas of dependence logic introduced in Väänänen [Dependence logic (Vol. 70 of London Mathematical Society Student Texts), 2007]. In particular, we answer a question raised by Wilfrid Hodges: how to characterize the sets of teams definable by means of identity only in dependence logic, or equivalently in independence friendly logic.

We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Väänänen, and their compositional semantics due to Hodges. We show how Hodges’ semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by the semantics (...) is the logic of Bunched Implications due to Pym and O’Hearn, which combines intuitionistic and multiplicative connectives. This introduces several new connectives not previously considered in logics of informational dependence, but which we show play a very natural rôle, most notably intuitionistic implication. As regards the quantifiers, we show that their interpretation in the Hodges semantics is forced, in that they are the image under the general construction of the usual Tarski semantics; this implies that they are adjoints to substitution, and hence uniquely determined. As for the dependence predicate, we show that this is definable from a simpler predicate, of constancy or dependence on nothing. This makes essential use of the intuitionistic implication. The Armstrong axioms for functional dependence are then recovered as a standard set of axioms for intuitionistic implication. We also prove a full abstraction result in the style of Hodges, in which the intuitionistic implication plays a very natural rôle. (shrink)

We present a compositional semantics for first-order logic with imperfect information that is equivalent to Sevenster and Sandu’s equilibrium semantics (under which the truth value of a sentence in a finite model is equal to the minimax value of its semantic game). Our semantics is a generalization of an earlier semantics developed by the first author that was based on behavioral strategies, rather than mixed strategies.

We study the computational complexity of the model checking problem for quantifier-free dependence logic ${(\mathcal{D})}$ formulas. We characterize three thresholds in the complexity: logarithmic space (LOGSPACE), non-deterministic logarithmic space (NL) and non-deterministic polynomial time (NP).

We identify the computational complexity of the satisfiability problem for FO 2, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite model. (...) Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

Independence‐Friendly logic introduced by Hintikka and Sandu studies patterns of dependence and independence of quantifiers which exceed those found in ordinary first‐order logic. The present survey focuses on the game‐theoretical interpretation of IF‐logic, including connections to solution concepts in classical game theory, but we shall also present its compositional interpretation together with its connections to notions of dependence and dependence between terms.