Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Multi-Structural Games and Number of Quantifiers

Ronald Fagin, Jonathan Lenchner, Kenneth W. Regan, Nikhil Vyas

TL;DR

The paper introduces multi-structural (MS) games as a refinement of Ehrenfeucht-Fraïssé games to measure the number of quantifiers needed in first-order descriptions of finite structures. It proves an Equivalence Theorem linking r-round MS game outcomes to the existence of a first-order sentence with at most $r$ quantifiers distinguishing two sets of structures, and extends this with a fixed-prefix variant. Focusing on finite linear orders, the authors derive tight bounds for the function $g(r)$ that captures the threshold where a property becomes definable with $r$ quantifiers, establishing $g(1)=1$, $g(2)=2$, $g(3)=4$, $g(4)=10$, and for $r>4$ the recurrence $g(r)=2g(r-1)$ if $r$ is even and $g(r)=2g(r-1)+1$ if $r$ is odd. To achieve these results, they develop MS games with atoms, a refined framework enabling recursive strategies and yielding matching upper and lower bounds, and they discuss extensions to second-order logic and other structure classes. The work provides a precise, game-theoretic account of quantifier-prefix complexity and offers tools for analyzing definability beyond linear orders, with potential implications for descriptive complexity and finite-model theory.

Abstract

We study multi-structural games, played on two sets $\mathcal{A}$ and $\mathcal{B}$ of structures. These games generalize Ehrenfeucht-Fraïssé games. Whereas Ehrenfeucht-Fraïssé games capture the quantifier rank of a first-order sentence, multi-structural games capture the number of quantifiers, in the sense that Spoiler wins the $r$-round game if and only if there is a first-order sentence $φ$ with at most $r$ quantifiers, where every structure in $\mathcal{A}$ satisfies $φ$ and no structure in $\mathcal{B}$ satisfies $φ$. We use these games to give a complete characterization of the number of quantifiers required to distinguish linear orders of different sizes, and develop machinery for analyzing structures beyond linear orders.

Multi-Structural Games and Number of Quantifiers

TL;DR

The paper introduces multi-structural (MS) games as a refinement of Ehrenfeucht-Fraïssé games to measure the number of quantifiers needed in first-order descriptions of finite structures. It proves an Equivalence Theorem linking r-round MS game outcomes to the existence of a first-order sentence with at most quantifiers distinguishing two sets of structures, and extends this with a fixed-prefix variant. Focusing on finite linear orders, the authors derive tight bounds for the function that captures the threshold where a property becomes definable with quantifiers, establishing , , , , and for the recurrence if is even and if is odd. To achieve these results, they develop MS games with atoms, a refined framework enabling recursive strategies and yielding matching upper and lower bounds, and they discuss extensions to second-order logic and other structure classes. The work provides a precise, game-theoretic account of quantifier-prefix complexity and offers tools for analyzing definability beyond linear orders, with potential implications for descriptive complexity and finite-model theory.

Abstract

We study multi-structural games, played on two sets and of structures. These games generalize Ehrenfeucht-Fraïssé games. Whereas Ehrenfeucht-Fraïssé games capture the quantifier rank of a first-order sentence, multi-structural games capture the number of quantifiers, in the sense that Spoiler wins the -round game if and only if there is a first-order sentence with at most quantifiers, where every structure in satisfies and no structure in satisfies . We use these games to give a complete characterization of the number of quantifiers required to distinguish linear orders of different sizes, and develop machinery for analyzing structures beyond linear orders.

Paper Structure

This paper contains 13 sections, 30 theorems, 20 equations, 20 figures.

Table of Contents

  1. Introduction
  2. Related work
  3. Overview of the Sections
  4. Proof of the Equivalence Theorem
  5. Preliminaries
  6. Towards Establishing Upper Bounds on $g(r)$
  7. Interlude: Why Naive Recursion cannot be used to Build up Duplicator Winning Strategies in MS Games
  8. Lower Bounds on $g(r)$
  9. Games with Atoms: A different Approach to Obtain Upper Bounds on $g(r)$
  10. Tight Bounds on $g(r)$ and Final Theorems
  11. Conclusions
  12. A Proof of Theorem \ref{['thm:f']}
  13. Game based proof of Lemma \ref{['lemma:g_underline_of_4']}

Key Result

Theorem 1.1

Spoiler wins the $r$-round E-F game on $(A,B)$ if and only if there is a 1st order sentence $\phi$ of quantifier rank at most $r$ such that $A \models \phi$ while $B \models \neg\phi$.

Figures (20)

  • Figure 1: An example showing the difference between MS and E-F games.
  • Figure 2: The case $|B| = 3, |L| = 2$.
  • Figure 3: In response to Spoiler playing $B(2)$, Duplicator makes a second copy of the $L$ board and place $L(1)$ on one board and $L(2)$ on the other board. (The diagrams omit parentheses.)
  • Figure 4: The case $|B| = 5, |L| = 4$.
  • Figure 5: After Spoiler plays $B(3)$ from the $B$ side, Duplicator plays $L(1)$, $L(2)$, $L(3)$ and $L(4)$ on different boards on the $L$ side.
  • ...and 15 more figures

Theorems & Definitions (55)

  • Theorem 1.1: Equivalence Theorem for E-F Games
  • Theorem 1.2
  • Theorem 1.3
  • Theorem 1.4: Ros82
  • Definition 1.5
  • Theorem 1.6
  • Theorem 1.7
  • proof : Proof of Theorem \ref{['thm:main1']}
  • proof : Proof of Theorem \ref{['thm:main1a']}
  • Definition 3.1
  • ...and 45 more