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.
翻译:多结构(MS)游戏是一种组合博弈,它能够刻画一阶句子中量词的数量。从定义上看,MS游戏与Ehrenfeucht-Fraisse(EF)游戏存在两点差异:第一,MS游戏在两个结构集合上进行,而EF游戏在一对结构上进行;第二,在MS游戏中,重复者(Duplicator)可以对结构进行任意次数的复制。在本文的第一部分,我们对MS游戏进行了更精细的分析,并将其与EF游戏进行了更深入的比较。特别地,我们指出结构集合的使用是本质性的,当MS游戏在结构对上进行时,它刻画的是具有固定量词数的一阶句子的布尔组合。在此基础上,我们聚焦于MS游戏与EF游戏的另一个重要区别,即在某些MS游戏中,挑战者(Spoiler)必须基于先前落子位置进行操作才能获胜。通过对MS游戏过程中所实现类型的分析,我们刻画了挑战者从未基于先前落子位置操作的MS游戏变体的表达能力。在第二部分中,我们着眼于同时刻画一阶逻辑中的量词数量和变量数量。我们证明了MS游戏的自然变体无法实现这一目标。随后,我们引入了一种新博弈——量词变量树博弈,并证明它能同时刻画量词数量和变量数量。