Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Game Comonads & Generalised Quantifiers

Adam Ó Conghaile, Anuj Dawar

TL;DR

The paper develops a categorical framework for logics with generalised quantifiers by extending game comonads. It introduces the graded comonad Hn,k as a quotient of the pebbling comonad Pk, establishing that Kleisli morphisms correspond to Duplicator strategies in a one-way k-pebble, n-bijection game, and that isomorphisms capture equivalence in a natural n-ary, infinitary logic with generalized quantifiers. A central contribution is the equivalence between Hn,k-coalgebras and a new notion of extended tree decompositions of width k and arity n, providing a generalized locality notion that encompasses traditional treewidth/treedepth decompositions as special cases. The paper also develops an eight-variant taxonomy of games and logics linked to restricted quantifier classes and proves crucial equivalences among them, including the KV and Hella logics. This categorical and decompositional lens yields a unified perspective on generalized quantifiers, with potential extensions to other quantifier classes and related descriptive-complexity frameworks.

Abstract

Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose connections between one-sided and two-sided games, and parameters such as treewidth and treedepth and corresponding notions of decomposition. In the present paper, we expand the realm of game comonads to logics with generalised quantifiers. In particular, we introduce a comonad graded by two parameters $n \leq k$ such that isomorphisms in the resulting Kleisli category are exactly Duplicator winning strategies in Hella's $n$-bijection game with $k$ pebbles. We define a one-sided version of this game which allows us to provide a categorical semantics for a number of logics with generalised quantifiers. We also give a novel notion of tree decomposition that emerges from the construction.

Game Comonads & Generalised Quantifiers

TL;DR

The paper develops a categorical framework for logics with generalised quantifiers by extending game comonads. It introduces the graded comonad Hn,k as a quotient of the pebbling comonad Pk, establishing that Kleisli morphisms correspond to Duplicator strategies in a one-way k-pebble, n-bijection game, and that isomorphisms capture equivalence in a natural n-ary, infinitary logic with generalized quantifiers. A central contribution is the equivalence between Hn,k-coalgebras and a new notion of extended tree decompositions of width k and arity n, providing a generalized locality notion that encompasses traditional treewidth/treedepth decompositions as special cases. The paper also develops an eight-variant taxonomy of games and logics linked to restricted quantifier classes and proves crucial equivalences among them, including the KV and Hella logics. This categorical and decompositional lens yields a unified perspective on generalized quantifiers, with potential extensions to other quantifier classes and related descriptive-complexity frameworks.

Abstract

Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose connections between one-sided and two-sided games, and parameters such as treewidth and treedepth and corresponding notions of decomposition. In the present paper, we expand the realm of game comonads to logics with generalised quantifiers. In particular, we introduce a comonad graded by two parameters such that isomorphisms in the resulting Kleisli category are exactly Duplicator winning strategies in Hella's -bijection game with pebbles. We define a one-sided version of this game which allows us to provide a categorical semantics for a number of logics with generalised quantifiers. We also give a novel notion of tree decomposition that emerges from the construction.

Paper Structure

This paper contains 26 sections, 16 theorems, 34 equations, 3 figures.

Table of Contents

  1. Background
  2. Logics
  3. Generalised quantifiers
  4. Games
  5. Comonads
  6. Games and Logic with Generalised Quantifiers
  7. Relaxing Bijkn
  8. Logics with generalised quantifiers
  9. Lk(Qbn) and Lk∞(Qn) are equivalent
  10. Generalised quantifiers and size
  11. Games and logics correspond
  12. The Hella Comonad and its Kleisli Category
  13. Translating between games
  14. Lifting the comonad Pk to Hn,k
  15. Classifying the morphisms of K(Hn,k)
  16. ...and 11 more sections

Key Result

Lemma 2.8

For all $n, k \in \mathbb{N}$, $\mathcal{L}^{k}(\mathcal{Q}^{\text{b}}_n) \equiv \mathcal{L}_{\infty}^{k}(\mathcal{Q}_n)$.

Figures (3)

  • Figure 1: Hasse Diagram of Games
  • Figure 2: Hasse Diagram of Logics
  • Figure 3: Cube of parameters

Theorems & Definitions (57)

  • Remark 1.1
  • Remark 1.2
  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Lemma 2.8
  • proof
  • Definition 2.10
  • ...and 47 more