Dependence logic extends first-order logic with dependence atoms, which express that the value of a variable is functionally determined by other variables. Team semantics gives dependence logic a second-order flavour, and even quantifier-free dependence logic formulas can have an NP-complete model-checking problem. This motivates the study of syntactic conditions under which model checking becomes tractable.

The talk starts with a brief introduction to team semantics and dependence logic, and then focuses on coherence, a notion introduced by Jarmo Kontinen to capture when the satisfaction of a formula can be determined by satisfaction by its small subteams. We show that, for quantifier-free formulas, coherence is precisely equivalent to first-order rewritability. We also study the complexity of deciding coherence, obtaining strong undecidability results for dependence logic and a precise complexity classification for propositional dependence logic.

The talk is based on joint work with Timon Barlag, Nicolas Fröhlich, Miika Hannula, Phokion G. Kolaitis, Arne Meier, and Jouko Väänänen: https://arxiv.org/abs/2605.31269