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.

One way of obtaining new comonads from the old one is by considering their linear variants.

Comonad	\(\Ck\)	Logic \(\mathcal L\)	\(\leftrightarrows_k\)	\(\leftrightarrow_k\)	\(\cong_{\mathrm{Kl}(\Ck)}\)	Coalgebras
Pebble Relation	\(\mathbb {PR}_k\)	\(k\)-variable logic, restricted \(\wedge\)	✓	??	✓ (I)	path width \({<} k\)
Linear EF	\(\mathbb {E}^L_k\)	quantifier rank \(\leq k\), restricted \(\wedge\) ?	??	??	??	linear tree depth \({<} k\) ?
Linear modal (*)	\(\mathbb {M}^L_k\)	??	??	??	??	??

(Although, most of the table is not filled in, it is expected to work out as usually)

The other way of creating new comonads from the old ones is by considering the reachability versions of the old ones. This is similar to how we might think of \(\mathbb M_k\) as the reachability variant of the pointed version of \(\mathbb E_k\).

These include the "immediate successor" variant of Mk due to Gabriel Goren and Santiago Figueira, and also Tom Paine's locality comonad.

Comonad	\(\Ck\)	Logic \(\mathcal L\)	\(\leftrightarrows_k\)	\(\leftrightarrow_k\)	\(\cong_{\mathrm{Kl}(\Ck)}\)	Coalgebras
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

And the last technique is obtaining new comonads as quotient comonads of the previously described comonad.

Comonad	\(\Ck\)	Logic \(\mathcal L\)	\(\leftrightarrows_k\)	\(\leftrightarrow_k\)	\(\cong_{\mathrm{Kl}(\Ck)}\)	Coalgebras
"Hella's game"	\(\mathbb H_{n,k}\) [1]	extension of \(\mathcal L^k\) with generalised quantifiers	✓	✓	✓	\(n\)-ary generalised tree width \({\leq} k\)
Hybrid comonad	\(\mathbb{HY}_{k}\)	modal depth \(\leq k\) for hybrid logic	✓	✓	✓	generated tree-depth

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. This is a useful technique when trying to enrich the expressibility of the logic by using translation functors. See Comonads and logic for details.

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