Public:Known Game Comonads

\( \newcommand\Ck{\mathbb C_k} \newcommand\Hom{\mathrm{Hom}} \newcommand\qtq[1]{\quad\text{#1}\quad} \)

In this page we gather the most important game comonads explored so far.

Convention:

• $$A \leftrightarrows_k B$$ iff there exist homomorphisms $$\Ck A \to B$$ and $$\Ck B \to A$$
• $$A \leftrightarrow_k B$$ iff there exists a span of open pathwise embeddings $$R \to \Ck A$$ and $$R \to \Ck B$$
• $$A \cong_{\mathrm{Kl}(\Ck)} B$$ iff $$A$$ and $$B$$ are isomorphic in the coKleisli category for $$\Ck$$, i.e. there exist homomorphisms $$f\colon\Ck A \to B$$ and $$g\colon\Ck B \to A$$ such that both $$f^* g^*$$ and $$g^* f^*$$ are identities

Typically, each of those equivalences corresponds to a certain logical equivalence. That is, we have that

1. $$A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists^+ \mathcal L} B$$
2. $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\mathcal L} B$$
3. $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\mathcal L^\#} B$$

where $$\exists^+ \mathcal L$$ is the existential-positive fragment of a certain logic $$\mathcal L$$ and $$\mathcal L^\#$$ is the extension of $$\mathcal L$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$.

Comonad	$$\Ck$$	Logic $$\mathcal L$$	$$\leftrightarrows_k$$	$$\leftrightarrow_k$$	$$\cong_{\mathrm{Kl}(\Ck)}$$	Coalgebras
Pebbling	$$\mathbb P_k$$	$$k$$-variable fragment $$\mathcal L^k$$ of FOL	$$\exists^+ \mathcal L^k$$	$$\mathcal L^k$$ (wrt $$I$$-morphisms)	$$(\mathcal L^k)^\#$$ (wrt $$I$$-morphisms)	tree width $${<} k$$
Ehrenfeucht-Fraissé	$$\mathbb E_k$$	quantifier rank $${\leq} k$$ fragment $$\mathcal L_k$$ of FOL	$$\exists^+ \mathcal L_k$$	$$\mathcal L_k$$ (wrt $$I$$-morphisms)	$$(\mathcal L_k)^\#$$ (wrt $$I$$-morphisms)	tree depth $${\leq} k$$
Modal (*)	$$\mathbb M_k$$	modal depth $${\leq} k$$ fragment $$\mathcal M_k$$ of ML	$$\exists^+ \mathcal M_k$$	$$\mathcal M_k$$	$$\mathcal M_k$$ + graded modalities	synchronization trees, depth $${\leq} k$$
Pebble Relation	$$\mathbb {PR}_k$$	$$k$$-variable logic, restricted $$\wedge$$	a fragment $$M^k$$ of $$\exists^+ \mathcal L^k$$	??	??	path width $${<} k$$
"Hella's game"	$$\mathbb H_{n,k}$$ [1]	extension of $$\mathcal L^k$$ with generalised quantifiers	$$\exists^+ \mathcal L^k(\mathcal Q_n^H)$$	$$\mathcal L^k(\mathcal Q_n^H)$$	$$\mathcal L^k_{\infty,\omega}(\mathcal{Q}_{n})$$	$$n$$-ary generalised tree width $${\leq} k$$
Guarded quantifier	$$\mathbb G^{\mathfrak g}_{k}$$	$$\mathfrak g$$-guarded logic w/ width $$\leq k$$	(identified)	(identified)	??	guarded treewidth
Loosely guarded	$$\mathbb{LG}_{k}$$	$$k$$-conjunct guarded logic	(identified)	??	??	hypertree-width
Hybrid comonad	$$\mathbb{HY}_{k}$$	modal depth $$\leq k$$ for hybrid logic	(identified)	(identified)	(identified)	generated tree-depth
Hypergraph comonad

The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs with unary predicates. Note that $$\exists^+ \mathcal M_k$$ denotes the positive $$\Box$$-free fragment of $$\mathcal M_k$$. The $$\leftrightarrows_k$$, $$\leftrightarrow_k$$, and $$\cong_{\mathrm{Kl}(\Ck)}$$ columns mark logic $$\mathcal L$$ such that they correspond to $$\equiv^{\mathcal L}$$ of that logic. Note that \(I\)-morphisms are simply homomorphisms w.r.t. an extended signature, see I-morphisms page.

TODO add the linearized variants of our comonads (i.e. the rebble-relation comoand as well as the the linear variants of Ek and Mk), the reachability variants and also the "immediate successor" variant of Mk due to Gabriel Goren and Santiago Figueira.

TODO further add a little bit about multi-sorted comonads and clarify the relationship with translation functors (e.g. by explaining how to capture logics without equality)