2023/11/27 by Harry Vinall-Smeeth, Vinall-Smeeth, Harry
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2311.15885
openalex publication_date 2023/11/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Given two n-element structures, A and B, which can be distinguished by a sentence of k-variable first-order logic (Lk), what is the minimum f(n) such that there is guaranteed to be a sentence ϕ∈ Lk with at most f(n) quantifiers, such that A \models ϕ but 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 Lk+1 is exponentially more succinct than Lk. 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.