一句话:提出多结构博弈,以 r 轮胜负刻画分离两组结构所需一阶量词数,并完整判定线性序区分所需量词数。
论文研究多结构博弈(multi-structural games),它在两组结构 A 与 B 上进行,是 Ehrenfeucht–Fraïssé 博弈的推广。经典 EF 博弈刻画一阶句子的量词秩,而多结构博弈刻画量词数量:Spoiler 在 r 轮博弈中获胜,当且仅当存在一个至多含 r 个量词的一阶句子 φ,使 A 中每个结构都满足 φ,而 B 中每个结构都不满足 φ。作者利用该博弈完整刻画了区分不同大小线性序所需的一阶量词数量,并发展了可分析线性序之外更一般结构的组合工具。该工作为量词数量这一资源度量提供了博弈论框架与精细结果。
We study multi-structural games, played on two sets ${\mathcal{A}}$ and ${\mathcal{B}}$ of structures. These games generalize Ehrenfeucht-Fraïssé games. Whereas Ehrenfeucht-Fraïssé games capture the quantifier rank of a first-order sentence, multi-structural games capture the number of quantifiers, in the sense that Spoiler wins the r-round game if and only if there is a first-order sentence ϕ with at most r quantifiers, where every structure in ${\mathcal{A}}$ satisfies ϕ and no structure in ${\mathcal{B}}$ satisfies ϕ. We use these games to give a complete characterization of the number of quantifiers required to distinguish linear orders of different sizes, and develop machinery for analyzing structures beyond linear orders.
DOI 原文 ·
@inproceedings{paperbot6191,
title = {Multi-Structural Games and Number of Quantifiers},
author = {Ronald Fagin and Jonathan Lenchner and Kenneth W. Regan and Nikhil Vyas},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470756}
}