一句话：利用 QVT 博弈研究 k 变量一阶逻辑中区分两个结构所需的量词数，并证明其与量词深度可指数分离。
论文研究如下问题：若两个 n 元结构可由 k 变量一阶逻辑（L^k）的某个句子区分，则最少需要多少个量词才能保证存在这样的区分句子？作者借助新近提出的 QVT 博弈（quantifier-variable tree games）给出若干结果。核心结论是：在限制变量数时，区分两个结构所需的量词深度与量词数之间可以存在指数级差距；由此推出 L^{k+1} 比 L^k 指数级更简洁。此外，在存在正片段中，作者展示了如何将量词深度下界提升为量词数下界，从而得到几乎紧确的界。该工作揭示变量数限制下量词数量作为逻辑简洁性度量的重要性，并为有限变量逻辑的分离与下界证明提供了新工具。
Given two n-element structures, A and ℬ, which can be distinguished by a sentence of k-variable first-order logic (ℒk), what is the minimum f(n) such that there is guaranteed to be a sentence Φ ∈ ℒk with at most f(n) quantifiers, such that A ⊨ Φ but ℬ ⊭ Φ? We will present various results related to this question obtained by using the recently introduced QVT games [14]. 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. As a consequence, we show that ℒk+1 is exponentially more succinct that ℒ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.