Multi-Structural Games and Beyond

TL;DR

The paper develops and analyzes multi-structural (MS) games as a robust framework for understanding the expressive power of first-order logic on sets of structures, clarifying how MS complements Ehrenfeucht-Fraïssé (EF) games in capturing the number of quantifiers rather than quantifier rank. It introduces and studies several variants and generalizations, including play-on-top moves, restricted variables via repebbling, and the quantifier-variable tree (QVT) game, establishing tight correspondences between game outcomes and logical separability for FO$^k$ with bounded quantifiers or variables. A central contribution is the Quantifier-Variable Tree Game theorem, which ties $r$-quantifier, $k$-variable formulas to a two-player game, and the Syntactic Game (SG) framework, which unifies a broad class of compositional syntactic measures (like quantifier count, rank, and formula size) with game-theoretic outcomes. Together, these results illuminate when MS-style methods yield lower bounds or separations, reveal limitations of naive variants (e.g., repebbling), and propose a cohesive program (via QVT and SG) for characterizing logical expressiveness through syntactic costs. The work advances the understanding of finite-model theory by linking structural properties of FO formulas to concrete, game-theoretic strategies, with implications for lower bounds and descriptive complexity in ordered and unordered structures.

Abstract

Multi-structural (MS) games are combinatorial games that capture the number of quantifiers of first-order sentences. On the face of their definition, MS games differ from Ehrenfeucht-Fraisse (EF) games in two ways: first, MS games are played on two sets of structures, while EF games are played on a pair of structures; second, in MS games, Duplicator can make any number of copies of structures. In the first part of this paper, we perform a finer analysis of MS games and develop a closer comparison of MS games with EF games. In particular, we point out that the use of sets of structures is of the essence and that when MS games are played on pairs of structures, they capture Boolean combinations of first-order sentences with a fixed number of quantifiers. After this, we focus on another important difference between MS games and EF games, namely, the necessity for Spoiler to play on top of a previous move in order to win some MS games. Via an analysis of the types realized during MS games, we delineate the expressive power of the variant of MS games in which Spoiler never plays on top of a previous move. In the second part we focus on simultaneously capturing number of quantifiers and number of variables in first-order logic. We show that natural variants of the MS game do *not* achieve this. We then introduce a new game, the quantifier-variable tree game, and show that it simultaneously captures the number of quantifiers and number of variables. We conclude by generalizing this game to a family of games, the *syntactic games*, that simultaneously capture reasonable syntactic measures and the number of variables.

Figures (8)

• Figure 1: The beginning of a $2$-round MS game on $(\mathcal{A}, \mathcal{B})$, where $\mathcal{A} = \{\mathsf{LO}(3)$}, the singleton linear order of size $3$, and $\mathcal{B} = \{\mathsf{LO}(2)\}$, the singleton linear order of size $2$. Spoiler plays his first move (indicated in red) on B2, the middle element of $\mathsf{LO}(3)$. Duplicator then makes a copy of $\mathsf{LO}(2)$ and plays each of the two possible moves in response. This example is a slight variation on the examples in MSgames1MSgames2.
• Figure 2: A rooted tree $\mathsf{RT}(4)$ whose longest branch has $4$ nodes, and a linear order $\mathsf{LO}(4)$ of $4$ nodes, drawn as a rooted tree (left); a rooted tree $\mathsf{RT}(3)$ whose longest branch has $3$ nodes and a linear order $\mathsf{LO}(3)$ of $3$ nodes (right).
• Figure 5: A rooted tree $\mathsf{RT}(4)$ whose longest branch has $4$ nodes (left); a rooted tree $\mathsf{RT}(3)$ whose longest branch has $3$ nodes (right).
• Figure 7: A complete play of the $\mathcal{QVT}({3},{2})\text{ game on }(\{\mathsf{LO}(3)\}, \{\mathsf{LO}(2)\})$. Spoiler closes the game tree $\mathcal{T}$ using only three pebble moves, and two pebble colors $x_1$ (red) and $x_2$ (blue). The atomic separating sentences are shown below, and the resulting separating sentence is $\exists x_1(\exists x_2 (x_2 < x_1) \land \exists x_2(x_1 < x_2))$, which can be read off $\mathcal{T}$.
• Figure 8: Configuration (partial) after two pebble moves, depicting just two pairs of pebbled structures that maintain isomorphisms.

Theorems & Definitions (49)

• Definition 2.1
• Definition 2.2
• Theorem 2.3: Immerman81MSgames1
• Theorem 2.4
• Proposition 3.2
• proof
• Proposition 3.2
• proof
• Example 3.4
• Theorem 3.5