Comonadic semantics for guarded fragments

TL;DR

This paper extends comonadic semantics to guarded fragments of first-order logic, linking model comparison games, combinatorial parameters, and guarded tree decompositions within a categorical framework.

Contribution

It systematically develops comonadic semantics for guarded fragments, capturing winning strategies and equivalences through coKleisli morphisms and spans, and relates these to guarded tree decompositions.

Findings

CoKleisli morphisms capture Duplicator's winning strategies.

Full guarded fragment equivalence is characterized by spans of open morphisms.

Coalgebras correspond to guarded tree decompositions.

Abstract

In previous work, Abramsky, Dawar and Wang (LiCS 2017) and Abramsky and Shah (CSL 2018) have shown how a range of model comparison games which play a central role in finite model theory, including Ehrenfeucht-Fraisse, pebbling, and bisimulation games, can be captured in terms of resource-indexed comonads on the category of relational structures. Moreover, the coalgebras for these comonads capture important combinatorial parameters such as tree-width and tree-depth. The present paper extends this analysis to quantifier-guarded fragments of first-order logic. We give a systematic account, covering atomic, loose and clique guards. In each case, we show that coKleisli morphisms capture winning strategies for Duplicator in the existential guarded bisimulation game, while back-and-forth bisimulation, and hence equivalence in the full guarded fragment, is captured by spans of open morphisms. We study the coalgebras for these comonads, and show that they correspond to guarded tree decompositions. We relate these constructions to a syntax-free setting, with a comonad on the category of hypergraphs.