The n-Category Café

Finite model theory is naturally related to complexity theory, as we may ask questions like what’s the time complexity to query a finite relational structure with a formula from some logic, and also the converse question—what kind of logic is needed to describe the algorithmic problems in a complexity class. For example, given a finite graph $G$, we may ask if it is possible to write a first-order logic formula $\varphi(u,v)$ using a relation symbol $E(x,y)$ saying there is an edge from $x$ to $y$, such that $\varphi(u,v)$ is satisfied precisely by vertices $u, v \in G$ that are connected by a path.

From a logical point of view, what makes finite model theory interesting is that some prominent techniques in model theory fail for finite models. In particular, compactness fails for finite model theory: a theory $T$ may not have a finite model even if all its finite sub-theories $S \subseteq T$ have finite models—consider e.g. $T = \left\{ \varphi_n \mid n \in \mathbb{N}\right\}$ where $\varphi_n$ asserts there are at least $n$ distinct elements.

Fortunately there are model-theoretic techniques remaining valid in the finite context. One of them is model-comparison games, which characterise logical equivalence of models, i.e. when two models satisfy exactly the same formulas of a logic.

Such logical equivalences are very useful for showing (in)expressivity of logics. For example, if we are able to show that two models $\mathcal{A}$ and $\mathcal{B}$ of a theory satisfy exactly the same formulas from first-order logic, but there is a semantic property $P$ (in the meta-theory) which $\mathcal{A}$ satisfies but $\mathcal{B}$ does not. Then we know the property $P$ necessarily cannot be expressed in first-order logic. This proof technique works for both finite and infinite models. In fact, using this technique one can show that connectivity of finite graphs cannot be expressed as a first-order logic formula with only the relation symbol $E(x,y)$ for edges.

Of course the logic equivalences for different logics need to be characterised by different games: first-order logic is characterised by Ehrenfeucht-Fraïssé games; the $k$-variable fragment of first-order logic is characterised by pebble games; modal logic is characterised by bisimulation games, and so on.

Despite being different, these games are structurally so similar that they almost begged to be unified. Their unification is eventually done by Abramsky and Shah (2018, 2021) in the categorical framework of game comonads. This two-part blog post aims to give a brief introduction to finite model theory and game comonads. This post will cover only a tiny part of this active research programme, but we will aim to exposit in a self-contained way the basics with some intuition that is hidden in the papers.

Basics of First-Order Logic

Let’s begin with a quick recap on classical first-order logic (FOL). A purely relational vocabulary $\sigma$ is a set of relation symbols $\left\{P_1,\dots,P_i,\dots\right\}$ where each relation symbol $P_i$ has an associated arity $n_i \in \mathbb{N}$. In this post we do not consider vocabularies with function symbols or constants since they can be alternatively modelled as relations with axioms asserting their functionality, which slightly makes our life easier.

The formulas $\varphi$ of FOL in a (purely relational) vocabulary $\sigma$ is inductively generated by the following grammar, where the meta-variable $x$ ranges over a countably infinite set of variables:

$$\begin{array}{rl} \varphi &::= x_1 = x_2 \ |\ P_i(x_1,\dots,x_{n_i}) \ |\ \top \ |\ \varphi_1 \wedge \varphi_2 \ |\ \bot \ | \ \varphi_1\vee \varphi_2 \ |\ \neg \varphi \ |\ \exists x. \varphi \ |\ \forall x. \varphi \end{array}$$

A set $T$ of closed formulas (i.e. formulas with no free variables) is called a theory.

We will only consider the classical semantics of FOL in the category of sets in this post. A $\sigma$-relational structure, or simply a $\sigma$-structure, $\mathcal{A} = \langle A, \langle P_i^A\rangle_{P_i \in \sigma}\rangle$ consists of a set $A$ and an $n_i$-ary relation $P^A_i \subseteq A^{n_i}$ on the set $A$ for each relation symbol $P_i \in \sigma$ of arity $n_i$.

A homomorphism of $\sigma$-structures from $\mathcal{A}$ to $\mathcal{B}$ is a function $h\colon A\to B$ on the underlying sets such that for each relation symbol $P_i$ in $\sigma$, we have $P_i^A(a_1,\dots,a_{n_i})$ implies $P_i^B(h(a_1),\dots,h(a_{n_i}))$ for all $a_1,\dots,a_{n_i}\in A$. Each vocabulary $\sigma$ thus yields a category $\mathcal{R}(\sigma)$ of $\sigma$-structures and homomorphisms.

Let $\varphi$ be a FOL formula (in the vocabulary $\sigma$) with $n$ free variables. The semantics of $\varphi$ in a $\sigma$-structure $\mathcal{A}$ is an $n$-ary relation $[\![\varphi]\!] \subseteq A^n$ on the set $A$. We will write $\mathcal{A} \models \varphi (\vec{a})$ when some $\vec{a} \in A^n$ is contained in $[\![\varphi]\!]$ and also write $\mathcal{A} \models \varphi$ when $\varphi$ is a closed formula and $\langle \rangle$ is in $[\![\varphi]\!] \subseteq A^0$. The relation $[\![\varphi]\!]$ is inductively defined on $\varphi$ as follows (we implicity treats $\vec{a} \in A^n$ as a function from the set of the $n$ free variables to the set $A$):

$$\begin{matrix} \mathcal{A}\models (x_i = x_j)(\vec{a}) &\iff& \vec{a}(x_i) = \vec{a}(x_j)\\ \mathcal{A}\models P_i(x_1,\dots,x_{n_i})(\vec{a}) &\iff& \langle \vec{a}(x_1),\dots,\vec{a}(x_{n_i})\rangle \in P_i^A\\ \mathcal{A}\models \top &\iff& true\\ \mathcal{A}\models (\varphi_1 \wedge \varphi_2)(\vec{a}) &\iff& \mathcal{A}\models \varphi_1(\vec{a}) \ \text{and}\ \mathcal{A}\models\varphi_2(\vec{a})\\ \mathcal{A}\models \bot &\iff& false\\ \mathcal{A}\models (\varphi_1 \vee \varphi_2)(\vec{a}) &\iff& \mathcal{A}\models \varphi_1(\vec{a}) \ \text{or}\ \mathcal{A}\models\varphi_2(\vec{a})\\ \mathcal{A}\models \neg\varphi(\vec{a}) &\iff& \mathcal{A}\models \varphi(\vec{a}) \ \text{does not hold}\\ \mathcal{A}\models (\exists y. \varphi)(\vec{a}) &\iff& \mathcal{A}\models \varphi(\vec{a}[y \mapsto a'])\ \text{for some }a'\in A\\ \mathcal{A}\models (\forall y. \varphi)(\vec{a}) &\iff& \mathcal{A}\models \varphi(\vec{a}[y \mapsto a'])\ \text{for all } a'\in A \end{matrix}$$ where $\vec{a}[y \mapsto a']$ is the function mapping $y$ to $a'$ and anything else $x$ to $\vec{a}(x)$.

Logical Equivalences and Ehrenfeucht-Fraïssé Games

As motivated earlier, we are interested in characterising when two models $\mathcal{A}$ and $\mathcal{B}$ of a relational vocabulary $\sigma$ satisfy exactly the same formulas, more precisely, when $\mathcal{A} \models \phi \iff \mathcal{B} \models \phi$ for all closed FOL formulas $\phi$ in the vocabulary $\sigma$. When it is the case, $\mathcal{A}$ and $\mathcal{B}$ are sometimes called elementarily equivalent.

An Example of Logical Equivalence

Let’s build up our intuition with a concrete example. Let $\sigma$ be the vocabulary with just one binary relation symbol $\leq$, and let $\mathcal{A}$ be the model $\left\{0, 1, \dots, 1000\right\}$ with $\leq$ being the usual linear order of natural numbers and similarly $\mathcal{B}$ be the model $\left\{0, 1, \dots, 1001\right\}$ with the same order. These two models are clearly different, and indeed they can be differentiated by a first-order logic formula in the vocabulary $\sigma$—the formula $$\varphi = \exists x_0\exists x_1\cdots\exists x_{1001}.\ \neg (x_0 = x_1) \wedge \dots \neg(x_i = x_j) \dots \neg (x_{1000} = x_{1001})$$ saying that there exist $1002$ different elements is satisfied by $\mathcal{B}$ but not by $\mathcal{A}$.

However, the formula $\varphi$ is a pretty big formula—it has 1002 quantifiers and 501501 clauses, so it is possible that small enough formulas cannot differentiate $\mathcal{A}$ and $\mathcal{B}$ since they are pretty similar (they are both linear orders). Let’s consider some formulas with just a few quantifiers:

• The vocabulary $\sigma = \left\{ \leq \right\}$ doesn’t have a constant, so there are no closed terms and thus no closed formulas other than $\bot$ and $\top$. Thus $\mathcal{A}$ and $\mathcal{B}$ agree on all formulas with 0 quantifiers.

• Consider formulas of the form $\exists x.\varphi(x)$ where $\varphi$ doesn’t have any quantifiers. We argue that $\mathcal{A} \models \exists x.\varphi(x)$ iff $\mathcal{B} \models \exists x.\varphi(x)$ as follows: supposing $\mathcal{A} \models \exists x.\varphi(x)$ holds, this means that there is some $a \in \mathcal{A}$ such that $\mathcal{A} \models \varphi(a)$, then we may choose any $b \in \mathcal{B}$, say $b = 0 \in \mathcal{B}$, making $\mathcal{B} \models \varphi(b)$ because the formula $\varphi$ is inductively built from the variable $x$, relations $\leq$, $=$, and propositional connectives; both $a \leq a$ and $b \leq b$ are true, so we can inductively show that $\varphi(a)$ and $\varphi(b)$ agree for all $\varphi$. Conversely, if $\mathcal{B} \models \exists x. \varphi(x)$ is witnessed by some $b$, we can always pick an arbitrary $a \in \mathcal{A}$ witnessing $\mathcal{A} \models \exists x. \varphi(x)$.

  Moreover, since the semantics of propositional connectives are defined compositionally, we can inductively show that $\mathcal{A}$ and $\mathcal{B}$ agree on all closed formulas built out of exactly one $\exists$ and $=$, $\neg$, $\wedge$, and $\vee$. Since we are considering classical logic, universal quantification $\forall x. \varphi(x)$ can be reduced to $\neg \exists x. \varphi(x)$, so $\mathcal{A}$ and $\mathcal{B}$ agree on it so we conclude that $\mathcal{A}$ and $\mathcal{B}$ agree on all FOL formulas with exactly one quanfier.

• This example gets interesting when we consider two nested quantifiers. Supposing $\psi = \exists x. \exists y. \varphi$ where $\varphi$ is quanfier-free, if $\mathcal{A} \models \psi$, there exist $a$ and $a' \in \mathcal{A}$ such that $\mathcal{A} \models \varphi (\langle a, a'\rangle)$. Then we can also choose any two elements $b, b' \in \mathcal{B}$ such that, importantly, (i) $b \leq b'$ iff $a \leq a'$, and (ii) $b = b'$ iff $a = a'$. This ensures $\mathcal{B} \models \varphi(\langle b, b'\rangle)$ since the atomic formulas in $\varphi$ are built from $\leq$, $=$, $x$ and $y$, on which $\mathcal{A}$ with the variable assignment $\langle x\mapsto a, y \mapsto a'\rangle$ and $\mathcal{B}$ with $\langle x\mapsto b, y \mapsto b'\rangle$ agree. Conversely, if $\mathcal{B} \models \psi$ witnessed by $b, b' \in \mathcal{B}$ we can also choose a matching pair $a, a' \in \mathcal{A}$ making $\mathcal{A} \models \psi$.

  Now suppose $\psi = \exists x. \forall y. \varphi$. Whenever $\mathcal{A} \models \psi$, there is some $a$ such that $\mathcal{A} \models \forall y.\varphi \langle x \mapsto a\rangle$. In this case we can also choose an element $b \in \mathcal{B}$ that mimics $a \in \mathcal{A}$: if $a$ is the bottom element $0$ in the structure $\mathcal{A}$, we let $b = 0$ as well; if $a$ is the top $1000$ in $\mathcal{A}$, we let $b$ be the top $1001$ in $\mathcal{B}$; otherwise we can choose an arbitrary $0 \lt b \lt 1001$. We then claim $\mathcal{B} \models \forall y. \varphi \langle x \mapsto b\rangle$ as well, because if there is some $b'$ making $\mathcal{B} \models \varphi \langle x\mapsto b, y \mapsto b'\rangle$ not hold, we can also find an $a'$ that is to $a$ in $\mathcal{A}$ as $b'$ is to $b$ in $\mathcal{B}$: precisely, if $b' = b$, we let $a' = a$; if $b' \lt b$, we let $a'$ be any element in $\mathcal{A}$ such that $a' \lt a$, and similarly for the case $b' \gt b$ (such a choice is always possible because earlier $a$ and $b$ are chosen to be at the same relative position). This choice of $a'$ entails $\mathcal{A} \models \varphi\langle x \mapsto a, y \mapsto a'\rangle$ not true, leading to a contradiction. Therefore $\mathcal{B} \models \psi$.

  By a symmetric argument, $\mathcal{B} \models \exists x. \forall y. \varphi$ implies $\mathcal{A} \models \exists x. \forall y. \varphi$ as well. Moreover, by the compositionality of the semantics of propositional connectives, the two paragraphs above imply that $\mathcal{A}$ and $\mathcal{B}$ agree on all FOL formulas with quantifiers are nested at most once.

Hopefully working through the example above reveals the intuition behind logical equivalence for FOL: two $\sigma$-structures $\mathcal{A}$ and $\mathcal{B}$ agree on a FOL formula $\varphi$ whenever a quantifier in $\varphi$ picks an element $x$ in $A$ or $B$, there is always an element $y$ in the other structure that “simulates the behaviour” of $x$ in the model.

The Ehrenfeucht-Fraïssé Game

The intuition is precisely formulated as Ehrenfeucht-Fraïssé (EF) games. Given two $\sigma$-structures $\mathcal{A}$ and $\mathcal{B}$ for any vocabulary $\sigma$ and a natural number $k$, the $k$-round EF game for $\mathcal{A}$ and $\mathcal{B}$ is a turn-based game between two players, called the spoiler and the duplicator. Roughly speaking, the goal of the spoiler is to point out the difference between $\mathcal{A}$ and $\mathcal{B}$ while the goal of the duplicator is to advocate that $\mathcal{A}$ and $\mathcal{B}$ are the same. The rules are very simple:

1. Movement: at each round, the spoiler picks an element from one of the structures and the duplicator must respond with an element from the other structure. For example, if the spoiler picks an element from the structure $\mathcal{A}$, then the duplicator must pick an element $b\in\mathcal{B}$.

2. Winning Condition: After $k$ rounds, the game state consists of $\vec{a} = (a_1,\dots,a_k)$ and $\vec{b} = (b_1,\dots,b_i)$ representing the elements chosen from each structure at each round. The duplicator wins this play if the mapping $a_i \mapsto b_i$ defines a partial isomorphism between $\mathcal{A}$ and $\mathcal{B}$, i.e., if the substructures of $\mathcal{A}$ and $\mathcal{B}$ generated by $\vec{a}$ and $\vec{b}$ are isomorphic. Otherwise, the spoiler has succeeded in showing the structures are different and wins.

If the duplicator can guarantee a win after $k$ rounds no matter how the spoiler plays, we say the duplicator has a $k$-round winning strategy.

The quantifier rank $\mathop{qr}(\varphi)$ of a FOL formula $\varphi$ is the depth of nesting of the quantifiers in $\varphi$: $$\begin{array}{rcll} \mathop{qr}(\varphi) &=& 0 &\text{for atomic}\ \varphi\\ \mathop{qr}(o(\varphi_1, \dots, \varphi_n)) &=& \max(\mathop{qr}(\varphi_1), \dots, \mathop{qr}(\varphi_n)) &\text{for propositional connectives}\ o\\ \mathop{qr}(Q x. \varphi) &=& 1 + \mathop{qr}(\varphi) &\text{for quantifiers}\ Q = \forall, \exists \end{array}$$

Theorem (Ehrenfeucht-Fraïssé). If the duplicator has a winning strategy for the $k$-round EF game for $\mathcal{A}$ and $\mathcal{B}$, $\mathcal{A}$ and $\mathcal{B}$ agree on all closed FOL formulas of quantifier-rank $k$. When the vocabulary $\sigma$ is finite, the converse is also true.

Proof sketch: Assuming a winning strategy for the duplicator, and let $\psi$ be any formula of quantifier rank $k$. Without loss of generality, we can assume $\psi = Q_{1} x_{1}.\cdots Q_k x_k.\varphi$ where $Q_i \in \left\{\forall, \exists\right\}$ are quantifiers and $\varphi$ is quantifier-free. We need to show $\mathcal{A} \models \psi \iff \mathcal{B} \models \psi$. As we demonstrated in the example above, we consider how $- \models \psi$ is defined inductively: if a quantifier $Q_i = \exists$ and one of $\mathcal{A}$ and $\mathcal{B}$ satisfies the formula, we use the winning strategy for the duplicator to pick a matching element in the other structure; if a quantifier $Q_i = \forall$ and one of $\mathcal{A}$ and $\mathcal{B}$ satisfies the formula, every counter-witness in the other structure leads to a counter-witness in this structure by the winning strategy of the duplicator, thus a contradiction.

The converse direction is also interesting and is not demonstrated in the example in the last section. We only give a rough sketch here and refer interested readers to Libkin (2004, section 3) for details.

Assuming that $\mathcal{A}$ and $\mathcal{B}$ agree on all FOL formulas of rank $k$, the duplicator’s strategy is that whenever the spoiler picks an element $a_i \in \mathcal{A}$ (or symmetrically $b_i \in \mathcal{B}$), the duplicator first constructs a FOL formula $\phi_{i}$ that “maximally describes the current board on $\mathcal{A}$”. Roughly speaking, $\phi_{i}$ is the conjunction of all formulas in the following set $$\left\{\psi \mid \mathop{qr}(\psi) = i - 1 \ \text{and}\ \mathcal{A} \models \psi\, \langle a_1, \dots, a_i\rangle\right\}$$ A priori, this set may have infinitely many formulas, but since there are only finitely many atomic formulas when $\sigma$ is finite, $\phi_{i}$ can be reduced to a finite formula using the rules of propositional connectives. With the formula $\phi_{i}$ in hand, the duplicator can use the fact that $$\mathcal{A} \models \exists x_i. \phi_{i}\langle x_1 \mapsto a_1, \dots, x_{i-1}\rangle \mapsto a_{i-1},$$ witnessed by $x_i \mapsto a_i$. Now using the assumption that $\mathcal{A}$ and $\mathcal{B}$ agree on FOL up to rank $k$ and the fact that $\exists x_i.\phi_i$ is of rank $i$, $\mathcal{B}$ has an element witnessing the truth of this formula as well, which is going to be the duplicator’s response. $\square$

EF games are very useful for showing inexpressivity results of FOL. Suppose we are interested in a property $P$ (in the meta-theory) on a class $M$ of $\sigma$-structures. If for every natural number $k$, we can find two models $\mathcal{A}_k, \mathcal{B}_k \in M$ such that

1. the duplicator has a winning strategy for the $k$-round EF game on $\mathcal{A}_k$ and $\mathcal{B}_k$, but
2. only one of $\mathcal{A}_k$ and $\mathcal{B}_k$ satisfy the property $P$,

Then by the EF theorem, the property $P$ cannot be expressed by a FOL formula, whatever the quantifier it has.

For example, using this technique, we can show that the evenness of finite linear orders is not expressible—there isn’t a FOL formula $\varphi$ in the vocabulary $\left\{\leq\right\}$ such that for every finite linear order $\mathcal{A} = \langle A, \leq^A\rangle$, $\mathcal{A} \models \varphi$ exactly when $a$ has an even number of elements. (Hint: we pick $\mathcal{A}_k$ and $\mathcal{B}_k$ to be the linear order of $2^k$ and $2^k + 1$ elements respectively and play the EF games.)