Arboreal Categories: An Axiomatic Theory of Resources
Samson Abramsky, Luca Reggio
TL;DR
This work builds an axiomatic framework of arboreal categories to capture the process-oriented semantics of game comonads and their coalgebras, unifying dynamic bisimulation and back-and-forth reasoning under a resource-sensitive lens. By formalizing path categories and arboreal covers via stable factorisation systems and comonadic adjunctions, it recovers core finite model theory constructs such as EF, pebbling, and modal bisimulation inside a single, syntax-free setting. The coalgebra numbers associated with $G_k$-coalgebras correspond to combinatorial invariants like tree-depth, tree-width, and unfolding depth, explaining why resource-bounded games reflect descriptive complexity. The framework also shows how back-and-forth systems and games characterize bisimilarity in arboreal categories and connects these notions to existential and FO fragments, offering a pathway to axiomatic meta-theory for resource-sensitive model theory. The results pave the way for new arboreal categories and generalized model-theoretic theorems at an axiomatised level, with potential applications to descriptive complexity and beyond.
Abstract
Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or "static" structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fraïssé and modal bisimulation games recently introduced by Abramsky et al. are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.