Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

September 11, 2023

Finite Model Theory and Game Comonads: Part 2

Posted by Emily Riehl

guest post by Elena Dimitriadis, Richie Yeung, Tyler Hanks, and Zhixuan Yang

In the Part 1 of this post, we saw how logical equivalences of first-order logic (FOL) can be characterised by a combinatory game, but there are still a few unsatisfactory aspects of the formulation of EF games in Part 1:

  1. The game was formulated in a slightly informal way, delegating the precise meaning of “turns”, “moves”, “wins” to our common sense.

  2. There are variants of the EF game that characterise logical equivalences for other logics, but these closely related games are defined ad hoc rather than as instances of one mathematical framework.

  3. We have confined ourselves entirely to the classical semantics of FOL in the category of sets, rather than general categorical semantics.

So you, a patron of the n-Category Café, must be thinking that category theory is perfect for addressing these problems! This is exactly what we are gonna talk about today—the framework of game comonads that was introduced by Abramsky, Dawar and Wang (2017) and Abramsky and Shah (2018).

(We will not address the third point above in this post though, but hopefully the reader will agree that what we talk about below is a useful first step towards model comparison games for general categorical logic.)

One-Way EF Games

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

Recall that a kk-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 1ik1 \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 kk-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 ia_i from 𝒜\mathcal{A} (so the duplicator responds with elements b ib_i from \mathcal{B}). Additionally, we weaken the winning condition for the duplicator to be a ib ia_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, true\text{true}, false\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 kk-round one-way EF game from 𝒜\mathcal{A} to \mathcal{B}, then AφA \models \varphi implies BφB \models \varphi for all closed formulas φ\varphi of quantifier rank kk 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 a 1,,a i\langle a_1, \cdots, a_i\rangle in each round ii to the duplicator’s response b ib_i \in \mathcal{B}, instead of a function from the whole board a 1,,a i,b 1,,b i1\langle\langle a_1, \cdots, a_i\rangle, \langle b_1, \cdots, b_{i-1}\rangle\rangle to their response b ib_i. The reason is that the \mathcal{B}-elements b 1,,b i1\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 kA^{\leq k} for the set {a 1,,a iA *1ik}\left\{\langle a_1, \cdots, a_i\rangle \in A^\ast \mid 1 \leq i \leq k\right\} of non-empty AA-sequences of length at most kk. Clearly, not every function f:A kBf : 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 ib_i maintain a partial homomorphism to the spoiler’s choices a ia_i.

More precisely, for all half-boards a 1,,a iA k\langle a_1, \cdots, a_i\rangle \in A^{\leq k}, if some of its elements are related by a relation PσP \in \sigma of arity mm, i.e. P A(a j 1,,a j m)P^A(a_{j_1}, \dots, a_{j_m}) holds for 1j 1,,j mi1 \leq j_1, \dots, j_m \leq i, the duplicator’s strategy f:A kBf : A^{\leq k} \to B must make P B(fa 1,,a j 1,,fa 1,,a j m)hold. 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,ϵ,() *)(G, \epsilon, (-)^\ast) on a category 𝒞\mathcal{C} is given by

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

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

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

such that the following equations hold for all f:GABf : G A \to B and g:GBCg : G B \to C: (gf *) * = g *f * :GAGC id GA = ϵ A * :GAGA f = ϵ Bf * :GAB. \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 kk, the mapping from sets AA to sets A kA^{\leq k} of non-empty AA-sequences of length at most kk can be equipped with a comonad structure E kE_k on Set\mathbf{Set}:

  • E kA=A kE_k A = A^{\leq k} for all sets AA;

  • ϵ Aa 1,,a i=a i\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 kABf: E_k A \to B, the co-extension f *:E kAE kBf^\ast : E_k A \to E_k B is f *a 1,,a i=fa 1,fa 1,a 2,,fa 1,,a i,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 BB given the spoiler’s half-board on AA.

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

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

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

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

    1. for all 1i,jn1 \leq i, j \leq n, the sequence s is_i is a prefix of s js_j or s js_j is a prefix of s is_i, and
    2. ϵ A(s 1),,ϵ A(s n)P 𝒜\langle \epsilon_A(s_1), \dots, \epsilon_A(s_n)\rangle\in P^\mathcal{A}.
  • The counit ϵ 𝒜:𝔼 k𝒜𝒜\epsilon_{\mathcal{A}} : \mathbb{E}_k \mathcal{A} \to \mathcal{A} and the co-extension f *:𝔼 k𝒜𝔼 kf^\ast : \mathbb{E}_k \mathcal{A} \to \mathbb{E}_k \mathcal{B} are the same as those of the comonad E k:SetSetE_k : \mathbf{Set} \to \mathbf{Set}. It can be checked that they are valid morphisms in the category (σ)\mathcal{R}(\sigma).

Co-Kleisli morphisms 𝔼 k𝒜\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}A=\{a,b,c\} and B={a,b,c,d}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 aAa\in A. In response, the duplicator chooses aBa' \in B: ϵ Aa=a,fa=a,f *a=a.\epsilon_A \langle a\rangle=a,\quad f \langle a\rangle=a',\quad f^\ast \langle a\rangle=\langle a'\rangle.

  • The spoiler chooses bAb\in A. In response, the duplicator chooses bBb'\in B: ϵ Aa,b=b,fa,b=b,f *a,b=a,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 cAc\in A. In response, the duplicator chooses cBc'\in B: ϵ Aa,b,c=c,fa,b,c=c,f *a,b,c=a,b,c.\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 𝔼 k\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 1s_1 and s 2s_2 can be stages of the same game play: either s 1s_1 evolves to s 2s_2 or s 2s_2 evolves to s 1s_1.

Condition (2) says that two sequences s 1s_1 and s 2s_2 are related iff their last elements are related. Since under Condition (1), s 1s_1 and s 2s_2 are two stages of the same play, so s 1s_1 and s 2s_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}A=\{a,b,c\} and B={a,b,c,d}B=\{a',b',c',d'\}, and suppose there is binary relation symbol \leq in σ\sigma whose interpretation in AA and BB are the alphabetical order \leq. Then, we can say that a,b E kAa,b,c\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 aa and then bb), and on the other hand bcb\leq c in the alphabetical order.

Now the intuition behind the comonad 𝔼 k\mathbb{E}_k might be clearer: in the σ\sigma-relational structure 𝔼 k𝒜\mathbb{E}_k\mathcal{A}, some sequences s 1,,s ns_1, \dots, s_n are related means precisely that there is a game play for which s 1,,s ns_1, \dots, s_n are the spoiler’s half-boards on 𝒜\mathcal{A} in certain rounds, and the spoiler’s choices ϵ(s 1),,ϵ(s n)\epsilon(s_1), \dots, \epsilon(s_n) are related by some relation in 𝒜\mathcal{A}. Therefore, a σ\sigma-structure homomorphism 𝔼 k𝒜\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σP \in \sigma on 𝒜\mathcal{A} to 𝔼 k𝒜\mathbb{E}_k \mathcal{A}, but there is a special built-in relation in FOL—the equality x=yx = 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𝒜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:𝔼 k𝒜f : \mathbb{E}_k \mathcal{A} \to \mathcal{B}, since e.g. a\langle a\rangle and a,b,a\langle a, b, a\rangle are different elements of 𝔼 k𝒜\mathbb{E}_k \mathcal{A}, ff 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:𝔼 k𝒜f : \mathbb{E}_k \mathcal{A} \to \mathcal{B} such that f(s 1)=f(s 2)f(s_1) = f(s_2) whenever s 1s_1 is a prefix of s 2s_2 and ϵ(s 1)=ϵ(s 2)\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 kk-round one-way EF game from 𝒜\mathcal{A} to \mathcal{B} if and only if there is an I-morphism f:𝔼 k𝒜f : \mathbb{E}_k \mathcal{A} \to \mathcal{B}.

Since kk-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 kk if and only if there are two I-morphisms 𝔼 k𝒜\mathbb{E}_k \mathcal{A} \to \mathcal{B} and 𝔼 k𝒜\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 nx.φ\exists_{\leq n}x. \varphi and nx.φ\exists_{\geq n} x. \varphi, whose semantics is that there exist at most nn, and respectively at least nn, elements a𝒜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 II-morphisms f:𝔼 k𝒜f : \mathbb{E}_k\mathcal{A} \to \mathcal{B} and g:𝔼 k𝒜g : \mathbb{E}_k\mathcal{B} \to \mathcal{A} that are mutual inverses (in the co-Kleisli category of 𝔼 k\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 kk as usual, a locally invertible pair F,G\langle F,G\rangle consists of a set FF of co-Kleisli I-morphisms 𝔼 k𝒜\mathbb{E}_k \mathcal{A} \to \mathcal{B} and a set GG of co-Kleisli I-morphisms 𝔼 k𝒜\mathbb{E}_k \mathcal{B} \to \mathcal{A} such that

  1. for all fFf \in F and s𝔼 k𝒜s \in \mathbb{E}_k \mathcal{A}, there is some g f,sGg_{f,s} \in G with g f,s *(f *(s))=sg_{f,s}^\ast (f^\ast(s)) = s, and
  2. for all gGg \in G and t𝔼 kt \in \mathbb{E}_k \mathcal{B}, there is some f g,tFf_{g,t} \in F with f g,t *(g *(t))=tf_{g,t}^\ast (g^\ast(t)) = t.

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

Proof. Assuming a non-empty locally invertible pair F,G\langle F,G\rangle, the duplicator has the following strategy such that the chosen elements s iA is_i \in A^i and t iB it_i \in B^i after round ii satisfy the condition ϕ i=f iF.g iG.(s i,t i)=(s i,f *s i)=(g *t i,t i). \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 11, if the spoiler chooses an element a 1Aa_1 \in A, the duplicator can pick an arbitrary fFf \in F and respond with fa 1Bf \, \langle a_1\rangle \in B. The condition ϕ 1\phi_1 is witnessed by f 1=ff_1 = f and g 1=g f,a 1g_1 = g_{f, \langle a_1\rangle} given by the definition of locally invertible pairs. If the spoiler chooses an element b 1Bb_1 \in B, the argument is the same.

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

After kk-rounds, ϕ k\phi_k is true and it implies that a 1,,a k\langle a_1, \dots, a_k\rangle and b 1,,b k\langle b_1, \dots, b_k\rangle are a partial isomorphism because f kf_k and g kg_k are coKleisli morphisms 𝔼 k𝒜\mathbb{E}_k \mathcal{A} \to \mathcal{B} and 𝔼 k𝒜\mathbb{E}_k \mathcal{B} \to \mathcal{A}.

For the other direction, assuming the duplicator has a winning strategy, let ΦA k×B k\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 F={f:𝔼 k𝒜s𝔼 k𝒜.(s,f *s)Ψ}, G={g:𝔼 k𝒜t𝔼 k.(g *t,t)Ψ}. \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)Ψ(s,t) \in \Psi, (i) f s,tF.f s,t *s=t\exists f_{s,t} \in F. f_{s,t}^\ast s = t and (ii) g s,tG.g s,t *t=s\exists g_{s,t} \in G. g_{s,t}^\ast t = s. To show (i) (and symmetrically for (ii)) we construct f s,tf_{s,t} as follows: for every s𝔼 k𝒜s'\in \mathbb{E}_k \mathcal{A}, let mm be the length of the longest common prefix of ss and ss'. We consider the game play where in the first mm-rounds the spoiler and the duplicator play in the way as (s,t)Φ(s,t) \in \Phi, and afterwards, the spoiler always chooses elements according to ss' 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,tf_{s,t} at ss'.

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


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 kk-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, 𝔼 k\mathbb{E}_k-coalgebras 𝒜𝔼 k𝒜\mathcal{A} \to \mathbb{E}_k \mathcal{A} are in bijection with forest covers of height k\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.

Posted at September 11, 2023 3:58 PM UTC

TrackBack URL for this Entry:

0 Comments & 0 Trackbacks

Post a New Comment