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

TL;DR

This paper investigates the relationship between quantifier depth and quantifier number in first-order logic with limited variables, revealing exponential gaps and providing bounds using QVT games.

Contribution

It introduces new bounds and techniques for separating structures with limited variables, highlighting exponential differences and lifting lower bounds in existential-positive fragments.

Findings

Exponential gap between quantifier depth and number for fixed variables

Lifting quantifier depth bounds to quantifier number bounds in existential-positive logic

Almost tight bounds for quantifier separation using QVT games

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 $\phi \in \mathcal{L}^k$ with at most $f(n)$ quantifiers, such that $\mathcal{A} \models \phi$ but $\mathcal{B} \not \models \phi$? 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.