Feferman–Vaught–Mostowski theorems and game comonads

Abstract: In recent years we have seen a growing number of examples of model comparison games (such as pebble games or Ehrenfreucht-Fraisse games) being encoded semantically, as comonads on the class of graphs or relational structures. Apart from the connections with logic (via the model comparison games), game comonads can also express a range of important parameters in finite model theory and combinatorics, such as tree-width and tree-depth.

After a brief overview of the emerging theory of game comonads, I will present my joint work with Dan Marsden and Nihil Shah. Our main focus are the so-called Feferman–Vaught-Mostowski-type theorems, which express when an operation on models preserves equivalence in a given logic.

Proving these theorems in the comonadic setting amounts to defining a Kleisli law and checking certain smoothness conditions. Surprisingly, the main ingredient of our approach is a generalisation of how monoidal monads lift the monoidal structure to the category of algebras. Furthermore, we also show the role of bilinear maps in this setting and how Johnstone's adjoint lifting theorem is a special case of all this.

game theorylogic in computer scienceprogramming languagescomputer science theorycategory theory

Audience: researchers in the topic

University of Birmingham theoretical computer science seminar

Series comments: Meeting ID: 818 7333 5084 ~ Password: 217