An invitation to game comonads

TL;DR

This paper explores game comonads, a categorical framework that unifies model comparison games with resource-bounded logic, revealing new connections between semantics, combinatorics, and algorithms.

Contribution

It introduces the categorical perspective of game comonads and demonstrates their applications in finite model theory and resource-sensitive logic.

Findings

Coalgebras for game comonads capture preservation of logical fragments.

Connections established between categorical semantics and combinatorial parameters.

Applications include homomorphism counting and preservation theorems.

Abstract

Game comonads offer a categorical view of a number of model-comparison games central to model theory, such as pebble and Ehrenfeucht-Fra\"iss\'e games. Remarkably, the categories of coalgebras for these comonads capture preservation of several fragments of resource-bounded logics, such as (infinitary) first-order logic with n variables or bounded quantifier rank, and corresponding combinatorial parameters such as tree-width and tree-depth. In this way, game comonads provide a new bridge between categorical methods developed for semantics, and the combinatorial and algorithmic methods of resource-sensitive model theory. We give an overview of this framework and outline some of its applications, including the study of homomorphism counting results in finite model theory, and of equi-resource homomorphism preservation theorems in logic using the axiomatic setting of arboreal categories. Finally, we describe some homotopical ideas that arise naturally in the context of game comonads.