Logic@GU

The mu-calculus is obtained from basic modal logic by adding least and greatest fixpoint operators. By doing so a lot of expressive power is added to the logic. However, the semantics can only be evaluated over labelled transition systems. Coalgebraic modal logic generalizes the basic modal logic and lets us evaluate the semantics over different coalgebras, instead of only labelled transition systems. In the coalgebraic mu-calculus, the expressive power of the mu-calculus and the generality of coalgebraic modal logic are combined.

In this talk we will introduce the coalgebraic mu-calculus and how to handle proof systems for this family of logics.

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