The n-Category Café

One-Way EF Games

Let’s warm up by recalling EF games and considering a simplified version of them.

Recall that a $k$-round EF game is parameterized by two $\sigma$-relational structures $\mathcal{A}$ and $\mathcal{B}$ for some relational vocabulary $\sigma$. The rule is that in every round $1 \leq i \leq k$, the spoiler picks either an element from $\mathcal{A}$ or an element from $\mathcal{B}$, and then the duplicator responds with an element from the other structure. The duplicator wins if after $k$-rounds, these elements form a partial isomorphism.

In the game the spoiler has the freedom in each round to pick the structure $\mathcal{A}$ or $\mathcal{B}$, so EF games are also sometimes called back-and-forth games. We can also consider the one-way variant of EF games from $\mathcal{A}$ to $\mathcal{B}$, where the spoiler can only pick elements $a_i$ from $\mathcal{A}$ (so the duplicator responds with elements $b_i$ from $\mathcal{B}$). Additionally, we weaken the winning condition for the duplicator to be $a_i \mapsto b_i$ forming a partial homomorphism from $\mathcal{A}$ to $\mathcal{B}$ (rather than a partial isomorphism).

It is not difficult to modify the Ehrenfeucht-Fraïssé theorem that we saw last time to show that such one-way EF games characterise the fragment of FOL that only uses $\exists$, $\wedge$, $\vee$, $\text{true}$, $\text{false}$. This fragment of FOL is known as existential-positive fragment of first-order logic or coherent logic.

Theorem (Existential Ehrenfeucht-Fraïssé). If the duplicator has a winning strategy for the $k$-round one-way EF game from $\mathcal{A}$ to $\mathcal{B}$, then $A \models \varphi$ implies $B \models \varphi$ for all closed formulas $\varphi$ of quantifier rank $k$ in the existential-positive fragment.

A consequence of the one-way EF games is that now a winning strategy for the duplicator can be thought of as a function from the half-board of $\mathcal{A}$-elements $\langle a_1, \cdots, a_i\rangle$ in each round $i$ to the duplicator’s response $b_i \in \mathcal{B}$, instead of a function from the whole board $\langle\langle a_1, \cdots, a_i\rangle, \langle b_1, \cdots, b_{i-1}\rangle\rangle$ to their response $b_i$. The reason is that the $\mathcal{B}$-elements $\langle b_1, \cdots, b_{i-1}\rangle$ were all picked by the duplicator themselves before, so the duplicator knows what they are, and they don’t have to be in the input to the duplicator’s winning strategy.

Write $A^{\leq k}$ for the set $\left\{\langle a_1, \cdots, a_i\rangle \in A^\ast \mid 1 \leq i \leq k\right\}$ of non-empty $A$-sequences of length at most $k$. Clearly, not every function $f : A^{\leq k} \to B$ is a valid winning strategy for the duplicator for the one-way EF game, since the duplicator has to make sure their responses $b_i$ maintain a partial homomorphism to the spoiler’s choices $a_i$.

More precisely, for all half-boards $\langle a_1, \cdots, a_i\rangle \in A^{\leq k}$, if some of its elements are related by a relation $P \in \sigma$ of arity $m$, i.e. $P^A(a_{j_1}, \dots, a_{j_m})$ holds for $1 \leq j_1, \dots, j_m \leq i$, the duplicator’s strategy $f : A^{\leq k} \to B$ must make $$P^B(f\;\langle a_1, \dots, a_{j_1}\rangle, \dots, f\;\langle a_1, \dots, a_{j_m}\rangle) \ \text{hold}.$$

The EF Game Comonad

Now we are ready to formulate EF games in a more categorical way using comonads. Recall that the Kleisli presentation a comonad $(G, \epsilon, (-)^\ast)$ on a category $\mathcal{C}$ is given by

• a map $G: \mathop{Obj}(\mathcal{C}) \to \mathop{Obj}(\mathcal{C})$,

• for all $A\in \mathcal{C}$, a counit $\epsilon_A: G A \to A$, and

• a co-extension operation $(-)^\ast$ that takes every morphism $f : G A \to B$ to a morphism $f^\ast: G A \to G B$

such that the following equations hold for all $f : G A \to B$ and $g : G B \to C$: $$\begin{array}{rcll} (g\circ {f^\ast})^\ast &=& g^\ast\circ f^\ast &: G A \to G C\\ \mathit{id}_{G A} &=& \epsilon_A^\ast &: G A \to G A\\ f &=& \epsilon_B\circ f^\ast &: G A \to B. \end{array}$$

Given any natural number $k$, the mapping from sets $A$ to sets $A^{\leq k}$ of non-empty $A$-sequences of length at most $k$ can be equipped with a comonad structure $E_k$ on $\mathbf{Set}$:

• $E_k A = A^{\leq k}$ for all sets $A$;

• $\epsilon_A \langle a_1, \dots, a_i\rangle = a_i$ extracts the last element of the sequence (which corresponds to the newest choice by the spoiler in the one-way EF game);

• for all $f: E_k A \to B$, the co-extension $f^\ast : E_k A \to E_k B$ is $$f^\ast\;\langle a_1, \ldots, a_i\rangle = \langle f \; \langle a_1\rangle,\ f \; \langle a_1,a_2\rangle,\ \dots, f \; \langle a_1, \ldots, a_i\rangle\rangle,$$ which intuitively means that the duplicator can recall their own historical moves on the half-board on $B$ given the spoiler’s half-board on $A$.

A co-Kleisli map $f : E_k A \to B$ for this comonad is then a function from half-boards of $A$-elements to responses in $B$, so $f$ encodes precisely a (not necessarily winning) strategy for the duplicator.

The way to formulate winning strategies is to lift the comonad $E_k$ on $\mathbf{Set}$ to a comonad $\mathbb{E}_k$ on the category $\mathcal{R}(\sigma)$ of $\sigma$-relational structures.

Definition (EF Comonad). The comonad $\mathbb{E}_k$ on $\mathcal{R}(\sigma)$ is defined as follows:

• The object mapping sends every $\sigma$-structure $\mathcal{A} = \langle{A, \{P^A\}_{P \in \sigma}}\rangle$ to the $\sigma$-structure $\mathbb{E}_k \mathcal{A} = \langle E_k A, \{P^{E_k A}\}_{P\in\sigma}\rangle$ whose underlying set is just $E_k A$, i.e. non-empty $A$-sequences of length at most $k$; for every relation symbol $P \in \sigma$ of arity $n$, its interpretation $P^{E_k A} \subseteq (E_k A)^n$ relates sequences $\langle s_1,\dots,s_n\rangle$ satisfying the following two conditions:

  1. for all $1 \leq i, j \leq n$, the sequence $s_i$ is a prefix of $s_j$ or $s_j$ is a prefix of $s_i$, and
  2. $\langle \epsilon_A(s_1), \dots, \epsilon_A(s_n)\rangle\in P^\mathcal{A}$.

• The counit $\epsilon_{\mathcal{A}} : \mathbb{E}_k \mathcal{A} \to \mathcal{A}$ and the co-extension $f^\ast : \mathbb{E}_k \mathcal{A} \to \mathbb{E}_k \mathcal{B}$ are the same as those of the comonad $E_k : \mathbf{Set} \to \mathbf{Set}$. It can be checked that they are valid morphisms in the category $\mathcal{R}(\sigma)$.

Co-Kleisli morphisms $\mathbb{E}_k \mathcal{A} \to \mathcal{B}$ are exactly winning strategies for the duplicator in the one-way EF game frome $\mathcal{A}$ to $\mathcal{B}$ (modulo one subtle problem that we will talk about later). Let’s gain some intuition by looking at a small example.

Let us have two $\sigma$-structures, $\mathcal{A}$ and $\mathcal{B}$, with underlying sets $A=\{a,b,c\}$ and $B=\{a',b',c',d'\}$ respectively, and let us play a 3-round one-way EF game. We will try to associate the objects of the comonad as we go: * The spoiler chooses $a\in A$. In response, the duplicator chooses $a' \in B$: $$\epsilon_A \langle a\rangle=a,\quad f \langle a\rangle=a',\quad f^\ast \langle a\rangle=\langle a'\rangle.$$

• The spoiler chooses $b\in A$. In response, the duplicator chooses $b'\in B$: $$\epsilon_A \langle a,b\rangle=b,\quad f \langle a,b\rangle=b',\quad f^\ast \langle a,b\rangle=\langle a',b'\rangle.$$

• The spoiler chooses $c\in A$. In response, the duplicator chooses $c'\in B$: $$\epsilon_A \langle a,b,c\rangle=c,\quad f \langle a,b,c\rangle=c',\quad f^\ast \langle a,b,c\rangle=\langle a',b',c'\rangle.$$

For intuition on how the EF comonad $\mathbb{E}_k$ acts on relations, let us look at the binary relation case. The general case has the same intuition, but with more terms.

Condition (1) of the above definition imposes that one sequence be a prefix of the other. In game terms, this amounts to that $s_1$ and $s_2$ can be stages of the same game play: either $s_1$ evolves to $s_2$ or $s_2$ evolves to $s_1$.

Condition (2) says that two sequences $s_1$ and $s_2$ are related iff their last elements are related. Since under Condition (1), $s_1$ and $s_2$ are two stages of the same play, so $s_1$ and $s_2$ being related mean precisely that two elements in a game are related.

Let us go back to our earlier example with our $\sigma$-structures $A=\{a,b,c\}$ and $B=\{a',b',c',d'\}$, and suppose there is binary relation symbol $\leq$ in $\sigma$ whose interpretation in $A$ and $B$ are the alphabetical order $\leq$. Then, we can say that $\langle a,b\rangle \leq^{E_k A} \langle a,b,c\rangle$, because on one hand both sequences start in the same way (this game has started with the spoiler playing $a$ and then $b$), and on the other hand $b\leq c$ in the alphabetical order.

Now the intuition behind the comonad $\mathbb{E}_k$ might be clearer: in the $\sigma$-relational structure $\mathbb{E}_k\mathcal{A}$, some sequences $s_1, \dots, s_n$ are related means precisely that there is a game play for which $s_1, \dots, s_n$ are the spoiler’s half-boards on $\mathcal{A}$ in certain rounds, and the spoiler’s choices $\epsilon(s_1), \dots, \epsilon(s_n)$ are related by some relation in $\mathcal{A}$. Therefore, a $\sigma$-structure homomorphism $\mathbb{E}_k \mathcal{A} \to \mathcal{B}$ is a winning strategy for the duplicator.

There is one problem though: we have lifted all relations $P \in \sigma$ on $\mathcal{A}$ to $\mathbb{E}_k \mathcal{A}$, but there is a special built-in relation in FOL—the equality $x = y$. The one-way EF game asks that after every round, the chosen $\mathcal{A}$-elements and the chosen $\mathcal{B}$-elements form a partial isomorphism, so if the spoiler chooses the same element $a \in \mathcal{A}$ in two rounds, the duplicator must respond with the same elements as well. Otherwise it won’t be a partial isomorphism. However, this requirement is not captured by co-Kleisli morphisms $f : \mathbb{E}_k \mathcal{A} \to \mathcal{B}$, since e.g. $\langle a\rangle$ and $\langle a, b, a\rangle$ are different elements of $\mathbb{E}_k \mathcal{A}$, $f$ do not need to map them to the same response.

This motivates us to consider what is called I-morphisms, which are coKleisli morphisms $f : \mathbb{E}_k \mathcal{A} \to \mathcal{B}$ such that $f(s_1) = f(s_2)$ whenever $s_1$ is a prefix of $s_2$ and $\epsilon(s_1) = \epsilon(s_2)$. (There is an alternative definition of I-morphisms using relative comonads, but the direct definition suffices for our purposes in this post.)

Theorem. There is an winning strategy for the duplicator in the $k$-round one-way EF game from $\mathcal{A}$ to $\mathcal{B}$ if and only if there is an I-morphism $f : \mathbb{E}_k \mathcal{A} \to \mathcal{B}$.

Since $k$-round one-way EF games characterise logical refinement of existential-positive FOL, a direct corollary is that two $\sigma$-structure $\mathcal{A}$ and $\mathcal{B}$ agree on all closed existential-positive FOL formula $\varphi$ of rank $k$ if and only if there are two I-morphisms $\mathbb{E}_k \mathcal{A} \to \mathcal{B}$ and $\mathbb{E}_k \mathcal{B} \to \mathcal{A}$.

Back-and-Forth Games

If we ask to have two coKleisli morphisms but nothing else of them, we get the existential-positive fragment, but recall our original goal was to characterise FOL and EF games. What if we ask for the morphisms to have a relationship between them? What if, as we usually do, we ask them to be inverses of each other?

It turns out to characterise the logical equivalence of FOL augmented with counting quantifiers $\exists_{\leq n}x. \varphi$ and $\exists_{\geq n} x. \varphi$, whose semantics is that there exist at most $n$, and respectively at least $n$, elements $a \in \mathcal{A}$ making $\varphi$ true.

Proposition. Two finite $\sigma$-structures $\mathcal{A}$ and $\mathcal{B}$ agree on all closed formulas on FOL with counting quantifiers if and only if there is a pair of $I$-morphisms $f : \mathbb{E}_k\mathcal{A} \to \mathcal{B}$ and $g : \mathbb{E}_k\mathcal{B} \to \mathcal{A}$ that are mutual inverses (in the co-Kleisli category of $\mathbb{E}_k$).

So if we don’t ask anything from the homomorphisms we get too little; but if we ask for them to be an isomorphism we go overboard and get too much. Can we find a middle ground?

Yes, the key intuition for this is that the duplicator can play the back-and-forth game like a one-way game when the spoiler keeps choosing elements from one structure, but the duplicator must have a plan B in mind in case the spoiler switches to choosing elements from the other structure in the next round.

This motivates what is called a locally invertible pair. Given two $\sigma$-structure $\mathcal{A}$ and $\mathcal{B}$ and a natural number $k$ as usual, a locally invertible pair $\langle F,G\rangle$ consists of a set $F$ of co-Kleisli I-morphisms $\mathbb{E}_k \mathcal{A} \to \mathcal{B}$ and a set $G$ of co-Kleisli I-morphisms $\mathbb{E}_k \mathcal{B} \to \mathcal{A}$ such that

1. for all $f \in F$ and $s \in \mathbb{E}_k \mathcal{A}$, there is some $g_{f,s} \in G$ with $g_{f,s}^\ast (f^\ast(s)) = s$, and
2. for all $g \in G$ and $t \in \mathbb{E}_k \mathcal{B}$, there is some $f_{g,t} \in F$ with $f_{g,t}^\ast (g^\ast(t)) = t$.

Theorem. The duplicator has a winning strategy for the $k$-round EF game on $\mathcal{A}$ and $\mathcal{B}$ if and only if there is a non-empty locally invertible pair $\langle F,G\rangle$.

Proof. Assuming a non-empty locally invertible pair $\langle F,G\rangle$, the duplicator has the following strategy such that the chosen elements $s_i \in A^i$ and $t_i \in B^i$ after round $i$ satisfy the condition $$\phi_i = \exists f_i \in F. \exists g_i \in G. (s_i, t_i) = (s_i, f^\ast s_i) = (g^\ast t_i, t_i).$$ 1. In round $1$, if the spoiler chooses an element $a_1 \in A$, the duplicator can pick an arbitrary $f \in F$ and respond with $f \, \langle a_1\rangle \in B$. The condition $\phi_1$ is witnessed by $f_1 = f$ and $g_1 = g_{f, \langle a_1\rangle}$ given by the definition of locally invertible pairs. If the spoiler chooses an element $b_1 \in B$, the argument is the same.

1. In round $i+1$, if the spoiler chooses an element $a_{i+1}$, the duplicator responds with $b_{i+1} = f_i\,\langle a_1, \dots, a_{i+1}\rangle$. The condition $\phi_{i+1}$ is then witnessed by $f_{i+1} = f_i$ and $g_{i+1} = g_{f_i, \langle a_1, \dots, a_{i+1}\rangle}$.

After $k$-rounds, $\phi_k$ is true and it implies that $\langle a_1, \dots, a_k\rangle$ and $\langle b_1, \dots, b_k\rangle$ are a partial isomorphism because $f_k$ and $g_k$ are coKleisli morphisms $\mathbb{E}_k \mathcal{A} \to \mathcal{B}$ and $\mathbb{E}_k \mathcal{B} \to \mathcal{A}$.

For the other direction, assuming the duplicator has a winning strategy, let $\Phi \subseteq A^{\leq k} \times B^{\leq k}$ be the set of all possible game states in each round following the winning strategy. The locally invertible pair is $$\begin{array}{l} &F = \left\{f : \mathbb{E}_k \mathcal{A} \to \mathcal{B} \mid \forall s \in \mathbb{E}_k \mathcal{A}. (s, f^\ast s) \in \Psi\right\}, \\ &G = \left\{g : \mathbb{E}_k \mathcal{B} \to \mathcal{A} \mid \forall t \in \mathbb{E}_k \mathcal{B}. (g^\ast t, t) \in \Psi\right\}. \end{array}$$

First we argue that for all $(s,t) \in \Psi$, (i) $\exists f_{s,t} \in F. f_{s,t}^\ast s = t$ and (ii) $\exists g_{s,t} \in G. g_{s,t}^\ast t = s$. To show (i) (and symmetrically for (ii)) we construct $f_{s,t}$ as follows: for every $s'\in \mathbb{E}_k \mathcal{A}$, let $m$ be the length of the longest common prefix of $s$ and $s'$. We consider the game play where in the first $m$-rounds the spoiler and the duplicator play in the way as $(s,t) \in \Phi$, and afterwards, the spoiler always chooses elements according to $s'$ and the duplicator follows the winning strategy. The last $\mathcal{B}$-element picked in this game play is the value of the function $f_{s,t}$ at $s'$.

Now we can see $\langle F,G\rangle$ defined as above is a locally invertible pair, for every $g \in G$ and $t \in \mathbb{E}_k \mathcal{B}$, $(g^\astt, t)$ is in $\Phi$, and thus by (i) there exists $f_{g^\ast t,t} \in F$ with $f_{g^\ast t,t}^\ast(g^\ast t) = t$. The symmetric condition for $F$ similarly holds. $\square$

Wrap-up

In Part 1 of the post, we have seen how logical equivalences for first-order logic can be characterised by combinatorial games, and how this can be used for showing inexpressivity results of first-order logic. In Part 2 of this post, we have seen how such games can be formulated in a concise way using comonads.

As an active research subject, what we didn’t say about game comonads in this blog post is a lot:

1. Many other logics have model comparison games and have received a comonadic treatment, including modal logics (Abramsky and Shah 2021), the $k$-variable fragment of FOL (Abramsky, Dawar and Wang 2017), guarded logics (Abramsky and Marsden 2021), monadic second-order logic (Jakl, Marsden and Shah 2022), finite-variable logics with generalised quantifiers (Conghaile and Dawar 2021).

2. Coalgebras of game comonads usually reveal interesting information about the combinatorial structure of finite structures. For example, $\mathbb{E}_k$-coalgebras $\mathcal{A} \to \mathbb{E}_k \mathcal{A}$ are in bijection with forest covers of height $\leq k$ for the Gaifman graph of $\mathcal{A}$.

3. Back-and-forth games can be defined in an axiomatic way (Abramsky and Reggio 2021).

Moreover, we have only considered the classical semantics of FOL in sets, so a natural question is how finite model theory interacts with the various notions of finiteness in constructive mathematics and the general categorical semantics of FOL in hyperdoctrines.