Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From Quantifier Depth to Quantifier Number: Separating Structures with k Variables

Harry Vinall-Smeeth

TL;DR

This work introduces the k-quantifier-variable (QVT) game to study the gap between quantifier depth and quantifier number (QN) in the k-variable fragment $\mathcal{L}^k$. It proves that limiting to $k$ variables can yield an exponential separation between depth and quantifier count, and shows that $\mathcal{L}^{k+1}$ is exponentially more succinct than $\mathcal{L}^k$ for $k\ge 4$. By developing existential-positive variants of the QVT game, the authors lift depth lower bounds to quantifier-number lower bounds, achieving almost-tight bounds in that fragment. The paper also generalizes XOR-based hard instances via abelian-group constraints, providing exponential lower bounds and insights into the structure of QVT games, with potential implications for complexity-theoretic separations and succinctness results in finite model theory.

Abstract

Given two $n$-element structures, $\mathcal{A}$ and $\mathcal{B}$, which can be distinguished by a sentence of $k$-variable first-order logic ($\mathcal{L}^k$), what is the minimum $f(n)$ such that there is guaranteed to be a sentence $φ\in \mathcal{L}^k$ with at most $f(n)$ quantifiers, such that $\mathcal{A} \models φ$ but $\mathcal{B} \not \models φ$? We present various results related to this question obtained by using the recently introduced QVT games. In particular, we show that when we limit the number of variables, there can be an exponential gap between the quantifier depth and the quantifier number needed to separate two structures. Through the lens of this question, we will highlight some difficulties that arise in analysing the QVT game and some techniques which can help to overcome them. As a consequence, we show that $\mathcal{L}^{k+1}$ is exponentially more succinct than $\mathcal{L}^{k}$. We also show, in the setting of the existential-positive fragment, how to lift quantifier depth lower bounds to quantifier number lower bounds. This leads to almost tight bounds.

From Quantifier Depth to Quantifier Number: Separating Structures with k Variables

TL;DR

This work introduces the k-quantifier-variable (QVT) game to study the gap between quantifier depth and quantifier number (QN) in the k-variable fragment . It proves that limiting to variables can yield an exponential separation between depth and quantifier count, and shows that is exponentially more succinct than for . By developing existential-positive variants of the QVT game, the authors lift depth lower bounds to quantifier-number lower bounds, achieving almost-tight bounds in that fragment. The paper also generalizes XOR-based hard instances via abelian-group constraints, providing exponential lower bounds and insights into the structure of QVT games, with potential implications for complexity-theoretic separations and succinctness results in finite model theory.

Abstract

Given two -element structures, and , which can be distinguished by a sentence of -variable first-order logic (), what is the minimum such that there is guaranteed to be a sentence with at most quantifiers, such that but ? We present various results related to this question obtained by using the recently introduced QVT games. In particular, we show that when we limit the number of variables, there can be an exponential gap between the quantifier depth and the quantifier number needed to separate two structures. Through the lens of this question, we will highlight some difficulties that arise in analysing the QVT game and some techniques which can help to overcome them. As a consequence, we show that is exponentially more succinct than . We also show, in the setting of the existential-positive fragment, how to lift quantifier depth lower bounds to quantifier number lower bounds. This leads to almost tight bounds.
Paper Structure (41 sections, 38 theorems, 36 equations, 8 figures)

This paper contains 41 sections, 38 theorems, 36 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. (Pebbled) Structures
  5. Partial Isomorphism/Homomorphism
  6. Finite Variable Logics and Pebble Games
  7. Quantifier Number in L(k) as a Complexity Measure
  8. The Multi-Structural Game
  9. The k-QVT game
  10. Game Description
  11. Remarks on the Game
  12. Proof of Correctness
  13. Upper Bounds
  14. Formula Size
  15. Variations of the Game
  16. ...and 26 more sections

Key Result

Theorem 1

For every integer $k \ge 3$ there exists $\varepsilon >0$ and $n_0 \in \mathbb{N}$, such that for all $n>n_0$ there exists a pair of $k$-ary structures $\mathcal{A}, \mathcal{B}$ with $|A| = |B| = n$ that can be distinguished in $\mathcal{L}^k$, but which agree on every sentence of $\mathcal{L}^k$ w

Figures (8)

  • Figure 1: Position of the MS game on $\mathcal{A}, \mathcal{B}$ after one round, the green circle indicates the pebbled element on each board.
  • Figure 2: The 3-round Spoiler win described in Example \ref{['ex: 3vs2tree']}.
  • Figure 3: From left to right: a visualisation of $F$; the first three rounds of the $3$-formula game on $F$, the filled vertices represent the fact the corresponding elements are pebbled, the labels are the Duplicator moves; a possible continuation of the game. In the next move Spoiler will move the yellow pebble to $x_8$ and win.
  • Figure 4: A visualisation of the two $\mathsf{RHS}$ boards in a critical position.
  • Figure 5: A pair of good boards. Here we consider the case $k=3$. The colours represent the three different pebbles. To see that the boards are good one just needs to check they are good for three.
  • ...and 3 more figures

Theorems & Definitions (71)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Theorem 4: immerman1982upper
  • Example 5
  • Example 6: Linear order of size 3 vs 2
  • Theorem 7
  • proof
  • Lemma 8
  • proof
  • ...and 61 more