1 Introduction
As is well known, the expressive power of first-order logic can be characterized in terms of Ehrenfeucht–Fraïssé games (Ehrenfeucht Reference Ehrenfeucht1961; Fraïssé Reference Fraïssé1957): a class of structures for a finite vocabulary is definable by a sentence of first-order logic if and only if there is a natural number n such that one of the two players, called Spoiler here, has a winning strategy in the Ehrenfeucht–Fraïssé game of length n on any pair of structures one of which is in the class and the other not in the class. Due to this characterization result, Ehrenfeucht–Fraïssé games have become a standard tool for proving undefinability results for first-order logic; this is particularly the case for classes of finite structures, where the usual tools from classical model theory, like the compactness theorem, cannot be used.
Looking from another perspective, Ehrenfeucht–Fraïssé games can also be used for studying the complexity of defining properties of structures. The length of the game corresponds exactly to the quantifier rank of sentences needed for defining the property: Spoiler has a winning strategy in the game of length n for an arbitrary structure in the class and another structure not in the class if and only if the class is definable by a sentence of quantifier rank (at most) n. However, quantifier rank is an extremely rough measure for the complexity of sentences. Consider, for example, the structure
${\mathfrak V}_n=(V_n,\in)$
, where
$V_n$
is the set of hereditarily finite sets of rank less than n. It is easy to show by induction on the rank of sets that every element of
${\mathfrak V}_n$
is definable by a formula of quantifier rank at most n, and hence there are
$2^{|V_n|}=\mathsf{twr}(n+1)$
non-equivalent formulas with one free variable of quantifier rank n on the structure
${\mathfrak V}_n$
. Here,
$\mathsf{twr}$
is the exponential tower function defined recursively by
$\mathsf{twr}(0)=0$
and
$\mathsf{twr}(n+1)=2^{\mathsf{twr}(n)}.$
Footnote 1 Thus, knowing the quantifier rank of a formula (over a vocabulary containing relations of arity at least two) only gives a nonelementary upper bound for the length of the shortest equivalent formula.
Furthermore, as is well known, the structure
${\mathfrak V}_n$
is isomorphic to
${\mathfrak B}_n=(B_n,{\mathsf{BIT}}^{-1})$
Footnote 2, where
$B_n$
is the set of natural numbers
$k<\mathsf{twr}(n)$
, and
${\mathsf{BIT}}^{-1}$
is the inverse of the BIT-relation (see, e.g., Immerman Reference Immerman1999):
$(i,j)\in{\mathsf{BIT}}^{-1}$
if and only if the ith bit of the binary representation of j is 1. Thus, all elements of structures with
$\mathsf{twr}(n)$
elements and a built-in BIT-relation are also definable by sentences of quantifier rank n (this remains true also for structures with less than
$\mathsf{twr}(n)$
elements). In particular, this means that equivalence with respect to quantifier rank n sentences captures isomorphism on structures of size at most
$\mathsf{twr}(n)$
with a built-in BIT-relation. Thus, to prove undefinability of properties of structures in the presence of a built-in BIT-relation via Ehrenfeucht–Fraïssé games of length n, it is necessary to consider structures of size more than
$\mathsf{twr}(n)$
. Note that the same holds for Ehrenfeucht–Fraïssé games for existential second-order logic, as it is easy to specify with a first-order formula that a quantified binary relation is isomorphic with the BIT-relation.
For these reasons, it is natural to study more fine-grained measures for the complexity of first-order sentences and look for games that characterize equivalence of structures with respect to these measures. There are two main lines of research in the literature that have started from such considerations. The first of them uses the number of quantifiers, instead of the quantifier rank, as a measure of complexity of first-order formulas. In the second approach, the size (or length) of formulas is used as a measure of complexity.
A game that characterizes the total number of quantifiers was first introduced by Immerman (Reference Immerman1981); accordingly, we call it the Immerman game. Immerman (Reference Immerman1981) does not give any concrete examples of the game but mentions a potential application in descriptive complexity theory: if one could prove that some PTIME-complete problem is not definable in ordered finite structures of size n by a sentence with
$\mathcal{O}(\log n)$
quantifiers, then this would separate PTIME from NLOGSPACE, as all NLOGSPACE properties can be defined by such sentences on ordered structures of size n. It is also pointed out in Immerman (Reference Immerman1981) that ordinary Ehrenfeucht–Fraïssé games cannot be used for this purpose, as equivalence with respect to quantifier rank
$\log n$
captures isomorphism on ordered structures of size n.
The Immerman game was apparently forgotten for some 40 years, but it was recently re-discovered by Fagin et al. (Reference Fagin, Lenchner, Regan and Vyas2021). In this paper, the authors provided the first applications for the game: they defined a function
$h\colon{\mathbb{N}}\to{\mathbb{N}}$
by a recursion formula and proved that two linear orders of different lengths can be separated by a sentence with n quantifiers if and only if at least one of them is of length less than h(n). After the article Fagin et al. (Reference Fagin, Lenchner, Regan and Vyas2021), the study of the Immerman game has been continued in Fagin et al. (Reference Fagin, Lenchner, Vyas, Ryan Williams, Szeider, Ganian and Silva2022) and Carmosino et al. (Reference Carmosino, Fagin, Immerman, Kolaitis, Lenchner and Sengupta2023).
The other research line that uses the size of formulas as a parameter was started by Adler and Immerman (Reference Adler and Immerman2003), who defined a game (usually called the Adler–Immerman game) that characterizes equivalence of temporal structures with respect to CTL formulas of a given size. They used this game to prove an
$n!$
lower bound for the size of CTL formulas required for defining certain property of temporal structures. On the other hand, this property is definable by a linear size CTL
${}^+$
formula, and consequently CTL
${}^+$
is
$n!$
times more succinct than CTL. After Adler and Immerman (Reference Adler and Immerman2003), the Adler–Immerman game has been adapted to several different types of modal logics and applied successfully to many similar succinctness proofs (see, e.g., French et al. Reference French, van der Hoek, Iliev and Kooi2013;Hella and Vilander Reference Hella and Vilander2019; Lutz Reference Lutz, Nakashima, Wellman, Weiss and Stone2006; van derHoek and Iliev 2014; van Ditmarsch et al. Reference van Ditmarsch, Fan, van der Hoek, Iliev, Goré, Kooi and Kurucz2014). It should be noted that already before Adler and Immerman (Reference Adler and Immerman2003), Razborov (Reference Razborov1990) introduced a game of a slightly different type that characterizes equivalence with respect to boolean formulas of a given size.
The idea behind the Adler–Immerman game was applied in the context of first-order logic by Grohe and Schweikardt (Reference Grohe and Schweikardt2005). Using so-called extended syntax trees, they proved lower bounds for the size of first-order formulas with 2 and 3 variables needed for separating linear orders of different lengths. An extended syntax tree is essentially a complete description of Spoiler’s strategy in the Adler–Immerman game.
An explicit game characterizing equivalence with respect to first-order formulas of a given size was formulated by Väänänen (2015). This game has a different flavor from the Adler–Immerman game in one important respect: In the Adler–Immerman game, Duplicator (the opponent of Spoiler) has a trivial strategy that is optimal, and thus the moves of Duplicator could be replaced by the default moves given by this optimal strategy. On the other hand, in the game of Hella and Väänänen (Reference Hella, Väänänen, Hirvonen, Kontinen, Kossak and Villaveces2015), the moves of Duplicator cannot be replaced by such default strategy. In this respect, the game introduced in Hella and Väänänen (Reference Hella, Väänänen, Hirvonen, Kontinen, Kossak and Villaveces2015) is similar to the game of Razborov (Reference Razborov1990) mentioned above.
A common feature of the Immerman game
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
and the games for the size of formulas is that they are played on two classes
$\mathbb{A}$
and
$\mathbb{B}$
of structures instead of just two structures
${\mathfrak A}$
and
${\mathfrak B}$
, like the usual Ehrenfeucht–Fraïssé game. The rules of
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
are similar to those of the Ehrenfeucht–Fraïssé game in the sense that Spoiler and Duplicator play
$\ell$
rounds, and in each round Spoiler chooses interpretations for a variable on the members of either
$\mathbb{A}$
or
$\mathbb{B}$
, and Duplicator answers by choosing interpretations for the variable on members of the other class. However, there is an important difference: Duplicator is allowed to make copies of each structure in the class she is playing on and choose a different interpretation for the variable in each copy. Duplicator wins the play of the game if after the
$\ell$
rounds there exist structures
${\mathfrak A}\in\mathbb{A}$
and
${\mathfrak B}\in\mathbb{B}$
such that for at least one copy of each of them, the interpretations chosen for the variables form a partial isomorphism from
${\mathfrak A}$
to
${\mathfrak B}$
.
In many applications, one can start the game
$\mathsf{IG}_\ell$
on singleton classes
$\mathbb{A}=\{{\mathfrak A}\}$
and
$\mathbb{B}=\{{\mathfrak B}\}$
, but since Duplicator can make copies of the structures and choose different interpretations for variables, after the initial position in the game, the classes are no longer singletons. Moreover, Carmosino et al. (Reference Carmosino, Fagin, Immerman, Kolaitis, Lenchner and Sengupta2023) show that there are properties of structures that can be proved to be undefinable by sentences with n quantifiers, but this cannot be proved by using the Immerman game on singleton classes.
While the rules of the Immerman game are relatively simple, and the game is certainly natural and intuitive, it turns out that it is by no means unique for characterizing the number of quantifiers in the same way as the Ehrenfeucht–Fraïssé game is for characterizing quantifier rank. Indeed, we will define in this paper three other games and prove that they are all equivalent to the Immerman game in the sense that Spoiler has a winning strategy in any of them if and only if he has a winning strategy in the Immerman game (naturally the same holds for Duplicator). Hence, each of the three games characterizes separability of classes by a sentence containing a given number of quantifiers.
The first of the games,
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
(number of quantifiers game), is obtained by a natural modification of the formula size game
$\mathsf{FSG}(\ell,\mathbb{A},\mathbb{B})$
of Hella and Väänänen (Reference Hella, Väänänen, Hirvonen, Kontinen, Kossak and Villaveces2015). The idea is simply to remove the number of connectives and atomic formulas from the size parameter
$\ell$
used in
$\mathsf{FSG}$
and leave just the number of quantifiers. The game
$\mathsf{NQG}$
still has separate rules for dealing with connectives, and thus it looks quite different from the Immerman game. However, this difference is not essential, as the connective moves can be easily eliminated from the game without affecting the winner.
The second game that we define,
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
(monotone prefix game), is first derived for singleton classes
$\{{\mathfrak A}\}$
and
$\{{\mathfrak B}\}$
by analyzing the strategies of Spoiler in the Immerman game against the default optimal strategy of Duplicator. Since Duplicator does not have any active role in the game, the order of the moves of Spoiler does not matter, so we can let Spoiler play his choices first on the structure
${\mathfrak A}$
, and after that on the structure
${\mathfrak B}$
. Furthermore, instead of playing the game move by move, we can let Spoiler play by just announcing his strategies on
${\mathfrak A}$
and
${\mathfrak B}$
. These strategies can be interpreted as strategies of
$\exists$
(the existential player) and
$\forall$
(the universal player) in the semantic game for a sentence of the form
$\vec Q\vec x\,\theta$
on
${\mathfrak A}$
and
${\mathfrak B}$
, respectively, where
$\vec Q\vec x$
is a quantifier prefix of length
$\ell$
and
$\theta$
is quantifier free. By changing the winning condition we can further let Duplicator play a strategy of
$\exists$
instead of Spoiler playing a strategy of
$\forall$
in the semantic game on
${\mathfrak B}$
. In this way, we obtain the game
$\mathsf{MPG}(\ell,{\mathfrak A},{\mathfrak B})$
that is equivalent to the Immerman game
$\mathsf{IG}_\ell(\{{\mathfrak A}\},\{{\mathfrak B}\})$
, but in which Duplicator makes nontrivial moves that cannot be eliminated by a default strategy. Furthermore, we introduce a natural generalization
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
of the game to arbitrary classes
$\mathbb{A}$
and
$\mathbb{B}$
and prove that it is equivalent to
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
. We also point out that the game
$\mathsf{MPG}(\ell,{\mathfrak A},{\mathfrak B})$
is actually a special case of the standard Ehrenfeucht–Fraïssé game for monotone generalized quantifiers (see Krawczyk and Krynicki Reference Krawczyk, Krynicki, Marek, Srebrny and Zarach1976).
During a play of the Immerman game
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B}),$
the players essentially produce a set
$T_{\mathfrak C}$
of assignments on each
${\mathfrak C}\in\mathbb{A}\cup\mathbb{B}$
:
$T_{\mathfrak C}$
consists of the assignments that arise from the interpretations chosen for the variables in
$\vec x$
in the copies of
${\mathfrak C}$
. The sets
$T_{\mathfrak C}$
are formed in a parallel way in the sense that Duplicator makes all the copies and chooses the corresponding interpretations for each variable simultaneously. The idea of our third game,
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
(prenex normal form game), is to let Spoiler and Duplicator play many repetitions of the semantic game for some fixed quantifier prefix
$\vec Q\vec x$
on structures
${\mathfrak A}\in\mathbb{A}$
chosen by D in succession, thus producing a set of assignments in a sequential way. Surprisingly, it suffices then to let Spoiler and Duplicator play the semantic game on a structure
${\mathfrak B}\in\mathbb{B}$
only once, assuming that they have played enough repetitions of it on structures of
$\mathbb{A}$
. A nice feature of the game
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
is that the number of repetitions needed is relatively small: it is bounded above by the number of complete atomic types of
$\ell$
-tuples of elements.
As for the two previous games, we prove that
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
is equivalent to
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
and thus characterizes separability of
$\mathbb{A}$
and
$\mathbb{B}$
by a sentence containing at most
$\ell$
quantifiers. We also illustrate the use of the prenex normal form game on linearly ordered sets: we show that a linearly ordered set
${\mathfrak A}$
of length m can be separated from a linearly ordered set
${\mathfrak B}$
of length n by a sentence of the form
$\forall x_1\ldots\forall x_k\exists y_1\ldots \exists y_\ell\,\theta$
if and only if
$m>n$
and
$n<(k+1)\ell$
, assuming that
$m,n\ge k$
.
The structure of this paper is as follows. In Section 2, we go quickly through the basic notions and notations used in the paper. In Section 3, we define the Immerman game
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
first in its original form by Immerman (Reference Immerman1981) and Fagin et al. (Reference Fagin, Lenchner, Regan and Vyas2021). After this, we define a slightly modified but equivalent game
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
that is easier to relate to the formula size game. In Section 4, we first review the formula size game
$\mathsf{FSG}(\ell,\mathbb{A},\mathbb{B})$
of Hella and Väänänen (Reference Hella, Väänänen, Hirvonen, Kontinen, Kossak and Villaveces2015). Then, we introduce the number of quantifiers game
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
and prove that it is equivalent to
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
, and that Spoiler has a winning strategy in either of these games if and only if the classes
$\mathbb{A}$
and
$\mathbb{B}$
can be separated by a sentence with at most
$\ell$
quantifiers. Section 5 is dedicated to the monotone prefix game
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
. We show how it can be derived from the modified Immerman game
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
and then relate it to the Ehrenfeucht–Fraïssé game for monotone generalized quantifiers. In Section 6, we introduce the prenex normal form game
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
and prove that it is equivalent to
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
. Finally, we close the paper in Section 7 by some concluding remarks.
2. Preliminaries
Let
$\tau$
be a vocabulary. We denote
$\tau$
-structures by
${\mathfrak A},{\mathfrak B},{\mathfrak C},\ldots$
, and their universes by
$A,B,C,\ldots$
, respectively. We will restrict our attention to finite relational vocabularies. Thus, a
$\tau$
-structure
${\mathfrak A}$
consists of the universe A, and a finite number of relations
$R^{\mathfrak A}\subseteq A^n$
for
$R\in\tau$
, where
$n={\rm ar}(R)$
is the arity of the relation symbol R. We are mainly interested in finite structures, but all the games we define in the subsequent sections work as such also on (classes of) infinite structures.
An assignment on a
$\tau$
-structure
${\mathfrak A}$
is a function
$s\colon V\to A$
for some set V of variables. We call the pair
${\mathcal A}=({\mathfrak A},s)$
a
$(\tau,V)$
-interpretation, or briefly just an interpretation if
$\tau$
and V are clear from the context. Given an element
$a\in A$
and a variable x, we denote by
$s[a/x]$
the modified assignment
$V\cup\{x\}\to A$
that maps x to a, and y to s(y) for all variables
$y\in V\smallsetminus\{x\}$
(note that the case
$x\in V$
is also allowed). If
$\vec x=(x_1,\ldots,x_\ell)$
and
$\vec a=(a_1,\ldots,a_\ell)\in A^n$
, we may use the notation
$\vec a/\vec x$
for the assignment
$s\colon \{x_1,\ldots,x_\ell\}\to A$
such that
$s(x_i)=a_i$
for
$1\le i\le \ell$
.
The formulas of first-order logic are defined in the usual way, and we write
${\mathcal A}\models\varphi$
if
${\mathcal A}=({\mathfrak A},s)$
is a
$(\tau,V)$
-interpretation and
$\varphi$
is a
$\tau$
-formula that is true in
${\mathfrak A}$
when the free variables of
$\varphi$
are interpreted by s. If
$\varphi$
is a sentence, we may write just
${\mathfrak A}\models\varphi$
instead of
$({\mathfrak A},s)\models\varphi$
.
Partial isomorphisms from a
$\tau$
-structure
${\mathfrak A}$
to another
$\tau$
-structure
${\mathfrak B}$
are defined as usual: a bijection
$p\colon C\to D$
, where
$C\subseteq A$
and
$D\subseteq B$
, is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
if the equivalence
$(a_1,\ldots,a_n)\in R^{\mathfrak A}\iff (p(a_1),\ldots,p(a_n))\in R^{\mathfrak B}$
holds for all
$R\in\tau$
and all
$a_1,\ldots,a_n\in C$
, where
$n={\rm ar}(R)$
. We will often use assignments for defining partial isomorphisms: if
$s\colon V\to A$
and
$t\colon V\to B$
are assignments on
${\mathfrak A}$
and
${\mathfrak B}$
, respectively, then we say that
$s\mapsto t$
is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
if the relation
$p\subseteq A\times B$
defined as
$p:=\{(s(x),t(x))\mid x\in V\}$
is a partial isomorphism. Similarly, we say that
${\vec{a}}\mapsto{\vec{b}}$
is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
for tuples
${\vec{a}}=(a_1,\ldots,a_\ell)\in A^\ell$
and
${\vec{b}}=(b_1,\ldots,b_\ell)\in B^\ell$
if the corresponding relation
$\{(a_1,b_1),\ldots,(a_\ell,b_\ell)\}$
is a partial isomorphism.
One of the key notions we need in the subsequent sections is that of separating two classes of interpretations by a formula:
Definition 1. Let
$\tau$
be a vocabulary, V a finite set of variables, and
$\mathbb{A}$
and
$\mathbb{B}$
classes of
$(\tau,V)$
-interpretations. We say that formula
$\varphi$
with free variables in V separates the classes
$\mathbb{A}$
and
$\mathbb{B}$
, in symbols
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
, if
${\mathcal A}\models\varphi$
for all
${\mathcal A}\in\mathbb{A}$
and
${\mathcal B}\not\models\varphi$
for all
${\mathcal B}\in\mathbb{B}$
.
We formulate next a recursive characterization for a formula separating two classes of interpretations. To deal with the quantifiers, we introduce the following handy notation:
• Let
$\mathbb{A}$
be a class of
$(\tau,V)$
-interpretations. A choice function for
$\mathbb{A}$
is a function F such that
$\mathrm{dom}(F)=\mathbb{A}$
and
$F({\mathcal A})\in A$
for all
${\mathcal A}=({\mathfrak A},s)\in\mathbb{A}$
.• If F is a choice function for
$\mathbb{A}$
and x is a variable, then we denote the class
$\{({\mathfrak A},s[F({\mathcal A})/x])\mid {\mathcal A}=({\mathfrak A},s)\in\mathbb{A}\}$
by
$F_x(\mathbb{A})$
.• Furthermore, we denote the class
$\{({\mathfrak A},s[a/x])\mid ({\mathfrak A},s)\in\mathbb{A}, a\in A\}$
by
$U_x(\mathbb{A})$
.
We omit the straightforward proof of the characterization result below.
Lemma 2. Let
$\mathbb{A}$
and
$\mathbb{B}$
be classes of
$(\tau,V)$
-interpretations.
(a)
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\lnot\varphi)$
if and only if
$\mathsf{Sep}(\mathbb{B},\mathbb{A},\varphi)$
.(b)
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi\lor\psi)$
if and only if there are subclasses
$\mathbb{C},\mathbb{D}\subseteq\mathbb{A}$
such that
$\mathbb{A}=\mathbb{C}\cup\mathbb{D}$
,
$\mathsf{Sep}(\mathbb{C},\mathbb{B},\varphi)$
and
$\mathsf{Sep}(\mathbb{D},\mathbb{B},\psi)$
.(c)
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi\land\psi)$
if and only if there are subclasses
$\mathbb{C},\mathbb{D}\subseteq\mathbb{B}$
such that
$\mathbb{B}=\mathbb{C}\cup\mathbb{D}$
,
$\mathsf{Sep}(\mathbb{A},\mathbb{C},\varphi)$
and
$\mathsf{Sep}(\mathbb{A},\mathbb{D},\psi)$
.(d)
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\exists x\,\varphi)$
if and only if there exists a choice function F for
$\mathbb{A}$
such that
$\mathsf{Sep}(F_x(\mathbb{A}),U_x(\mathbb{B}),\varphi)$
.(e)
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\forall x\,\varphi)$
if and only if there exists a choice function G for
$\mathbb{B}$
such that
$\mathsf{Sep}(U_x(\mathbb{A}),G_x(\mathbb{B}),\varphi)$
.
3. Immerman Game
In this section, we will first define the Immerman game according to its original formulation (Fagin et al. Reference Fagin, Lenchner, Regan and Vyas2021; Immerman Reference Immerman1981). We will later define a slightly modified game, which is however clearly equivalent to the original version. The modified version is easier to compare with the formula size game that we consider in the next section.
As explained in Introduction, the Immerman game
$\mathsf{IG}_\ell$
is played on a pair
$(\mathbb{A},\mathbb{B})$
of classes of structures instead of single structures. The parameter
$\ell$
refers to the number of rounds. During the game, the players, Spoiler (S) and Duplicator (D), choose interpretations for variables
$x_1,\ldots,x_\ell$
in the structures. Thus, after the initial state, the classes will consist of interpretations of the form
$({\mathfrak A},s)$
, where
$s\colon \{x_1,\ldots,x_i\}\to A$
, and
$i\le \ell$
is the number of rounds played.
In round i, S chooses one interpretation for a variable
$x_i$
in each interpretation in
$\mathbb{A}$
or in
$\mathbb{B}$
. However, D is allowed to make as many copies of the interpretations (in the other class) and give different interpretations for
$x_i$
in different copies.
Definition 3. The starting position of
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
is
$(\mathbb{A}_0,\mathbb{B}_0)=(\mathbb{A},\mathbb{B})$
. Suppose the position after
$i<\ell$
moves is
$(\mathbb{A}_i,\mathbb{B}_i)$
. There are two possibilities for the continuation of the game:
∃-move: S chooses an element
$c_{\mathcal A}\in A$
from each interpretation
${\mathcal A}=({\mathfrak A},s)\in\mathbb{A}_i$
, and sets
$\mathbb{A}_{i+1}=\{({\mathfrak A},s[c_{\mathcal A}/x_{i+1}])\mid {\mathcal A}=({\mathfrak A},s)\in \mathbb{A}_i\}$
.
D answers by choosing a nonempty set
$D_{\mathcal B}\subseteq B$
for each
${\mathcal B}=({\mathfrak B},t)\in\mathbb{B}_i$
, and sets
$\mathbb{B}_{i+1}=\{({\mathfrak B},t[d/x_{i+1}])\mid {\mathcal B}=({\mathfrak B},t)\in \mathbb{B}_i, d\in D_{\mathcal B}\}$
.
The next position in the game is
$(\mathbb{A}_{i+1},\mathbb{B}_{i+1})$
.
∀-move: Similar to
$\exists$
-move, but with the roles of
$\mathbb{A}_i$
and
$\mathbb{B}_i$
switched.
The game ends after
$\ell$
rounds in position
$(\mathbb{A}_\ell,\mathbb{B}_\ell)$
. The winning condition of the game is the following: 12pt
PI D wins the game if there are interpretations
$({\mathfrak A},s)\in\mathbb{A}_\ell$
and
$({\mathfrak B},t)\in\mathbb{B}_\ell$
such that
$s\mapsto t$
is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
. Otherwise S wins.
The notions of strategy and winning strategy for a player in
$\mathsf{IG}_\ell$
(and other games that follow) are defined as usual in terms of functions that determine the moves of the player in each position. We omit the technical definition here. Informally, a winning strategy of S (D) in
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
is a systematic way of making his moves which guarantees that he wins the play irrespective of the moves made by D (S, respectively).
Theorem 4. (Fagin et al. Reference Fagin, Lenchner, Regan and Vyas2021; Immerman Reference Immerman1981). The following conditions are equivalent:
(1) There is a sentence
$\varphi$
with at most
$\ell$
quantifiers such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
.(2) S has a winning strategy in
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
.
We will later see that Theorem 4 follows from another characterization of separability of classes with
$\ell$
-quantifier sentences (see Theorem 11).
Note that if the intersection of the classes
$\mathbb{A}$
and
$\mathbb{B}$
is nonempty, then it is obvious that there can be no sentence
$\varphi$
that separates them. In this case, D has a simple winning strategy in
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
: fix a structure
${\mathfrak A}\in\mathbb{A}\cap\mathbb{B}$
, and copying the moves of S on
${\mathfrak A}$
, make sure that for each
$i\le\ell$
, there is an assignment
$s_i\colon\{x_1,\ldots,x_i\}\to A$
such that
$({\mathfrak A},s_i)\in\mathbb{A}_i\cap\mathbb{B}_i$
. Then
$({\mathfrak A},s_\ell)\in\mathbb{A}_\ell$
and
$({\mathfrak A},s_\ell)\in\mathbb{B}_\ell$
, witnessing that the winning condition PI for D holds.
Note further that D has an obvious optimal strategy in
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
: simply always choose all possible interpretations for variables (i.e., choose
$D_{\mathcal B}=B$
for each
${\mathcal B}=({\mathfrak B},t)\in\mathbb{B}_i$
in
$\exists$
-moves, and
$D_{\mathcal A}=A$
for each
${\mathcal A}=({\mathfrak A},s)\in\mathbb{A}_i$
in
$\forall$
-moves). This is called the oblivious strategy in Fagin et al. (Reference Fagin, Lenchner, Regan and Vyas2021). In this sense, the game
$\mathsf{IG}_\ell$
can be seen as a “solitaire” rather than a genuine two-player game. In Sections 5 and 6, we will define alternative games that also characterize separability of classes by
$\ell$
-quantifier sentences, but in which both players have an essential role (see Definitions 13 and 17).
As the length of the game
$\mathsf{IG}_\ell$
is finite, and there are no ties, it is determined for any classes
$\mathbb{A}$
and
$\mathbb{B}$
, i.e., exactly one of the players S and D has a winning strategy in
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
.
A reformulation of the Immerman game
To facilitate comparison with the formula size games that we introduce in the next section, we give here a reformulation of the Immerman game. Observe first that the winning condition PI can be equivalently stated as
QFSep S wins the game if there exists a quantifier-free formula
$\varphi$
such that
$\mathsf{Sep}(\mathbb{A}_\ell,\mathbb{B}_\ell,\varphi)$
holds. Otherwise D wins.
Indeed, if
$\mathsf{Sep}(\mathbb{A}_\ell,\mathbb{B}_\ell,\varphi)$
holds for some quantifier-free formula
$\varphi$
, then it is obvious that
$s\mapsto t$
cannot be a partial isomorphism for any
$({\mathfrak A},s)\in\mathbb{A}_\ell$
and
$({\mathfrak B},t)\in\mathbb{B}_\ell$
. Conversely, if there are no
$({\mathfrak A},s)\in\mathbb{A}_\ell$
and
$({\mathfrak B},t)\in\mathbb{B}_\ell$
such that
$s\mapsto t$
is a partial isomorphism, then for each pair
$({\mathcal A},{\mathcal B})\in\mathbb{A}_\ell\times\mathbb{B}_\ell$
there is a quantifier-free formula
$\psi_{{\mathcal A},{\mathcal B}}$
such that
${\mathcal A}\models\psi_{{\mathcal A},{\mathcal B}}$
and
${\mathcal B}\not\models\psi_{{\mathcal A},{\mathcal B}}$
, and it is straightforward to check that
$\mathsf{Sep}(\mathbb{A}_\ell,\mathbb{B}_\ell,\varphi)$
holds for
$\varphi:=\bigvee_{{\mathcal A}\in\mathbb{A}_\ell}\bigwedge_{{\mathcal B}\in\mathbb{B}_\ell}\psi_{{\mathcal A},{\mathcal B}}$
.
Note further that the condition QFSep can be true already in some position
$(\mathbb{A}_i,\mathbb{B}_i)$
with
$i<\ell$
. In such a case, S can be declared the winner immediately without the need to continue the play.
Instead of fixing a sequence
$x_1,\ldots,x_\ell$
of variables beforehand, we let S choose in each move a (fresh) variable x. Furthermore, instead of fixing
$\ell$
, and considering the sequence of consecutive positions
$(\mathbb{A}_i,\mathbb{B}_i)$
,
$i\le\ell$
, of the game
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
, we regard
$\ell$
as a dynamic parameter and define the game recursively: after the players have completed the first round of the game
$\mathsf{IG}_\ell(\mathbb{C},\mathbb{D})$
and determined the next pair
$(\mathbb{C}',\mathbb{D}')$
of classes, they continue by playing
$\mathsf{IG}_{\ell-1}(\mathbb{C}',\mathbb{D}')$
.
We are now ready to define the rules of the reformulated Immerman game. In order to separate the new version of the game from the one given in Definition 3, we denote this game by
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
.
Definition 5. The rules of the game
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
are the following.
(1) If there is a quantifier-free formula
$\varphi$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
, the game ends and S wins.
(2) If
$\ell=0$
, and (1) does not hold, the game ends and D wins.
(3) If
$\ell\ge 1$
, but (1) does not hold, then S plays either of the following two moves:
∃-move: S chooses a variable x and a choice function F for
$\mathbb{A}$
, and sets
$\mathbb{A}'=F_x(\mathbb{A})$
,
$\mathbb{B}'=U_x(\mathbb{B})$
and
$\ell'=\ell-1$
.
∀-move: Similar to
$\exists$
-move, but with the roles of
$\mathbb{A}$
and
$\mathbb{B}$
switched.
After the move is completed, S and D continue by playing
$\mathsf{IG}^*(\ell',\mathbb{A}',\mathbb{B}')$
.
Note that D has no active role in the game
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
! Nevertheless, it should be clear that the two games
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
and
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
are equivalent in the sense that S has a winning strategy in the former if and only if he has a winning strategy in the latter. In fact, S can use essentially the same strategy in both games, and he wins the play against the oblivious strategy of D in
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
if and only if he wins the corresponding play in
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
.
4. Formula Size Game
In this section, we first consider more general games that are aimed at characterizing expressive power of sentences of size at most a given bound
$\ell$
. Here, the size of a formula counts the number of atomic formulas, connectives, and quantifiers. The precise definition of the size
$\mathrm{fs}(\varphi)$
of a formula
$\varphi$
of first-order logic is as follows:
\begin{eqnarray*}\mathrm{fs}(\varphi)&=&1\;\mbox{ for atomic $\varphi$}\\\mathrm{fs}(\neg\varphi)&=&\mathrm{fs}(\varphi)+1\\\mathrm{fs}(\varphi\lor\psi)&=&\mathrm{fs}(\varphi)+\mathrm{fs}(\psi)+1\\\mathrm{fs}(\varphi\land\psi)&=&\mathrm{fs}(\varphi)+\mathrm{fs}(\psi)+1\\\mathrm{fs}(\exists x\,\varphi)&=&\mathrm{fs}(\varphi)+1\\\mathrm{fs}(\forall x\,\varphi)&=&\mathrm{fs}(\varphi)+1\end{eqnarray*}
Note that by this definition,
$\mathrm{fs}(\varphi)$
is the number of occurrences of subformulas in
$\varphi$
, which is less than the length
$|\varphi|$
of
$\varphi$
as a string of symbols. It would be straightforward to define
$|\varphi|$
by a similar recursion by modifying the clause for atomic formulas (e.g., setting
$|R(x,y,z)|=8$
and
$|x=y|=3$
) and adding
$+2$
to the clauses of disjunction and conjunction (corresponding to the parentheses). Counting the length of atomic formulas would lead to a finer analysis, and potentially new applications, but we refrain from doing this here.
We are now ready to define the formula size game. The moves of the game reflect directly the corresponding items in Lemma 2.
Definition 6. The rules of the formula size game
$\mathsf{FSG}(\ell,\mathbb{A},\mathbb{B})$
are the following.
(1) If
$\ell=0$
, the game ends and D wins.
(2) If
$\ell\ge 1$
and there is an atomic formula
$\varphi$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
, the game ends and S wins.
(3) If
$\ell\ge 1$
, but (2) does not hold, then S chooses one of the following five types of moves:
￢-move: S sets
$\ell'=\ell-1$
,
$\mathbb{A}'=\mathbb{B}$
and
$\mathbb{B}'=\mathbb{A}$
.
∨-move: S chooses numbers
$m,n\in{\mathbb{N}}$
such that
$m+n+1=\ell$
and classes
$\mathbb{C}$
and
$\mathbb{D}$
such that
$\mathbb{A}=\mathbb{C}\cup \mathbb{D}$
.
D answers by choosing
$(\ell',\mathbb{A}',\mathbb{B}')$
to be either
$(m,\mathbb{C},\mathbb{B})$
or
$(n,\mathbb{D},\mathbb{B})$
.
∧-move: Similar to
$\lor$
-move, but switching the roles of
$\mathbb{A}$
and
$\mathbb{B}$
.
∃-move: S chooses a variable x and a choice function F for
$\mathbb{A}$
, and sets
$\mathbb{A}'=F_x(\mathbb{A})$
,
$\mathbb{B}'=U_x(\mathbb{B})$
and
$\ell'=\ell-1$
.
∀-move: Similar to
$\exists$
-move, but switching the roles of
$\mathbb{A}$
and
$\mathbb{B}$
.
After the move is completed, S and D continue by playing
$\mathsf{FSG}(\ell',\mathbb{A}',\mathbb{B}')$
.
The game
$\mathsf{FSG}(\ell,\mathbb{A},\mathbb{B})$
is a variation of the similar formula size game
${\mathrm{EF}}_\ell(\mathbb{A},\mathbb{B})$
defined by Hella and Väänänen (Reference Hella, Väänänen, Hirvonen, Kontinen, Kossak and Villaveces2015). In
${\mathrm{EF}}_\ell(\mathbb{A},\mathbb{B}),$
formulas are assumed to be in negation normal form, whence there are no
$\lnot\,$
-moves. Furthermore, disjunctions and conjunctions are not counted in the size of formulas in
${\mathrm{EF}}_\ell(\mathbb{A},\mathbb{B})$
; thus, instead of
$m+n+1=\ell$
the condition in
$\lor$
- and
$\land$
-moves is
$m+n=\ell$
.
Theorem 7. (cf. Hella and Väänänen Reference Hella, Väänänen, Hirvonen, Kontinen, Kossak and Villaveces2015). Let
$\mathbb{A}$
and
$\mathbb{B}$
be classes of
$(\tau,V)$
-interpretations, and let
$\ell$
be a positive integer. Then the following conditions are equivalent:
(a) S has a winning strategy in the game
$\mathsf{FSG}(\ell,\mathbb{A},\mathbb{B})$
.(b) There is a formula
$\varphi$
with
$\mathrm{fs}(\varphi)\le \ell$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
.
The equivalence of the conditions (a) and (b) in Theorem 7 is proved by induction on
$\ell$
. In the case
$\ell=0$
, the claim holds since S loses the game
$\mathsf{FSG}(0,\mathbb{A},\mathbb{B})$
immediately, and there are no formulas of size 0.
The induction step is based on the correspondence between the items in Lemma 2 and the types of moves in Definition 6. For example, if S has a winning strategy
$\sigma$
in
$\mathsf{FSG}(\ell,\mathbb{A},\mathbb{B})$
and the first move given by
$\sigma$
is a
$\lnot\,$
-move, then S has a winning strategy in
$\mathsf{FSG}(\ell-1,\mathbb{B},\mathbb{A})$
, and hence by induction hypothesis, there is a formula
$\psi$
such that
$\mathrm{fs}(\psi)\le \ell-1$
and
$\mathsf{Sep}(\mathbb{B},\mathbb{A},\psi)$
. Then by Lemma 2(a),
$\varphi:=\lnot\psi$
is a formula such that
$\mathrm{fs}(\varphi)\le \ell$
and
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
. Conversely, if
$\mathrm{fs}(\varphi)\le\ell$
,
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
holds, and
$\varphi$
is of the form
$\lnot\psi$
, then by Lemma 2(a),
$\mathsf{Sep}(\mathbb{B},\mathbb{A},\psi)$
holds. Hence by induction hypothesis, S has a winning strategy
$\sigma$
in
$\mathsf{FSG}(\ell-1,\mathbb{B},\mathbb{A})$
. Thus, playing first a
$\lnot\,$
-move, and then using
$\sigma$
provides S with a winning strategy in
$\mathsf{FSG}(\ell,\mathbb{A},\mathbb{B})$
.
The cases related to disjunction, conjunction, existential quantifier, universal quantifier, and the corresponding moves are handled in the same way (see Hella and Väänänen Reference Hella, Väänänen, Hirvonen, Kontinen, Kossak and Villaveces2015 for details).
From formula size to number of quantifiers
Starting from the formula size game
$\mathsf{FSG}$
, we derive here a game that characterizes equivalence with respect to the number of quantifiers. This is achieved simply by using the number of quantifiers as a resource parameter instead of the size of formulas.
Remark 8. A similar idea of deriving the Immerman game as a special case of a more general game is pointed out by Carmosino et al. (Reference Carmosino, Fagin, Immerman, Kolaitis, Lenchner and Sengupta2023). Their syntactic game characterizes separability of classes of structures by sentences having a fixed size with respect to a given syntactic measure. As
$\mathrm{fs}(\varphi)$
is an example of a syntactic measure, an alternative version
$\mathsf{FSG}'$
of the formula size game
$\mathsf{FSG}$
can be obtained as a special case of the syntactic game. However, the syntactic game is similar to the Immerman game in the sense that Duplicator has a default optimal strategy. Thus, for any syntactic measure, Duplicator can be completely eliminated from the game; in particular, this concerns the game
$\mathsf{FSG}'$
. On the other hand, Duplicator cannot be eliminated from
$\mathsf{FSG}$
or the game
$\mathsf{NQG}$
for the number of quantifiers that we define below.
Let
$\mathrm{nq}(\varphi)$
be the total number of quantifiers in a formula
$\varphi$
. Clearly
$\mathrm{nq}(\varphi)$
can be defined recursively as follows:
\begin{eqnarray*}\mathrm{nq}(\varphi)&=&{0}\;\mbox{ for atomic $\varphi$}\\\mathrm{nq}(\neg\varphi)&=&\mathrm{nq}(\varphi)\\\mathrm{nq}(\varphi\lor\psi)&=&\mathrm{nq}(\varphi)+\mathrm{nq}(\psi)\\\mathrm{nq}(\varphi\land\psi)&=&\mathrm{nq}(\varphi)+\mathrm{nq}(\psi)\\\mathrm{nq}(\exists x\,\varphi)&=&\mathrm{nq}(\varphi)+1\\\mathrm{nq}(\forall x\,\varphi)&=&\mathrm{nq}(\varphi)+1\end{eqnarray*}
Definition 9. The rules of the number of quantifiers game
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
are the following.
(1) If there is a quantifier-free formula
$\varphi$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
, the game ends and S wins.(2) If
$\ell=0$
, and (1) does not hold, the game ends and D wins.
(3) If
$\ell\ge 1$
, but (1) does not hold, then S chooses one of the following five types of moves:
￢-move: S sets
$\ell'=\ell$
,
$\mathbb{A}'=\mathbb{B}$
and
$\mathbb{B}'=\mathbb{A}$
.
∨-move: S chooses numbers
$m,n\in{\mathbb{N}}$
such that and
$m+n=\ell$
and classes
$\mathbb{C}$
and
$\mathbb{D}$
such that
$\mathbb{A}=\mathbb{C}\cup \mathbb{D}$
.
D answers by choosing
$(\ell',\mathbb{A}',\mathbb{B}')$
to be either
$(m,\mathbb{C},\mathbb{B})$
or
$(n,\mathbb{D},\mathbb{B})$
.
∧-move: Similar to
$\lor$
-move, but switching the roles of
$\mathbb{A}$
and
$\mathbb{B}$
.
∃-move: S chooses a variable x and a choice function F for
$\mathbb{A}$
, and sets
$\mathbb{A}'=F_x(\mathbb{A})$
,
$\mathbb{B}'=U_x(\mathbb{B})$
and
$\ell'=\ell-1$
.
∀-move: Similar to
$\exists$
-move, but switching the roles of
$\mathbb{A}$
and
$\mathbb{B}$
.
After the move is completed, S and D continue by playing
$\mathsf{NQG}(\ell',\mathbb{A}',\mathbb{B}')$
.
Note that the rules of the game
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
are quite different from those of the Immerman game
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
. Intuitively, the former appears to give S more power, as he can use the connective moves in addition to the quantifier moves. However, this additional power does not help S, since using a nontrivial connective move would just be wasting the quantifier resource
$\ell$
. We will prove that S has a winning strategy in one of the games
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
and
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
if and only if he has a winning strategy in both of them.
Before proving the result, we show that any sentence is equivalent to a sentence in prenex normal form with the same number of quantifiers. This also explains why there is no point for S to use connective moves in the game
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
. Here, a formula is in prenex normal form if it is of the form
$Q_1x_1\ldots Q_nx_n\,\psi$
, where
$Q_i\in\{\forall,\exists\}$
for each
$i\in[n]$
, and
$\psi$
is a quantifier free formula. The sequence
$\vec Q\vec x=Q_1x_1\ldots Q_nx_n$
is called a quantifier prefix.
Lemma 10. For any first-order formula
$\varphi$
with
$\mathrm{nq}(\varphi)=\ell,$
there exists a logically equivalent formula of the form
$\vec Q\vec x \,\theta$
, where
$\vec Q\vec x$
is a quantifier prefix of length
$\ell$
and
$\theta$
is a quantifier free formula.
Proof. It is easy to see that the standard procedure of transforming a formula into prenex normal form preserves the number of quantifiers (see, e.g., Ebbinghaus et al. Reference Ebbinghaus, Flum and Thomas1984). Thus, we can simply let
$\vec Q\vec x \,\theta$
to be the result of applying the procedure to
$\varphi$
.
Theorem 11. Let
$\mathbb{A}$
and
$\mathbb{B}$
be classes of
$(\tau,V)$
-interpretations, and let
$\ell$
be a natural number. Then the following conditions are equivalent:
(1) S has a winning strategy in the game
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
.(2) S has a winning strategy in the game
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
.(3) There is a formula
$\varphi$
with
$\mathrm{nq}(\varphi)\le \ell$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
.(4) There is a quantifier prefix
$\vec Q\vec x$
of length at most
$\ell$
and a quantifier-free formula
$\theta$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\vec Q\vec x\,\theta)$
.
Proof.
$(1)\Rightarrow (2)$
: If S has a winning strategy
$\sigma$
in the game
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
, he can use it as such in
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
, as any move given by
$\sigma$
is also a legal move in
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
. Since the winning condition for S is the same in both games,
$\sigma$
is a winning strategy in
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
, too.
The implication
$(2)\Rightarrow (3)$
is proved by induction on
$\ell$
in the same way as the implication (a)
$\Rightarrow$
(b) in Theorem 7.
The implication
$(3)\Rightarrow (4)$
follows directly from Lemma 10.
$(4)\Rightarrow (1)$
: Assume that
$\vec Q\vec x=Q_n x_n\ldots Q_1 x_1$
, where
$n\le\ell$
and
$\theta$
is a quantifier-free formula such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\vec Q\vec x\,\theta)$
. For each
$i\le n$
, let
$(\vec Q\vec x)_i$
denote the end segment
$Q_ix_i\ldots Q_1x_1$
of the prefix
$\vec Q\vec x$
; note that
$(\vec Q\vec x)_n=\vec Q\vec x$
and
$(\vec Q\vec x)_0$
is the empty prefix. We prove by induction on
$i\le n$
that if
$\mathbb{C}$
and
$\mathbb{D}$
are classes of
$(\tau,V\cup\{x_{i+1},\ldots,x_n\})$
-interpretations such that
$\mathsf{Sep}(\mathbb{C},\mathbb{D},(\vec Q\vec x)_i\,\theta)$
, then S has a winning strategy in
$\mathsf{IG}^*(i,\mathbb{C},\mathbb{D})$
.
In the case
$i=0$
,
$(\vec Q\vec x)_i\,\theta=\theta$
is quantifier free, whence S wins the game
$\mathsf{IG}^*(0,\mathbb{C},\mathbb{D})$
immediately. Assume then that
$i>0$
, and the claim holds for
$i-1$
. We describe a move for S in the first round of
$\mathsf{IG}^*(i,\mathbb{C},\mathbb{D})$
and show that it can be extended to a winning strategy in the rest of the game. The move depends on whether
$Q_i$
is
$\exists$
or
$\forall$
as follows.
• If
$Q_i=\exists$
, we let S play a
$\exists$
-move and choose the variable
$x_i$
. Since
$\mathsf{Sep}(\mathbb{C},\mathbb{D},(\vec Q\vec x)_i\,\theta)$
and
$(\vec Q\vec x)_i=\exists x_i(\vec Q\vec x)_{i-1}$
, by Lemma 2(d) there is a choice function F for
$\mathbb{C}$
such that
$\mathsf{Sep}(F_{x_i}(\mathbb{C}),U_{x_i}(\mathbb{D}),(\vec Q\vec x)_{i-1}\,\theta)$
. We let S use this choice function F in the move. By the induction hypothesis, S has a winning strategy in the continuation
$\mathsf{IG}^*(i-1,F_{x_i}(\mathbb{C}),U_{x_i}(\mathbb{D}))$
of the game.• If
$Q_i=\forall$
, S plays a
$\forall$
-move with the variable
$x_i$
and uses Lemma 2(e) for choosing a choice function G for
$\mathbb{D}$
such that
$\mathsf{Sep}(U_{x_i}(\mathbb{C}),G_{x_i}(\mathbb{D}),(\vec Q\vec x)_{i-1}\,\theta)$
holds. A winning strategy for S in the continuation
$\mathsf{IG}^*(i-1,U_{x_i}(\mathbb{C}),G_{x_i}(\mathbb{D}))$
of the game is again given by the induction hypothesis.
Thus, we see that S has a winning strategy in the game
$\mathsf{IG}^*(n,\mathbb{A},\mathbb{B})$
. Since
$n\le\ell$
, it is clear that this strategy is also winning in
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
.
Note that since the
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
is equivalent to the game
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
, the characterization result, Theorem 4, by Immerman (Reference Immerman1981) and Fagin et al. (Reference Fagin, Lenchner, Regan and Vyas2021) is a corollary of Theorem 11.
5. Connection to Monotone Quantifier Game
In this section, we consider the modified Immerman game from another perspective: since D does not make any moves in
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
, the order of moves by S can be freely changed without affecting the winner. Moreover, the choices of S on the class
$\mathbb{A}$
(
$\mathbb{B}$
, respectively) can be replaced by a single move in which he reveals the strategy (i.e., the sequence of choice functions) he uses in these moves. Using these observations as a starting point, we derive a new game that is equivalent to
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
.
Assuming that
$\mathbb{A}$
and
$\mathbb{B}$
consist of single structures, our new game turns out to be a special case of the Ehrenfeucht–Fraïssé game for monotone generalized quantifiers by Krawczyk and Krynicki (Reference Krawczyk, Krynicki, Marek, Srebrny and Zarach1976). Thus, we consider first the case where
$\mathbb{A}$
and
$\mathbb{B}$
are singletons; this also simplifies the presentation considerably. We define a version of the new game for arbitrary classes
$\mathbb{A}$
and
$\mathbb{B}$
in the end of the section and give there a self-contained proof for the corresponding characterization result.
From Immerman game to monotone prefix game on singleton classes
Let
${\mathfrak A}$
and
${\mathfrak B}$
be
$\tau$
-structures for a finite relational vocabulary
$\tau$
. In each play of
$\mathsf{IG}^*(\ell,\{{\mathfrak A}\},\{{\mathfrak B}\})$
, the moves of S determine a quantifier prefix
$\vec Q\vec x= Q_1x_1\ldots Q_\ell x_\ell$
, where
$Q_i=\exists$
(
$Q_i=\forall$
) if the ith move of S is an
$\exists$
-move (
$\forall$
-move, respectively), and
$x_i$
is the variable chosen by S in ith move. We denote by
$E(\vec Q)\subseteq\{1,\ldots,\ell\}$
the set of those indices for which
$Q_i=\exists$
, and by
$U(\vec Q)$
the complement
$\{j\in [\ell]\mid Q_j=\forall\}$
of
$E(\vec Q)$
. Furthermore, we denote the set
$\{x_1,\ldots,x_i\}$
by
$X_i$
for each
$i\le \ell$
.
Let
$F_i$
,
$i\in E(\vec Q)$
, be the choice functions that S uses in his
$\exists$
-moves, and let
$G_j$
,
$j\in U(\vec Q)$
, be the choice functions he uses in his
$\forall$
-moves. Since
${\mathfrak A}$
and
${\mathfrak B}$
are the only structures in the classes we consider, we assume that each
$F_i$
is defined on assignments
$s\colon X_{i-1}\to A$
instead of pairs
$({\mathfrak A},s)$
, and similarly, each
$G_j$
is defined on assignments
$t\colon X_{j-1}\to B$
. Given any sequence
$H_i$
,
$i\in I\subseteq [\ell]$
of choice functions that map assignments
$u\colon X_{i-1}\to C$
to C, where
$C\in\{A,B\}$
, we use the notation
•
$T_\ell(\vec H):=\{u\colon X_\ell\to C\mid u(x_i)=H_i(u\restriction X_{i-1})\text{ for all }i\in I\}$
for the set of assignments arising from
$\vec H=(H_i)_{i\in I}$
.
The outcome of the play, where S plays the sequences
$\vec F=(F_i)_{i\in E(\vec Q)}$
and
$\vec G=(G_j)_{j\in U(\vec Q)}$
, is determined by the two sets
$T_\ell(\vec F)$
and
$T_\ell(\vec G)$
: by Definition 3, S wins the play if and only if there is a quantifier-free formula
$\theta$
such that
$({\mathfrak A},s)\models\theta$
for all
$s\in T_\ell(\vec F)$
and
$({\mathfrak B},t)\not\models\theta$
for all
$t\in T_\ell(\vec G)$
. Equivalently, D wins the play if and only if there are
$s\in T_\ell(\vec F)$
and
$t\in T_\ell(\vec G)$
such that
$s\mapsto t$
is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
.
Observe now that since D does not make any moves in the game
$\mathsf{IG}^*(\ell,\mathbb{A},\mathbb{B})$
, the order of moves by S does not make any difference to the outcome. Thus, we may as well assume that the game is played in the following four steps:
(i) S reveals the quantifier prefix
$\vec Q\vec x=Q_1 x_1\ldots Q_\ell x_\ell$
.(ii) S gives the sequence
$F_i$
,
$i\in E(\vec Q)$
, of choice functions on
${\mathfrak A}$
.(iii) S gives the sequence
$G_j$
,
$j\in U(\vec Q)$
, of choice functions on
${\mathfrak B}$
.(iv) D chooses
$s\in T_\ell(\vec F)$
and
$t\in T_\ell(\vec G)$
.
D wins the game if
$s\mapsto t$
is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
; otherwise S wins.
Step (ii) can be interpreted as S giving a strategy for
$\exists$
in the semantic game of a prenex normal form sentence with prefix
$\vec Q\vec x$
on the structure
${\mathfrak A}$
. Similarly, step (iii) can be seen as S giving a strategy for the other player,
$\forall$
, in the semantic game of the same sentence on the structure
${\mathfrak B}$
.
Definition 12. Let
${\mathfrak A}$
be a structure,
$\vec Q\vec x=Q_1x_1\ldots Q_\ell x_\ell$
a quantifier prefix, and
$\varphi=\vec Q\vec x\,\theta$
a sentence, where
$\theta$
is quantifier free. The semantic game
$\mathsf{SemG}({\mathfrak A},\varphi)$
is played by two players
$\exists$
and
$\forall$
. The game has
$\ell$
rounds, and in each round i one of the players chooses an interpretation
$a_i\in A$
for the variable
$x_i$
: if
$i\in E(\vec Q)$
, then
$\exists$
chooses
$a_i$
, and if
$i\in U(\vec Q)$
, then
$\forall$
chooses
$a_i$
.
$\exists$
wins the game if
$({\mathfrak A},\vec a/\vec x)\models\theta$
; otherwise
$\forall$
wins.
It is well known that the semantic game
$\mathsf{SemG}$
can be used as an alternative to the Tarski truth definition:
${\mathfrak A}\models\vec Q\vec x\,\theta$
if and only if
$\exists$
has a winning strategy in the game
$\mathsf{SemG}({\mathfrak A},\vec Q\vec x\,\theta)$
.
As we mentioned above, in steps (ii) and (iii) S essentially gives strategies for
$\exists$
and
$\forall$
in the semantic games
$\mathsf{SemG}({\mathfrak A},\vec Q\vec x\,{\square})$
and
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
, where
${\square}$
is a placeholder for some quantifier-free formula.Footnote 3 The intuition of steps (i)–(iv) can now be explained as follows: In step (i), S starts by giving the prefix
$\vec Q\vec x$
, and claims that there is a sentence starting with this prefix that separates the classes
$\mathbb{A}$
and
$\mathbb{B}$
. To show this, he gives in step (ii) a strategy
$\vec F$
for
$\exists$
in the semantic game
$\mathsf{SemG}({\mathfrak A},\vec Q\vec x\,{\square})$
, and in step (iii) a strategy
$\vec G$
for
$\forall$
in the semantic game
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
, and claims that there is a quantifier-free formula
$\theta$
such that these strategies are winning with
$\theta$
in place of
${\square}$
. Finally, in step (iv), D challenges the claim of S by picking assignments
$s\in T_\ell(\vec F)$
and
$t\in T_\ell(\vec G)$
and makes the counterclaim that no quantifier-free formula
$\theta$
separates
$({\mathfrak A},s)$
and
$({\mathfrak B},t)$
.
However, we can also look at step (iii) from another perspective: instead of S choosing a strategy for
$\forall$
in the game
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
, we can as well let D choose a strategy
$\vec H=(H_i)_{i\in E(\vec Q)}$
for
$\exists$
in
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
and claim that it is winning for any quantifier-free formula
$\theta$
for which the strategy given by S in step (ii) is winning in
$\mathsf{SemG}({\mathfrak A},\vec Q\vec x\,{\square})$
. Then S challenges this by choosing an assignment
$t\in T_\ell(\vec H)$
and claiming that
$({\mathfrak B},t)\not\models\theta$
for the quantifier-free formula
$\theta$
he meant. Finally, D answers by choosing an assignment
$s\in T_\ell(\vec F)$
and claims that no quantifier-free formula
$\theta$
separates
$({\mathfrak A},s)$
and
$({\mathfrak B},t)$
. Clearly, D is correct in her last claim if and only if
$s\mapsto t$
is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
. Thus, steps (iii) and (iv) can be replaced by the following three steps:
-
(iii’) D gives the sequence
$H_i$
,
$i\in E(\vec Q)$
, of choice functions on
${\mathfrak B}$
. -
(iv’) S chooses
$t\in T_\ell(\vec H)$
. -
(v) D chooses
$s\in T_\ell(\vec F)$
.
The winning condition remains the same.
Before a formal definition of the game that arises from steps (i), (ii), (iii’), (iv’), and (v), we encode the information contained in the sequences
$\vec F$
and
$\vec H$
into relations
$R_{\vec F}\subseteq A^\ell$
and
$R_{\vec H}\subseteq B^\ell$
, defined as follows:
•
$R_{\vec F}:=\{(a_1,\ldots,a_\ell)\in A^\ell\mid\{(x_1,a_1),\ldots,(x_\ell,a_\ell)\}\in T_\ell(\vec F)\}$
,•
$R_{\vec H}:=\{(b_1,\ldots,b_\ell)\in B^\ell\mid \{(x_1,b_1),\ldots,(x_\ell,b_\ell)\}\in T_\ell(\vec H)\}$
.
Observe now that, by their definition, relations of the form
$R_{\vec F}$
have the property that
$(A,R_{\vec F})\models\vec Q\vec x\,R(\vec x)$
(and similarly
$(B,R_{\vec H})\models\vec Q\vec x\,R(\vec x)$
). Conversely, if
$R_A\subseteq A^\ell$
is a relation such that
$(A,R_A)\models\vec Q\vec x\,R(\vec x)$
, then there is a strategy
$\vec F$
for
$\exists$
in the semantic game
$\mathsf{SemG}({\mathfrak A},\vec Q\vec x\,{\square})$
such that
$R_{\vec F}\subseteq R_A$
. Thus, we can assume that in step (ii), S chooses a relation
$R_A\subseteq A^\ell$
such that
$(A,R_A)\models\vec Q\vec x\,R(\vec x)$
instead of the sequence
$\vec F$
of choice functions, and similarly D chooses in (iii’) a relation
$R_B\subseteq B^\ell$
such that
$(B,R_B)\models\vec Q\vec x\,R(\vec x)$
.
Thus, we have arrived to the following alternative game for the number of quantifiers in the case of singleton classes
$\mathbb{A}=\{{\mathfrak A}\}$
and
$\mathbb{B}=\{{\mathfrak B}\}$
.
Definition 13. The monotone prefix game
$\mathsf{MPG}(\ell,{\mathfrak A},{\mathfrak B})$
is played by S and D, and it has the following rules.
(1) S chooses a quantifier prefix
$\vec Q\vec x=Q_1x_1\ldots Q_\ell x_\ell$
.(2) S chooses a relation
$R_A\subseteq A^\ell$
such that
$(A,R_A)\models\vec Q\vec x\,R(\vec x)$
.(3) D chooses a relation
$R_B\subseteq B^\ell$
such that
$(B,R_B)\models\vec Q\vec x\,R(\vec x)$
.(4) S chooses a tuple
$\vec b=(b_1,\ldots,b_\ell)\in R_B$
.(5) D chooses a tuple
$\vec a=(a_1,\ldots,a_\ell)\in R_A$
.
D wins the game if the mapping
$\vec a\mapsto\vec b$
is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
. Otherwise S wins the game.
The reason for calling this game monotone prefix game is that the moves (2)–(5) form one round of the well-known Ehrenfeucht–Fraïssé game for monotone generalized quantifiers, due to Krawczyk and Krynicki (Reference Krawczyk, Krynicki, Marek, Srebrny and Zarach1976). Indeed, any quantifier prefix
$\vec Q\vec x=Q_1x_1\ldots Q_\ell x_\ell$
can be seen as a generalized quantifier
$Q_K$
, where the defining class K consists of all structures (C,R) such that
$R\subseteq C^\ell$
and
$(C,R)\models \vec Q\vec x\, R(\vec x)$
. The quantifier
$Q_K$
is monotone, i.e., for any
$(C,R)\in K$
, if
$R\subseteq P\subseteq C^\ell$
, then
$(C,P)\in K$
. From the characterization theorem (see Krawczyk and Krynicki Reference Krawczyk, Krynicki, Marek, Srebrny and Zarach1976) for monotone quantifiers, it follows directly that if D has a winning strategy in
$\mathsf{MPG}(\ell,{\mathfrak A},{\mathfrak B})$
after S has chosen a prefix
$\vec Q\vec x$
, then any sentence of the form
$\vec Q\vec x\,\theta$
that is true in
${\mathfrak A}$
is also true in
${\mathfrak B}$
. Note that if this holds for all prefixes
$\vec Q\vec x$
of length
$\ell$
, then
${\mathfrak A}$
and
${\mathfrak B}$
satisfy exactly the same sentences of form
$\vec Q\vec x\,\theta$
, as the negation of
$\vec Q\vec x\,\theta$
is equivalent to
$\vec Q^d\vec x\,\lnot\theta$
, where
$\vec Q^d\vec x$
is the dual prefix of
$\vec Q\vec x$
(i.e.,
$\vec Q^d$
is obtained from
$\vec Q$
by replacing each
$\exists$
by
$\forall$
, and vice versa).
Thus, we see that
$\mathsf{MPG}(\ell,{\mathfrak A},{\mathfrak B})$
characterizes the equivalence of
${\mathfrak A}$
and
${\mathfrak B}$
with respect to all sentences containing (at most)
$\ell$
quantifiers. Formulating this again from the point of view of S, we obtain the following result.
Theorem 14. Let
${\mathfrak A}$
and
${\mathfrak B}$
be
$\tau$
-structures, and let
$\ell$
be a natural number. Then the following conditions are equivalent:
(1) S has a winning strategy in the game
$\mathsf{MPG}(\ell,{\mathfrak A},{\mathfrak B})$
.(2) There is a formula
$\varphi$
with
$\mathrm{nq}(\varphi)\le \ell$
such that
$\mathsf{Sep}(\{{\mathfrak A}\},\{{\mathfrak B}\},\varphi)$
.
Monotone prefix game on arbitrary classes
We end this section by generalizing the game
$\mathsf{MPG}$
from single structures to arbitrary classes
$\mathbb{A}$
and
$\mathbb{B}$
of structures. Clearly step (2) in Definition 13 has to be replaced by S choosing a relation
$R_{\mathfrak A}$
for every
${\mathfrak A}\in\mathbb{A}$
. However, in step (3) it suffices that D chooses a relation
$R_{\mathfrak B}$
for a single structure
${\mathfrak B}\in\mathbb{B}$
. This is because in steps (1) and (2) S basically commits to a fixed sentence
$\vec Q\vec x\,\theta$
that he claims to separate the classes
$\mathbb{A}$
and
$\mathbb{B}$
, and hence D only needs to demonstrate that
${\mathfrak B}\models\vec Q\vec x\,\theta$
holds for one of the structures
${\mathfrak B}\in\mathbb{B}$
. Similarly, in step (5) D only needs to choose a tuple
$\vec a$
from one of the structures
${\mathfrak A}\in\mathbb{A}$
.
Definition 15. Let
$\mathbb{A}$
and
$\mathbb{B}$
be classes of
$\tau$
-structures. The monotone prefix game
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
is played by S and D, and it has the following rules.
(1) S chooses a quantifier prefix
$\vec Q\vec x=Q_1x_1\ldots Q_\ell x_\ell$
.(2) For each
${\mathfrak A}\in\mathbb{A}$
, S chooses a relation
$R_{\mathfrak A}\subseteq A^\ell$
such that
$(A,R_{\mathfrak A})\models\vec Q\vec x\,R(\vec x)$
.(3) D chooses
${\mathfrak B}\in\mathbb{B}$
and a relation
$R_{\mathfrak B}\subseteq B^\ell$
such that
$(B,R_{\mathfrak B})\models\vec Q\vec x\,R(\vec x)$
.(4) S chooses a tuple
$\vec b=(b_1,\ldots,b_\ell)\in R_{\mathfrak B}$
.(5) D chooses
${\mathfrak A}\in\mathbb{A}$
and a tuple
$\vec a=(a_1,\ldots,a_\ell)\in R_{\mathfrak A}$
.
D wins the game if the mapping
$\vec a\mapsto\vec b$
is a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
. Otherwise S wins the game.
Note that the rules of the game
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
are quite asymmetric with respect to the classes
$\mathbb{A}$
and
$\mathbb{B}$
. In spite of this, the game characterizes the separability of
$\mathbb{A}$
and
$\mathbb{B}$
by a sentence with n quantifiers, which is a symmetric condition with respect to
$\mathbb{A}$
and
$\mathbb{B}$
.
Theorem 16. Let
$\mathbb{A}$
and
$\mathbb{B}$
be classes of
$\tau$
-structures, and let
$\ell$
be a natural number. Then the following conditions are equivalent:
(1) S has a winning strategy in the game
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
.(2) There is a formula
$\varphi$
with
$\mathrm{nq}(\varphi)\le \ell$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
.
Proof. Assume first that (1) holds. Let
$\vec Q\vec x$
be the prefix and let
$R_{\mathfrak A}$
,
${\mathfrak A}\in\mathbb{A}$
, be the relations given by the winning strategy of S. For each structure
${\mathfrak A}\in\mathbb{A}$
and tuple
$\vec a\in R_{\mathfrak A}$
, let
$\theta_{{\mathfrak A},\vec a}(\vec x)$
be the complete atomic type of
$\vec a$
(i.e.,
$\theta_{{\mathfrak A},\vec a}(\vec x)$
is the conjunction of all atomic and negated atomic formulas
$\eta(\vec x)$
such that
$({\mathfrak A},\vec a/\vec x)\models\eta(\vec x)$
), and let
$\theta:=\bigvee_{{\mathfrak A}\in\mathbb{A},\vec a\in R_{\mathfrak A}}\theta_{{\mathfrak A},\vec a}(\vec x)$
.Footnote 4
We show now that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
holds for
$\varphi:=\vec Q\vec x\,\theta$
. Let
${\mathfrak A}\in\mathbb{A}$
and consider the semantic game
$\mathsf{SemG}({\mathfrak A},\varphi)$
. Since
$(A,R_{\mathfrak A})\models\vec Q\vec x\,R(\vec x)$
,
$\exists$
has a strategy guaranteeing that
$\vec a\in R_{\mathfrak A}$
for the tuple
$\vec a$
produced by the moves of
$\exists$
and
$\forall$
. Using this strategy, she wins the game
$\mathsf{SemG}({\mathfrak A},\varphi)$
, since clearly
$({\mathfrak A},\vec a/\vec x)\models\theta$
for every
$\vec a\in R_{\mathfrak A}$
. Thus,
${\mathfrak A}\models\varphi$
for every
${\mathfrak A}\in\mathbb{A}$
.
We still need to show that
${\mathfrak B}\not\models\varphi$
for all
${\mathfrak B}\in\mathbb{B}$
. Assume toward contradiction that
${\mathfrak B}\in\mathbb{B}$
and
${\mathfrak B}\models\varphi$
. Then choosing
${\mathfrak B}\in\mathbb{B}$
and the relation
$R_{\mathfrak B}:=\{\vec b\in B^\ell\mid ({\mathfrak B},\vec b/\vec x)\models\theta\}$
is a legal move for D in step (3) of the game
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
. Let
$\vec b\in R_{\mathfrak B}$
be the response of S given by his winning strategy. By the definition of
$\theta,$
there is a structure
${\mathfrak A}\in\mathbb{A}$
and a tuple
$\vec a\in R_{\mathfrak A}$
such that
$({\mathfrak B},\vec b/\vec x)\models\theta_{{\mathfrak A},\vec a}(\vec x)$
. Let
${\mathfrak A}$
and
$\vec a$
be the response of D in step (5) of the game
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
. Since S has used his winning strategy, the mapping
$\vec a\mapsto\vec b$
is not a partial isomorphism
${\mathfrak A}\to{\mathfrak B}$
. But this is impossible since
$({\mathfrak B},\vec b/\vec x)\models\theta_{{\mathfrak A},\vec a}(\vec x)$
implies that
$\vec b$
satisfies exactly the same atomic and negated atomic formulas as
$\vec a$
.
Assume then that (2) holds. We describe a winning strategy for S in the game
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
. Note first that by Theorem 11, there is a quantifier prefix
$\vec Q\vec x$
of length
$\ell$
and a quantifier-free formula
$\theta$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\vec Q\vec x\,\theta)$
. Thus, for each
${\mathfrak A}\in\mathbb{A}$
we have
$(A,R_{\mathfrak A})\models\vec Q\vec x\,R(\vec x)$
, where
$R_{\mathfrak A}$
is the relation
$\{\vec a\in A^\ell\mid ({\mathfrak A},\vec a/\vec x)\models\theta\}$
. We let S use the prefix
$\vec Q\vec x$
in step (1), and the relations
$R_{\mathfrak A}$
,
${\mathfrak A}\in\mathbb{A}$
, in step (2) of his strategy. Assume now that D responds by
${\mathfrak B}\in\mathbb{B}$
and
$R_{\mathfrak B}$
in step (3) of the game. Since
$(B,R_{\mathfrak B})\models\vec Q\vec x\,R(\vec x)$
, but
${\mathfrak B}\not\models\vec Q\vec x\,\theta$
, there must exist a tuple
$\vec b\in R_{\mathfrak B}$
such that
$({\mathfrak B},\vec b/\vec x)\not\models\theta$
. We let S use this tuple
$\vec b$
as his response in step (4) of the game. Since
$({\mathfrak A},\vec a/\vec x)\models\theta$
for all
${\mathfrak A}\in\mathbb{A}$
and
$\vec a\in R_{\mathfrak A}$
, the mapping
$\vec a\mapsto\vec b$
cannot be a partial isomorphism irrespective of the tuple
$\vec a$
chosen by D in step (5) of the game. Thus, the strategy we have described is indeed winning for S.
6. Prenex Normal Form Game
In the games of the previous section, the players produce assignments in a “parallel way” by giving strategies in the semantic game. An alternative game is obtained by using a sequential approach: we let S and D play the semantic game repeatedly until a large enough set of assignments has been formed.
Definition 17. Let
$\mathbb{A}$
and
$\mathbb{B}$
be classes of
$\tau$
-structures. The prenex normal form game
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
is played between two players, S and D, and it is played as follows:
(1) S chooses a quantifier prefix
$\vec Q\vec x=Q_1x_1\ldots Q_\ell x_\ell$
.(2) S and D play the semantic game for the prefix
$\vec Q\vec x$
repeatedly on structures in
$\mathbb{A}$
; S plays in the role of
$\exists$
and D in the role of
$\forall$
. In each repetition i, D first chooses
${\mathfrak A}_i\in\mathbb{A}$
, and then S and D play
$\mathsf{SemG}({\mathfrak A}_i,\vec Q\vec x\,{\square})$
. Let
$s_i\colon X_\ell\to A_i$
be the assignment formed by the choices of S and D. If
$s_j\mapsto s_i$
is not a partial isomorphism
${\mathfrak A}_j\to{\mathfrak A}_i$
for any
$j<i$
, then S and D continue to play the next repetition
$i+1$
of the semantic game. Otherwise, they move to (3).
(3) D chooses
${\mathfrak B}\in\mathbb{B}$
and S and D play the semantic game
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
once; this time S plays in the role of
$\forall$
and D in the role of
$\exists$
. Let
$t\colon X_\ell\to B$
be the assignment formed by the choices of S and D.
The result of the game is the sequence
$({\mathfrak A}_1,s_1),\ldots,({\mathfrak A}_r,s_r),({\mathfrak B},t)$
, where r is the number of repetitions of the semantic game in step (2). D wins the game if
$s_i\mapsto t$
is a partial isomorphism
${\mathfrak A}_i\to{\mathfrak B}$
for some
$1\le i\le r$
. Otherwise S wins.
Note that since the vocabulary
$\tau$
of the classes
$\mathbb{A}$
and
$\mathbb{B}$
is finite and relational, the number of repetitions of
$\mathsf{SemG}({\mathfrak A},\vec Q\vec x\,{\square})$
in step (2) is always finite. Indeed, it is bounded by
$N_{\mathrm{at}}(\tau,\ell)+1$
, where
$N_{\mathrm{at}}(\tau,\ell)$
is the number of complete atomic types of
$(\tau,X_\ell)$
-interpretations. Clearly,
$N_{\mathrm{at}}(\tau,\ell)$
is at most
$2^{m(\tau,\ell)}$
, where
$m(\tau,\ell)$
is the number of atomic
$\tau$
-formulas with variables in
$\{x_1,\ldots,x_\ell\}$
.
The authors of the present paper defined the prenex normal form game for a pair
$({\mathfrak A},{\mathfrak B})$
of structures and a fixed quantifier prefix
$\vec Q\vec x$
(i.e., without the first move (1) of S) some 20 years ago and proved in an unpublished manuscript that it characterizes the preservation of the truth of all sentences of the form
$\vec Q\vec x\,\theta$
. We denote this version of the game by
$\mathsf{PNFG}(\vec Q\vec x,{\mathfrak A},{\mathfrak B})$
, and we write
${\mathfrak A}\Rrightarrow_{\vec Q}{\mathfrak B}$
if
${\mathfrak A}\models\vec Q\vec x\,\theta$
implies
${\mathfrak B}\models\vec Q\vec x\,\theta$
for every quantifier-free formula
$\theta$
.
Theorem 18. (Hella and Luosto Reference Hella and Luosto1999, unpublished).
${\mathfrak A}\Rrightarrow_{\vec Q}{\mathfrak B}$
if and only if D has a winning strategy in the game
$\mathsf{PNFG}(\vec Q\vec x,{\mathfrak A},{\mathfrak B})$
.
We adapt here our proof of Theorem 18 to classes
$\mathbb{A}$
and
$\mathbb{B}$
of structures. Thus, we denote the prenex normal form game with a fixed quantifier prefix
$\vec Q\vec x$
on
$\mathbb{A}$
and
$\mathbb{B}$
by
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
, and we write
$\mathbb{A}\Rrightarrow_{\vec Q}\mathbb{B}$
if the implication
• if
${\mathfrak A}\models\vec Q\vec x\,\theta$
for all
${\mathfrak A}\in\mathbb{A}$
, then
${\mathfrak B}\models\vec Q\vec x\,\theta$
for some
${\mathfrak B}\in\mathbb{B}$
holds for every quantifier-free formula
$\theta$
. In other words,
$\mathbb{A}\Rrightarrow_{\vec Q}\mathbb{B}$
if and only if
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\vec Q\vec x\,\theta)$
does not hold for any quantifier-free formula
$\theta$
. Theorem 18 is now a special case of the following result.
Lemma 19.
$\mathbb{A}\Rrightarrow_{\vec Q}\mathbb{B}$
if and only if D has a winning strategy in the game
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
.
Proof. Assume first that
$\mathbb{A}\Rrightarrow_{\vec Q}\mathbb{B}$
. Then D has the following winning strategy in the game
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
.
(i) D chooses an arbitrary structure
${\mathfrak A}_1\in\mathbb{A}$
and uses an arbitrary strategy in the semantic game
$\mathsf{SemG}({\mathfrak A}_1,\vec Q\vec x\,{\square})$
.(ii) Assume that S and D have played i repetitions of the semantic game for
$\vec Q\vec x$
,
${\mathfrak A}_1,\ldots,{\mathfrak A}_i\in\mathbb{A}$
are the structures chosen by D, and
$s_1\colon X_\ell\to A_1,\ldots,s_i\colon X_\ell\to A_i$
are the corresponding assignments. Assume further that
$s_j\mapsto s_i$
is not a partial isomorphism
${\mathfrak A}_j\to{\mathfrak A}_i$
for any
$1\le j<i$
. Thus, according to the rules of the game, S and D play a further repetition of the semantic game for
$\vec Q\vec x$
. The strategy of D in this repetition depends on the truth of the sentence
$\varphi_i:=\vec Q\vec x\,\bigvee_{1\le j\le i}\theta_j(\vec x)$
in the structures
${\mathfrak A}\in\mathbb{A}$
, where
$\theta_j(\vec x)$
is the complete atomic type of
$s_j$
.(a) If
${\mathfrak A}\not\models\varphi_i$
for some
${\mathfrak A}\in\mathbb{A}$
, then
$\forall$
has a winning strategy in the game
$\mathsf{SemG}({\mathfrak A},\varphi_i)$
, and we let D choose
${\mathfrak A}_{i+1}={\mathfrak A}$
and use this winning strategy in the game
$\mathsf{SemG}({\mathfrak A}_{i+1},\vec Q\vec x\,{\square})$
.(b) If
${\mathfrak A}\models\varphi_i$
for all
${\mathfrak A}\in\mathbb{A}$
, then we let D choose an arbitrary structure
${\mathfrak A}_{i+1}\in\mathbb{A}$
and use an arbitrary strategy in the game
$\mathsf{SemG}({\mathfrak A}_{i+1},\vec Q\vec x\,{\square})$
.
(iii) Assume then that r repetitions of the semantic game for
$\vec Q\vec x$
have been played, and
$s_i\mapsto s_r$
is a partial isomorphism
${\mathfrak A}_i\to{\mathfrak A}_r$
for some
$1\le i<r$
. Thus, S and D continue by playing the game
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
for some
${\mathfrak B}\in\mathbb{B}$
once.Observe now that
${\mathfrak A}\models\varphi_{r-1}$
for all
${\mathfrak A}\in\mathbb{A}$
, since otherwise according to case (ii)(a), D would have used the winning strategy of
$\forall$
in
$\mathsf{SemG}({\mathfrak A}_r,\varphi_{r-1})$
, and thus guaranteed that
$({\mathfrak A}_r,s_r)\not\models\bigvee_{1\le j<r}\theta_j(\vec x)$
which clearly implies that
$s_i\mapsto s_r$
cannot be a partial isomorphism
${\mathfrak A}_i\to{\mathfrak A}_r$
for any
$1\le i< r$
.Since
$\mathbb{A}\Rrightarrow_{\vec Q}\mathbb{B}$
and
${\mathfrak A}\models\varphi_{r-1}$
for all
${\mathfrak A}\in\mathbb{A}$
, there is
${\mathfrak B}\in\mathbb{B}$
such that
${\mathfrak B}\models\varphi_{r-1}$
, and consequently
$\exists$
has a winning strategy
$\sigma$
in the game
$\mathsf{SemG}({\mathfrak B},\varphi_{r-1})$
. We let D choose this
${\mathfrak B}$
in step (3) of the game
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
and use the strategy
$\sigma$
in the game
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
. Let
$t\colon X_\ell\to B$
be the assignment arising from the moves of S and D.
To conclude the proof of the first implication, observe that since D plays the game
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
by using a winning strategy of
$\exists$
in
$\mathsf{SemG}({\mathfrak B},\varphi_{r-1})$
, it holds that
$({\mathfrak B},t)\models\bigvee_{1\le j<r}\theta_j(\vec x)$
, and hence
$({\mathfrak B},t)\models\theta_j(\vec x)$
for some
$1\le j<r$
. Clearly, this means that
$s_j\mapsto t$
is a partial isomorphism
${\mathfrak A}_j\to{\mathfrak B}$
. Thus, the strategy of D we described is indeed a winning strategy.
Assume then that
$\mathbb{A}\not\Rrightarrow_{\vec Q}\mathbb{B}$
. We show that S has a winning strategy in the game
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
, whence D cannot have one. By the assumption there is a sentence
$\varphi$
of the form
$\vec Q\vec x\,\theta$
with
$\theta$
quantifier free such that
${\mathfrak A}\models\varphi$
for all
${\mathfrak A}\in\mathbb{A}$
and
${\mathfrak B}\not\models\varphi$
for all
${\mathfrak B}\in\mathbb{B}$
. Thus,
$\exists$
has a winning strategy in the semantic game
$\mathsf{SemG}({\mathfrak A},\varphi)$
for all
${\mathfrak A}\in\mathbb{A}$
, while
$\forall$
has a winning strategy in
$\mathsf{SemG}({\mathfrak B},\varphi)$
for all
${\mathfrak B}\in\mathbb{B}$
. We let S use the first winning strategy in all the repetitions of the semantic game for
$\vec Q\vec x$
on structures
${\mathfrak A}\in\mathbb{A}$
, and the second winning strategy in the final semantic game
$\mathsf{SemG}({\mathfrak B},\vec Q\vec x\,{\square})$
on the structure
${\mathfrak B}\in\mathbb{B}$
chosen by D.
Let
$({\mathfrak A}_1,s_1),\ldots,({\mathfrak A}_r,s_r),({\mathfrak B},t)$
be the result of the game. The strategy of S described above guarantees that
$({\mathfrak A}_i,s_i)\models\theta$
for all
$1\le i\le r$
, and
$({\mathfrak B},t)\not\models\theta$
. Thus, none of the mappings
$s_i\mapsto t$
,
$1\le i\le r$
, is a partial isomorphism
${\mathfrak A}_i\to{\mathfrak B}$
, and hence S wins the game
$\mathsf{PNFG}(\vec Q\vec x,{\mathfrak A},{\mathfrak B})$
.
Corollary 20. Let
$\mathbb{A}$
and
$\mathbb{B}$
be classes of
$\tau$
-structures, and let
$\ell$
be a natural number. Then the following conditions are equivalent:
(1) S has a winning strategy in the game
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
.(2) There is a sentence
$\varphi$
with
$\mathrm{nq}(\varphi)\le \ell$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
.
Proof. If S has a winning strategy in
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
, then he has one in
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
, where
$\vec Q\vec x$
is the quantifier prefix he uses in step (1) of
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
. Then D cannot have a winning strategy in
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
, whence by Lemma 19,
$\mathbb{A}\not\Rrightarrow_{\vec Q}\mathbb{B}$
. Thus, there is a sentence
$\varphi$
of the form
$\vec Q\vec x\, \theta$
with
$\theta$
quantifier free such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
, and clearly
$\mathrm{nq}(\varphi)=\ell$
.
Assume then that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
holds for some sentence
$\varphi$
with
$\mathrm{nq}(\varphi)\le\ell$
. By Theorem 11, we can assume that
$\varphi$
is of the form
$\vec Q\vec x\, \theta$
for some quantifier-free formula
$\theta$
. Then
$\mathbb{A}\not\Rrightarrow_{\vec Q}\mathbb{B}$
, and hence, by Lemma 19, S has a winning strategy in
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
. Thus, S is guaranteed to win the game
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
, if he starts in step (1) by giving the prefix
$\vec Q\vec x$
(by adding dummy variables we can assume that the length of
$\vec Q\vec x$
is
$\ell$
), and then continues in steps (2) and (3) by his winning strategy in
$\mathsf{PNFG}(\vec Q\vec x,\mathbb{A},\mathbb{B})$
.
We end this section by giving an example that illustrates the use of the prenex normal form game
$\mathsf{PNFG}(\vec Q\vec x,{\mathfrak A},{\mathfrak B})$
for prefixes
$\vec Q\vec x$
with one quantifier alternation on linearly ordered sets
${\mathfrak A}$
and
${\mathfrak B}$
.
Example 21. Let k and
$\ell$
be positive integers. We consider the game
$\mathsf{PNFG}({\vec{Q}}{\vec{z}},{\mathfrak A},{\mathfrak B})$
between finite linearly ordered sets
${\mathfrak A}=(A,\le^{\mathfrak A})$
and
${\mathfrak B}=(B,\le^{\mathfrak B})$
where
${\vec{Q}}{\vec{z}}$
is the prefix
${\forall}^k{\vec{x}}\,{\exists}^\ell{\vec{y}}:={\forall} x_1\ldots{\forall} x_k{\exists} y_1\ldots{\exists} y_\ell$
. We assume all the way that both
${\mathfrak A}$
and
${\mathfrak B}$
are of size at least k. Let us call either of the structures considered large if it has at least
$(k+1)\ell$
elements, and small, otherwise. The rationale behind this bound is that if we choose k elements from a large structure, then removing these elements divides the structure in at most
$k+1$
(possibly empty) intervals, and at least one of them has at least
$\lceil((k+1)\ell-k)/(k+1)\rceil=\ell$
elements. On the other hand, from a small structure one can choose k points such that all the resulting
$k+1$
intervals have less than
$\ell$
elements.
We consider the following three cases according to the sizes of
${\mathfrak A}$
and
${\mathfrak B}$
.
(1) Assume first that
$|A|\le|B|$
. We describe a winning strategy for D in the game
$\mathsf{PNFG}({\forall}^k{\vec{x}}\,{\exists}^\ell{\vec{y}},{\mathfrak A},{\mathfrak B})$
. In the first phase of the game, D plays in a canonical way: As the players play the semantic game
$\mathsf{SemG}({\mathfrak A},{\forall}^k{\vec{x}}\,{\exists}^\ell{\vec{y}}\,{\square})$
where D assumes the role of
${\forall}$
, she is to choose a k-tuple
${\vec{a}}_j=(a_{j,1},\ldots,a_{j,k})$
during each round, after which S chooses an
$\ell$
-tuple
${\vec{c}}_j=(c_{j,1},\ldots,c_{j,l})$
. In order to do this, she fixes an order on
$A^k$
, e.g., the lexicographic order, before the rounds. When round j is played, D plays the least unused tuple
${\vec{a}}_j$
for which S cannot make his choice
${\vec{c}}_j\in A^\ell$
in such a way that
${\vec{a}}_i{\vec{c}}_i\mapsto {\vec{a}}_j{\vec{c}}_j$
is a partial isomorphism for some
$i<j$
. If there is no such choice for D, then she repeats the previous choice and allows the play to proceed to the second phase.In the second phase of the game, the roles have switched and the semantic game
$\mathsf{SemG}({\mathfrak B},{\forall}^k{\vec{x}}\,{\exists}^\ell{\vec{y}}\,{\square})$
is to be played once, with S as
${\forall}$
and D as
${\exists}$
. So S chooses
${\vec{b}}=(b_1,\ldots,b_k)\in B^k$
, and D has to find a right answer
${\vec{d}}\in B^\ell$
against this choice. The elements of
${\vec{b}}$
divide the set
$B\smallsetminus\{b_1,\ldots,b_k\}$
into at most
$k+1$
(possibly empty) intervals
$\Gamma_0,\ldots,\Gamma_r$
. Since
$k\le|A|\le|B|$
, there is a tuple
${\vec{a}}^{\,*}\in A^k$
such that for some embedding
$q\colon {\mathfrak A}\to {\mathfrak B}$
, q maps
${\vec{a}}^{\,*}$
to
${\vec{b}}$
. D has not necessarily played
${\vec{a}}^{\,*}$
during any round, but in any case, there has to be some round j of the first phase such that there is a partial isomorphism p from
${\mathfrak A}$
to
${\mathfrak A}$
with the following property: p maps
${\vec{a}}_j$
to
${\vec{a}}^{\,*}$
and
${\vec{c}}_j\in\mathrm{dom}(p)^\ell$
. Now D chooses
${\vec{d}}=q(p({\vec{c}}_j))$
, and
$q\circ p$
is obviously a partial isomorphism that shows that D has won.(2) Assume then that
${\mathfrak A}$
and
${\mathfrak B}$
are both large. A similar strategy as in previous case wins for D again. In the first phase, D plays canonically, exactly as before. In the only round of the second phase, suppose S has chosen
${\vec{b}}=(b_1,\ldots,b_k)\in B^k$
. Again,
${\vec{b}}$
determines a division of the set
$B\smallsetminus\{b_1,\ldots,b_k\}$
into at most
$k+1$
possibly empty intervals
$\Gamma_0,\ldots,\Gamma_r$
. For simplicity, we may assume that now
$|A|>|B|$
. By the pigeonhole argument explained in the first paragraph of the example, there is some
$i^*\in\{0,\ldots,r\}$
with
$|\Gamma_{i^*}|\ge \ell$
. This ensures that D can find
${\vec{a}}^{\,*}\in A^k$
such that
${\vec{a}}^{\,*}$
can be mapped to
${\vec{b}}$
by some partial isomorphism
$q_0$
and that the following holds: Considering the division
$\Delta_0,\ldots,\Delta_r$
in
${\mathfrak A}$
induced by
${\vec{a}}^{\,*}$
in
$A\smallsetminus\{a^*_1,\ldots,a^*_k\}$
, we have
$|\Delta_i|=|\Gamma_i|$
or simultaneously
$|\Delta_i|\ge\ell$
and
$|\Gamma_i|\ge\ell$
, for every
$i\in\{0,\ldots,r\}$
. (We may put all the extra elements in
$\Delta_{i^*}$
.) As in the previous case, we can find a round j and a partial isomorphism p with
${\vec{a}}_j\mapsto{\vec{a}}^{\,*}$
and
${\vec{c}}_j\in\mathrm{dom}(p)^\ell$
, where
${\vec{c}}_j=(c_{j,1},\ldots,c_{j,\ell})\in A^\ell$
is the tuple chosen by S in round j. Note that for every
$i\in\{0,\ldots r\}$
, we have that the set
$\{p(c_{j,1}),\ldots,p(c_{j,\ell})\}\cap\Delta_i$
has at most
$\ell$
elements, so that there certainly exists a partial isomorphism q extending
$q_0$
with
$\{p(c_{j,1}),\ldots,p(c_{j,\ell})\}\subseteq\mathrm{dom}(q)$
. Clearly, D wins the game by playing
${\vec{d}}=q(p({\vec{c}}_j))$
.(3) The remaining case is that
${\mathfrak B}$
is small and that
$|A|>|B|$
. Then S has a winning strategy. The smallness of
${\mathfrak B}$
means that
$|B| \le (k+1)(\ell-1)+k$
, which implies that there is a strictly ascending sequence
${\vec{b}}=(b_1,\ldots,b_k)\in B^k$
dividing the set
$B\smallsetminus\{b_1,\ldots,b_k\}$
into (possibly empty) intervals
$\Gamma_0,\ldots,\Gamma_k$
, all of which have size less than
$\ell$
. S plans to play this sequence in the second phase. Suppose that D plays the sequence
${\vec{a}}_j=(a_{j,1},\ldots,a_{j,k})\in A^k$
during a round j of the first phase. We may assume that the tuple
${\vec{a}}_j$
is strictly increasing, otherwise S replies arbitrarily. Let
$\Delta_0,\ldots,\Delta_k$
be the intervals of the induced division of
$A\smallsetminus\{a_{j,1},\ldots,a_{j,k}\}$
. As
$|A|>|B|$
, there is
$i\in\{0,\ldots,k\}$
with
$|\Delta_i|>|\Gamma_i|$
. Also
$m=|\Gamma_i|<\ell$
, so S chooses the tuple
${\vec{c}}_j=(c_{j,1},\ldots,c_{j,k})$
so that the first
$m+1\le \ell$
elements
$c_{j,1},\ldots,c_{j,m+1}$
are different elements of
$\Delta_i$
. Supposing now S moves
${\vec{b}}\in B^k$
in the second phase of the play, it is clear that D has no reply
${\vec{d}}\in B^\ell$
such that
${\vec{a}}_j{\vec{c}}_j\mapsto{\vec{b}}{\vec{d}}$
is a partial isomorphism for any round j of the first phase.
Summarizing, assuming that
${\mathfrak A}$
and
${\mathfrak B}$
are finite linearly ordered sets with
$|A|,|B|\ge k$
, D has a winning strategy in the game
$\mathsf{PNFG}({\forall}^k{\vec{x}}\,{\exists}^\ell{\vec{y}},{\mathfrak A},{\mathfrak B})$
if and only if
$|A|\le|B|$
or
$|B|\ge (k+1)\ell$
. By Theorem 18, this means that the structure
${\mathfrak A}$
can be separated from
${\mathfrak B}$
by a sentence of the form
${\forall}^k{\vec{x}}\,{\exists}^\ell{\vec{y}}\,\theta$
if and only if
$|A|>|B|$
and
$|B|< (k+1)\ell$
.
7. Conclusion
In this paper, we introduced three different games, the number of quantifiers game
$\mathsf{NQG}$
, the monotone prefix game
$\mathsf{MPG}$
, and the prenex normal form game
$\mathsf{PNFG}$
, and proved that they are all equivalent to the Immerman game
$\mathsf{IG}$
, and hence they characterize equivalence of structures with respect to sentences containing a given number of quantifiers. The main results in the paper can be summarized as follows.
Theorem. Let
$\mathbb{A}$
and
$\mathbb{B}$
be classes of structures, and let
$\ell$
be a natural number. Then the following conditions are equivalent:
(1) S has a winning strategy in the game
$\mathsf{IG}_\ell(\mathbb{A},\mathbb{B})$
.(2) S has a winning strategy in the game
$\mathsf{NQG}(\ell,\mathbb{A},\mathbb{B})$
.(3) S has a winning strategy in the game
$\mathsf{MPG}(\ell,\mathbb{A},\mathbb{B})$
.(4) S has a winning strategy in the game
$\mathsf{PNFG}(\ell,\mathbb{A},\mathbb{B})$
.(5) There is a formula
$\varphi$
with
$\mathrm{nq}(\varphi)\le \ell$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\varphi)$
.(6) There is a quantifier prefix
$\vec Q\vec x$
of length at most
$\ell$
and a quantifier-free formula
$\theta$
such that
$\mathsf{Sep}(\mathbb{A},\mathbb{B},\vec Q\vec x\,\theta)$
.
The monotone prefix game
$\mathsf{MPG}$
and the prenex normal form game
$\mathsf{PNFG}$
differ from the Immerman game
$\mathsf{IG}$
in an interesting aspect. In the Immerman game, D has a canonical optimal strategy (the oblivious strategy), which means that she can be completely removed from the game by replacing her moves with the default moves defined by the optimal strategy. No such canonical optimal strategy for D exists in the games
$\mathsf{MPG}$
and
$\mathsf{PNFG}$
. Thus,
$\mathsf{IG}$
can be regarded as a one-player game, but
$\mathsf{MPG}$
and
$\mathsf{PNFG}$
are genuine two-player games.
Competing interests
The authors declare none.
