Existential and positive games: a comonadic and axiomatic view
Samson Abramsky, Thomas Laure, Luca Reggio
TL;DR
The paper presents a unifying, syntax-free framework for resource-bounded logical fragments by modeling finite and possibly infinite relational structures with three game comonads: $\mathbb{E}_k$, $\mathbb{P}_k$, and $\mathbb{M}_k$. It shows that existential resource-sensitive fragments are captured by pathwise embeddings between cofree coalgebras, while positive fragments are captured by asymmetric spans called positive bisimulations, within the axiomatic setting of arboreal categories. The results extend known concrete characterisations for FO$_k$, $\mathcal{L}^k$, and ML$_k$ and yield a new proof of an equi-resource Lyndon positivity theorem for modal logic. The work bridges semantics and structure, providing a uniform, resource-aware account that applies to both finite and infinite structures and offers an axiomatic foundation for further logical-preservation theorems. Applications include principled proofs of positivity theorems in modal logic and a richer understanding of how logical resources interact with structural transformations.
Abstract
A number of model-comparison games central to (finite) model theory, such as pebble and Ehrenfeucht-Fraïssé games, can be captured as comonads on categories of relational structures. In particular, the coalgebras for these comonads encode in a syntax-free way preservation of resource-indexed logic fragments, such as first-order logic with bounded quantifier rank or a finite number of variables. In this paper, we extend this approach to existential and positive fragments (i.e., without universal quantifiers and without negations, respectively) of first-order and modal logic. We show, both concretely and at the axiomatic level of arboreal categories, that the preservation of existential fragments is characterised by the existence of so-called pathwise embeddings, while positive fragments are captured by a newly introduced notion of positive bisimulation. As an application, we offer a new proof of an equi-resource Lyndon positivity theorem for (multi)modal logic.