Parallel Play Saves Quantifiers

TL;DR

This work introduces parallel play for multi-structural (MS) games as a powerful method to bound the number of quantifiers needed in FO descriptions of properties on ordered structures. By combining sub-games in parallel, the authors derive near-tight upper bounds for separating sets of linear orders and binary strings, notably proving $q(ll) \,\le\, r(ll) + 1$ with $r(ll) = 1 + \lfloor \log(\u001ell)\rfloor$ for linear orders, and establishing $(1+\varepsilon)\frac{n}{\log(n)}$-quanta upper bounds for separating arbitrary disjoint sets of $n$-bit strings. They develop the Closest-to-Midpoint Alternation (CMA) strategy, provide base and inductive analyses, and obtain alternating quantifier signatures in various regimes, including all-vs-all string separation. The results significantly advance understanding of quantifier complexity in ordered structures, with concrete open questions about tightening string-separation bounds, and potential extensions using numeric relations like the bit predicate. Overall, parallel play yields substantial quantifier savings and tight bounds in fundamental FO expressiveness problems on linear orders and binary strings.

Abstract

The number of quantifiers needed to express first-order properties is captured by two-player combinatorial games called multi-structural (MS) games. We play these games on linear orders and strings, and introduce a technique we call "parallel play", that dramatically reduces the number of quantifiers needed in many cases. Linear orders and strings are the most basic representatives of ordered structures -- a class of structures that has historically been notoriously difficult to analyze. Yet, in this paper, we provide upper bounds on the number of quantifiers needed to characterize different-sized subsets of these structures, and prove that they are tight up to constant factors, including, in some cases, up to a factor of $1+\varepsilon$, for arbitrarily small $\varepsilon$.

Figures (2)

• Figure 1: The position after $\bS$'s round $1$ move in the game $\textrm{MSL}_{\exists,4}(5)$. The pebble $\r$ is on the closest-to-midpoint of every board on the left.
• Figure 2: The $\textrm{MSL}_{\exists,4}(5)$ game tree. Each leaf is decorated with the associated quantifier signature. All paths can be played in parallel using Lemma \ref{['lem:parallelplay']} using the pattern $(\exists, \forall, \exists, \forall)$.

Theorems & Definitions (30)

• Theorem 1: Fundamental Theorem of MS Games, MScanon0MScanon1
• Definition 3
• Lemma 4
• Lemma 5: Parallel Play Lemma --- Baby Version
• Lemma 6: Parallel Play Lemma
• Theorem 7: Quantifier Rank, ROSENSTEIN:1982
• Claim 7: Splitting Rules
• Lemma 7
• Lemma 9
• Corollary 9