Jouko Väänänen

Joni Puljujärvi, Jouko Väänänen

We define a new Ehrenfeucht-Fraïssé game for dependence logic. The previously known rendition of such a game was based on moves that are teams. Since teams can be massive, making team moves may be quite complicated. To remedy this, our new Ehrenfeucht-Fraïssé game for dependence logic has only moves that consist of single elements, as in the classical Ehrenfeucht-Fraïssé game of first order logic. A new feature of the game is that a player can declare that their move is made on the basis of certain previous moves only and thereby in a sense independent of other moves. We show that our game characterizes elementary equivalence in dependence logic.

Timon Barlag, Nicolas Fröhlich, Miika Hannula et al.

Dependence logic extends first-order logic with dependence atoms asserting that the value of a variable is determined by the values of certain other variables. The semantics of dependence logic has a second-order character and involves sets of assignments, called teams, instead of individual assignments as in the classical Tarski semantics. Since the model-checking problem is known to be NP-complete even for quantifier-free dependence logic (DQF) formulas, researchers have pursued conditions on formulas that make this problem tractable. In 2010, Jarmo Kontinen introduced the notion of k-coherence for dependence logic formulas, where k is a positive integer. This notion asserts that if the formula is satisfied in a structure by all k-element subteams of a given team, then the given team itself satisfies the formula. It has been proved that k-coherent DQF-formulas have a tame model-checking problem, because such formulas admit a first-order rewriting. In this paper, we investigate the structural and algorithmic aspects of coherence. We show that if a DQF-formula is first-order ewritable, then it is k-coherent for some positive integer k. Thus, for DQF-formulas, coherence is equivalent to first-order rewritability. Furthermore, we show that an analogous result holds for universally quantified dependence logic formulas under a stronger notion of coherence. After this, we focus on the complexity of deciding if a given dependence logic formula is k-coherent. We establish that this decision problem is highly undecidable for arbitrary dependence logic formulas, while for DQF-formulas this problem is co-recursively enumerable. Furthermore, we pinpoint the computational complexity of the coherence problem for propositional dependence logic formulas by showing that this problem is complete for the second level of the exponential hierarchy.