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 8, 2023

Finite Model Theory and Game Comonads: Part 1

Posted by Emily Riehl

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

Finite model theory (Libkin 2004) studies finite models of logics. Its main motivation comes from computer science: a finite relational structure, i.e. a finite set AA with a finite set of relations on AA, is essentially a database in the sense of good old SQL tables, and a logic formula φ\varphi with nn free variables is understood as a query to the database that selects all nn-tuples of AA that satisfy the formula φ\varphi.

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 GG, we may ask if it is possible to write a first-order logic formula φ(u,v)\varphi(u,v) using a relation symbol E(x,y)E(x,y) saying there is an edge from xx to yy, such that φ(u,v)\varphi(u,v) is satisfied precisely by vertices u,vGu, 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 TT may not have a finite model even if all its finite sub-theories STS \subseteq T have finite models—consider e.g. T={φ nn}T = \left\{ \varphi_n \mid n \in \mathbb{N}\right\} where φ n\varphi_n asserts there are at least nn 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 PP (in the meta-theory) which 𝒜\mathcal{A} satisfies but \mathcal{B} does not. Then we know the property PP 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)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 kk-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 {P 1,,P i,}\left\{P_1,\dots,P_i,\dots\right\} where each relation symbol P iP_i has an associated arity n in_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 xx ranges over a countably infinite set of variables:

φ ::=x 1=x 2|P i(x 1,,x n i)||φ 1φ 2||φ 1φ 2|¬φ|x.φ|x.φ \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 TT 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, 𝒜=A,P i A P iσ\mathcal{A} = \langle A, \langle P_i^A\rangle_{P_i \in \sigma}\rangle consists of a set AA and an n in_i-ary relation P i AA n iP^A_i \subseteq A^{n_i} on the set AA for each relation symbol P iσP_i \in \sigma of arity n in_i.

A homomorphism of σ\sigma-structures from 𝒜\mathcal{A} to \mathcal{B} is a function h:ABh\colon A\to B on the underlying sets such that for each relation symbol P iP_i in σ\sigma, we have P i A(a 1,,a n i)P_i^A(a_1,\dots,a_{n_i}) implies P i B(h(a 1),,h(a n i))P_i^B(h(a_1),\dots,h(a_{n_i})) for all a 1,,a n iAa_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 nn free variables. The semantics of φ\varphi in a σ\sigma-structure 𝒜\mathcal{A} is an nn-ary relation [[φ]]A n[\![\varphi]\!] \subseteq A^n on the set AA. We will write 𝒜φ(a)\mathcal{A} \models \varphi (\vec{a}) when some aA n\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 [[φ]]A 0[\![\varphi]\!] \subseteq A^0. The relation [[φ]][\![\varphi]\!] is inductively defined on φ\varphi as follows (we implicity treats aA n\vec{a} \in A^n as a function from the set of the nn free variables to the set AA):

𝒜(x i=x j)(a) a(x i)=a(x j) 𝒜P i(x 1,,x n i)(a) a(x 1),,a(x n i)P i A 𝒜 true 𝒜(φ 1φ 2)(a) 𝒜φ 1(a)and𝒜φ 2(a) 𝒜 false 𝒜(φ 1φ 2)(a) 𝒜φ 1(a)or𝒜φ 2(a) 𝒜¬φ(a) 𝒜φ(a)does not hold 𝒜(y.φ)(a) 𝒜φ(a[ya])for some aA 𝒜(y.φ)(a) 𝒜φ(a[ya])for all aA\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 a[ya]\vec{a}[y \mapsto a'] is the function mapping yy to aa' and anything else xx to a(x)\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 {0,1,,1000}\left\{0, 1, \dots, 1000\right\} with \leq being the usual linear order of natural numbers and similarly \mathcal{B} be the model {0,1,,1001}\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 φ=x 0x 1x 1001.¬(x 0=x 1)¬(x i=x j)¬(x 1000=x 1001) \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 10021002 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 x.φ(x)\exists x.\varphi(x) where φ\varphi doesn’t have any quantifiers. We argue that 𝒜x.φ(x)\mathcal{A} \models \exists x.\varphi(x) iff x.φ(x)\mathcal{B} \models \exists x.\varphi(x) as follows: supposing 𝒜x.φ(x)\mathcal{A} \models \exists x.\varphi(x) holds, this means that there is some a𝒜a \in \mathcal{A} such that 𝒜φ(a)\mathcal{A} \models \varphi(a), then we may choose any bb \in \mathcal{B}, say b=0b = 0 \in \mathcal{B}, making φ(b)\mathcal{B} \models \varphi(b) because the formula φ\varphi is inductively built from the variable xx, relations \leq, ==, and propositional connectives; both aaa \leq a and bbb \leq b are true, so we can inductively show that φ(a)\varphi(a) and φ(b)\varphi(b) agree for all φ\varphi. Conversely, if x.φ(x)\mathcal{B} \models \exists x. \varphi(x) is witnessed by some bb, we can always pick an arbitrary a𝒜a \in \mathcal{A} witnessing 𝒜x.φ(x)\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 x.φ(x)\forall x. \varphi(x) can be reduced to ¬x.φ(x)\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 ψ=x.y.φ\psi = \exists x. \exists y. \varphi where φ\varphi is quanfier-free, if 𝒜ψ\mathcal{A} \models \psi, there exist aa and a𝒜a' \in \mathcal{A} such that 𝒜φ(a,a)\mathcal{A} \models \varphi (\langle a, a'\rangle). Then we can also choose any two elements b,bb, b' \in \mathcal{B} such that, importantly, (i) bbb \leq b' iff aaa \leq a', and (ii) b=bb = b' iff a=aa = a'. This ensures φ(b,b)\mathcal{B} \models \varphi(\langle b, b'\rangle) since the atomic formulas in φ\varphi are built from \leq, ==, xx and yy, on which 𝒜\mathcal{A} with the variable assignment xa,ya\langle x\mapsto a, y \mapsto a'\rangle and \mathcal{B} with xb,yb\langle x\mapsto b, y \mapsto b'\rangle agree. Conversely, if ψ\mathcal{B} \models \psi witnessed by b,bb, b' \in \mathcal{B} we can also choose a matching pair a,a𝒜a, a' \in \mathcal{A} making 𝒜ψ\mathcal{A} \models \psi.

    Now suppose ψ=x.y.φ\psi = \exists x. \forall y. \varphi. Whenever 𝒜ψ\mathcal{A} \models \psi, there is some aa such that 𝒜y.φxa\mathcal{A} \models \forall y.\varphi \langle x \mapsto a\rangle. In this case we can also choose an element bb \in \mathcal{B} that mimics a𝒜a \in \mathcal{A}: if aa is the bottom element 00 in the structure 𝒜\mathcal{A}, we let b=0b = 0 as well; if aa is the top 10001000 in 𝒜\mathcal{A}, we let bb be the top 10011001 in \mathcal{B}; otherwise we can choose an arbitrary 0<b<10010 \lt b \lt 1001. We then claim y.φxb\mathcal{B} \models \forall y. \varphi \langle x \mapsto b\rangle as well, because if there is some bb' making φxb,yb\mathcal{B} \models \varphi \langle x\mapsto b, y \mapsto b'\rangle not hold, we can also find an aa' that is to aa in 𝒜\mathcal{A} as bb' is to bb in \mathcal{B}: precisely, if b=bb' = b, we let a=aa' = a; if b<bb' \lt b, we let aa' be any element in 𝒜\mathcal{A} such that a<aa' \lt a, and similarly for the case b>bb' \gt b (such a choice is always possible because earlier aa and bb are chosen to be at the same relative position). This choice of aa' entails 𝒜φxa,ya\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, x.y.φ\mathcal{B} \models \exists x. \forall y. \varphi implies 𝒜x.y.φ\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 xx in AA or BB, there is always an element yy in the other structure that “simulates the behaviour” of xx 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 kk, the kk-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 bb\in\mathcal{B}.

  2. Winning Condition: After kk rounds, the game state consists of a=(a 1,,a k)\vec{a} = (a_1,\dots,a_k) and b=(b 1,,b i)\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 ib ia_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 a\vec{a} and b\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 kk rounds no matter how the spoiler plays, we say the duplicator has a kk-round winning strategy.

The quantifier rank qr(φ)\mathop{qr}(\varphi) of a FOL formula φ\varphi is the depth of nesting of the quantifiers in φ\varphi: qr(φ) = 0 for atomicφ qr(o(φ 1,,φ n)) = max(qr(φ 1),,qr(φ n)) for propositional connectiveso qr(Qx.φ) = 1+qr(φ) for quantifiersQ=, \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 kk-round EF game for 𝒜\mathcal{A} and \mathcal{B}, 𝒜\mathcal{A} and \mathcal{B} agree on all closed FOL formulas of quantifier-rank kk. 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 kk. Without loss of generality, we can assume ψ=Q 1x 1.Q kx k.φ\psi = Q_{1} x_{1}.\cdots Q_k x_k.\varphi where Q i{,}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=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=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 kk, the duplicator’s strategy is that whenever the spoiler picks an element a i𝒜a_i \in \mathcal{A} (or symmetrically b ib_i \in \mathcal{B}), the duplicator first constructs a FOL formula ϕ i\phi_{i} that “maximally describes the current board on 𝒜\mathcal{A}”. Roughly speaking, ϕ i\phi_{i} is the conjunction of all formulas in the following set {ψqr(ψ)=i1and𝒜ψa 1,,a i} \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, ϕ i\phi_{i} can be reduced to a finite formula using the rules of propositional connectives. With the formula ϕ i\phi_{i} in hand, the duplicator can use the fact that 𝒜x i.ϕ ix 1a 1,,x i1a i1,\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 ia ix_i \mapsto a_i. Now using the assumption that 𝒜\mathcal{A} and \mathcal{B} agree on FOL up to rank kk and the fact that x i.ϕ i\exists x_i.\phi_i is of rank ii, \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 PP (in the meta-theory) on a class MM of σ\sigma-structures. If for every natural number kk, we can find two models 𝒜 k, kM\mathcal{A}_k, \mathcal{B}_k \in M such that

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

Then by the EF theorem, the property PP 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 𝒜=A, A\mathcal{A} = \langle A, \leq^A\rangle, 𝒜φ\mathcal{A} \models \varphi exactly when aa has an even number of elements. (Hint: we pick 𝒜 k\mathcal{A}_k and k\mathcal{B}_k to be the linear order of 2 k2^k and 2 k+12^k + 1 elements respectively and play the EF games.)

Posted at September 8, 2023 2:19 PM UTC

TrackBack URL for this Entry:

0 Comments & 1 Trackback

Read the post Finite Model Theory and Game Comonads: Part 2
Weblog: The n-Category Café
Excerpt: 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, which we'll clear up now.
Tracked: September 11, 2023 4:09 PM

Post a New Comment