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 \(\Ck A \leftarrow 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.

Direct modifications of the previous comonads include

• \(\mathbb E_\omega\), \(\mathbb P_\omega\), \(\mathbb M_\omega\) which are like the previous comonads but with infinite resource bound \(k\)
• \(\mathbb P_{n,k}\) which is like \(\mathbb P_k\) but restricted to sequences of length \(\leq n\)
• \(\sum_{k=1}^\infty \mathbb E_k\) which is a coproduct of comonads, capturing \(FO\) (unlike \(\mathbb E_\omega\) which captures \(FO\) with infinite conjunctions and disjunctions)
• \(\mathbb E_k\), \(\mathbb P_k\), etc. can be defined over the categories with constants/pointed structures, by requiring that the first element(s) of every word is according to the constants/selected point

A non-trivial way of obtaining new comonads from the old one is by considering their linear variants (see references in Linear arboreal categories).

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\)	linear modal logic	✓	✓	✓	??

(Although, parts of the table are 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\).

Comonad	\(\Ck\)	Logic \(\mathcal L\)	\(\leftrightarrows_k\)	\(\leftrightarrow_k\)	\(\cong_{\mathrm{Kl}(\Ck)}\)	Coalgebras
Hybrid (Temporal) comonad (*)	\(\mathbb{HT}_{k}\)	modal depth \(\leq k\) for hybrid logic	✓	✓	✓	generated tree-depth
PPML Comonad (*)		Path Predicate Modal Logic	✓	✓ (modified)	??	as in \(\mathbb M_k\), but with relations only along paths
Reachability	\(\mathbb{R}_{k}\)

And the last technique is obtaining new comonads as quotient comonads of other comonads.

Comonad	\(\Ck\)	Logic \(\mathcal L\)	\(\leftrightarrows_k\)	\(\leftrightarrow_k\)	\(\cong_{\mathrm{Kl}(\Ck)}\)	Coalgebras
Hella comonad	\(\mathbb H_{n,k}\)	\(\mathcal L^k\) + all \(n\)-ary 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

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.

\[ \xymatrix{ \mathcal Rel(\sigma) \ar[r]^t & \mathcal A \ar@(rd,ru)[]_{\Ck} } \]

The intuition is that we have a translation functor \(t\) to a potentially vastly different category \(\mathcal A\) with an (arboreal) comonad that we use to capture logic the same way the translation to the setting with \(I\)-morphisms is used to capture equality in the logic.

Comonad	\(\Ck\)	Category \(\mathcal A\)	Logic \(\mathcal L\)	\(\leftrightarrows_k\)	\(\leftrightarrow_k\)	\(\cong_{\mathrm{Kl}(\Ck)}\)	Coalgebras
Hypergraph comonad
MSO EF comonad	\(\mathbb E_k\)	many-sorted structures	\(MSO_k\)	✓	✓	??
Description Logic	\(\mathbb M_k\)
Local invariant