Multi-structural (MS) games are combinatorial games that capture the number of quantifiers of first-order sentences. On the face of their definition, MS games differ from Ehrenfeucht-Fraisse (EF) games in two ways: first, MS games are played on two sets of structures, while EF games are played on a pair of structures; second, in MS games, Duplicator can make any number of copies of structures. In the first part of this paper, we perform a finer analysis of MS games and develop a closer comparison of MS games with EF games. In particular, we point out that the use of sets of structures is of the essence and that when MS games are played on pairs of structures, they capture Boolean combinations of first-order sentences with a fixed number of quantifiers. After this, we focus on another important difference between MS games and EF games, namely, the necessity for Spoiler to play on top of a previous move in order to win some MS games. Via an analysis of the types realized during MS games, we delineate the expressive power of the variant of MS games in which Spoiler never plays on top of a previous move. In the second part we focus on simultaneously capturing number of quantifiers and number of variables in first-order logic. We show that natural variants of the MS game do *not* achieve this. We then introduce a new game, the quantifier-variable tree game, and show that it simultaneously captures the number of quantifiers and number of variables. We conclude by generalizing this game to a family of games, the *syntactic games*, that simultaneously capture reasonable syntactic measures and the number of variables.
翻译:多结构(MS)博弈是组合博弈,它们捕获了一阶语句中量词的数量。从定义表面上看,MS博弈与Ehrenfeucht-Fraisse(EF)博弈存在两点差异:首先,MS博弈在两个结构集上进行,而EF博弈在一对结构上进行;其次,在MS博弈中,复制者可以复制任意数量的结构副本。在本文的第一部分,我们对MS博弈进行更精细的分析,并将其与EF博弈进行更深入的比较。特别地,我们指出使用结构集具有本质重要性,当MS博弈在成对结构上进行时,它们捕获的是具有固定量词数量的一阶语句的布尔组合。在此之后,我们聚焦于MS博弈与EF博弈间的另一个重要差异,即破坏者在某些MS博弈中需要基于前一步动作进行落子方能获胜。通过分析MS博弈过程中实现的类型,我们刻画了破坏者从不基于前一步动作落子的MS博弈变体的表达力。在第二部分中,我们聚焦于同时捕获一阶逻辑中量词数量与变量数量的问题。我们证明MS博弈的自然变体无法实现这一目标。随后我们引入一种新博弈——量词-变量树博弈,并证明它能同时捕获量词数量与变量数量。最后,我们将此博弈推广至一系列博弈——*句法博弈*,它们能同时捕获合理的句法度量与变量数量。