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}\).

1st generation of game comonads

The first comonads described in the game comonad programme were the following.

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	✓	✓ (I)	✓ (I)	tree width \({<} k\)
Ehrenfeucht-Fraissé	\(\mathbb E_k\)	quantifier rank \({\leq} k\) fragment \(\mathcal L_k\) of FOL	✓	✓ (I)	✓ (I)	tree depth \({\leq} k\)
Modal (*)	\(\mathbb M_k\)	modal depth \({\leq} k\) fragment \(\mathcal M_k\) of ML	✓	✓	✓	synchronization trees of depth \({\leq} k\)

The \(\leftrightarrows_k\), \(\leftrightarrow_k\), and \(\cong_{\mathrm{Kl}(\Ck)}\) columns express whether it has been shown that this relation corresponds to a logical equivalence with respect to some fragment of logic \(\mathcal L\). We add a little (I) symbol to designate that this requires the usage of \(I\)-morphisms to capture the equality/identity in the logic, cf. I-morphisms page for explanation.

The comonads we mark with (*) are defined over the category of pointed structures in relational signature with only unary and binary relations. The modal comonad \(\mathbb M_k\) captures the fragment of modal logic \(\mathcal M_k\) consisting of modal formulas of modal depth \(\leq k\). The positive existential fragment \(\exists^+ \mathcal M_k\) of this logic denotes the positive \(\Box\)-free fragment of \(\mathcal M_k\).

2nd generation of game comonads

These comonads are build as variants or modifications of 1st generation comonads. For example, we have the following comonads.

Comonad	\(\Ck\)	Logic \(\mathcal L\)	\(\leftrightarrows_k\)	\(\leftrightarrow_k\)	\(\cong_{\mathrm{Kl}(\Ck)}\)	Coalgebras
Pebble Relation	\(\mathbb {PR}_k\)	\(k\)-variable logic, restricted \(\wedge\)	✓	??	✓	path width \({<} k\)
"Hella's game"	\(\mathbb H_{n,k}\) [1]	extension of \(\mathcal L^k\) with generalised quantifiers	✓	✓	✓	\(n\)-ary generalised tree width \({\leq} k\)
Guarded quantifier	\(\mathbb G^{\mathfrak g}_{k}\)	\(\mathfrak g\)-guarded logic w/ width \(\leq k\)	✓	✓	??	guarded treewidth
Loosely guarded	\(\mathbb{LG}_{k}\)	\(k\)-conjunct guarded logic	✓	??	??	hypertree-width
Hybrid comonad	\(\mathbb{HY}_{k}\)	modal depth \(\leq k\) for hybrid logic	✓	✓	✓	generated tree-depth

The common techniques of constructing new comonads from the old ones include:

• 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 (which includes the "immediate successor" variant of Mk due to Gabriel Goren and Santiago Figueira)
• quotienting of the previously described comonad (e.g. "Hella's comonad" and also "Hybrid comonad", as variants of Pk and Ek, respectively).

3nd generation of game comonads

These are comonads where the signature or base category was modified more than by just adding the \(I\)-relation to the signature.

Comonad	\(\Ck\)	Logic \(\mathcal L\)	\(\leftrightarrows_k\)	\(\leftrightarrow_k\)	\(\cong_{\mathrm{Kl}(\Ck)}\)	Coalgebras
Hypergraph comonad
MSO EF comonad

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)