COUNTING TO INFINITY: GRADED MODAL LOGIC WITH AN INFINITY DIAMOND

Abstract

We extend the languages of both basic and graded modal logic with the infinity diamond, a modality that expresses the existence of infinitely many successors having a certain property. In both cases we define a natural notion of bisimilarity for the resulting formalisms, that we dub $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$, respectively. We then characterise these logics as the bisimulation-invariant fragments of the naturally corresponding predicate logic, viz., the extension of first-order logic with the infinity quantifier. Furthermore, for both $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ we provide a sound and complete axiomatisation for the set of formulas that are valid in every Kripke frame, we prove a small model property with respect to a widened class of weighted models, and we establish decidability of the satisfiability problem.

1 Introduction

The aim of this paper is to study some properties of a modality $\lozenge ^{\infty }$ , that we shall refer to as the infinity diamond because of its interpretation in a standard Kripke model $\mathbb {S} = (S,R,V)$ :

$$\begin{align*}\mathbb{S},s \Vdash \lozenge^{\infty}\varphi \text{ if there are infinitely many states } t \text{ such that } Rst \text{ and } \mathbb{S},t \Vdash \varphi. \end{align*}$$

Although this interpretation makes $\lozenge ^{\infty }$ a quite natural modality, it seems to have received very little attention in the literature. ¹

Rather than investigate the properties of the infinity diamond in isolation, we study the effects of adding $\lozenge ^{\infty }$ to a more basic modal language. In the simplest setting we define $\mathtt {ML}^{\infty }$ as the language we obtain by adding $\lozenge ^{\infty }$ to the basic modal language that features one modality $\lozenge $ . Perhaps a more natural setting is where we add $\lozenge ^{\infty }$ to the language $\mathtt {GML}$ of graded modal logic, since this logic already has a so-called counting modality $\lozenge ^{k}$ for every natural number k, with the following interpretation:

$$\begin{align*}\mathbb{S},s \Vdash \lozenge^{k}\varphi \text{ if there are at least } k \text{ many states }t\text{ such that } Rst \text{ and } \mathbb{S},t \Vdash \varphi. \end{align*}$$

These counting modalities were introduced in the early 1970s by Goble [15] and Fine [14], who gave a complete axiomatisation for the set of valid formulas. The name “graded modalities” originates with the eponymous paper [12] by Fattorosi-Barnaba and De Caro, which contains results on completeness (independently of Fine) and decidability, and is the first of a line of papers in which various aspects of counting modalities were studied. Subsequently, graded modal logic increasingly gained attention as a convenient formalism for describing and reasoning about (finite) quantities in a setting of modal or description logics [17], and as an interesting logic in its own right. The literature is by now too extensive to be reviewed here; two notable results are that the finite model property was established by van der Hoek [18], and that Tobies [27] showed that the satisfiability problem for $\mathtt {GML}$ can be solved in polynomial space. Of specific interest to our investigations is the work of de Rijke [24] who introduced a notion of bisimulation that is appropriate for graded modal logic in the sense that he showed $\mathtt {GML}$ to correspond to the bisimulation-invariant fragment of first-order logic, thus transferring van Benthem’s seminal characterisation of basic modal logic to the setting with counting modalities.

Our main goal is to investigate to which degree these results can be extended to the setting where we add the infinite counting modality to graded modal logic. The properties that we will consider here concern expressiveness, axiomatisations and decidability.

Before we continue to discuss our results in more detail, we need to discuss the ambient predicate logic for $\mathtt {GML}^{\infty }$ and $\mathtt {ML}^{\infty }$ . Since the semantics of $\lozenge ^{\infty }$ cannot be encoded in first-order logic, the natural candidate for such an ambient logic is the extension $\mathtt {FO}^{\infty }$ of first-order logic with the generalised quantifier “there exists infinitely many” that we shall denote as $\exists ^{\infty }$ .

Generalised quantifiers were introduced by Mostowski in [21], and in a more general sense by Lindström in [20], motivated by the observation that the standard first-order quantifiers do not suffice for expressing some basic mathematical concepts. Since then, they have attracted a lot of interest, to the effect that nowadays their study constitutes a well-established field of logic [1, 29]. The infinity quantifier, which is part of the broader family of cardinal quantifiers, provides a natural extension of first-order logic, but it was soon discovered that $\mathtt {FO}^{\infty }$ lacks many important metalogical properties, including compactness, finite axiomatisability and the Löwenheim–Skolem property (see [1]), but also Craig interpolation [22]. Probably due to these negative results, $\mathtt {FO}^{\infty }$ lost prominence to better behaved cardinal logics.

Negative properties of a logic, however, are not necessarily inherited by its fragments. For instance, the monadic fragment of $\mathtt {FO}^{\infty }$ is quite well behaved: Mostowski [21] already proved that this fragment is decidable, and recently, some model-theoretic characterisation theorems were obtained by Carreiro et al. [6].

In the same spirit, the results in this paper show that positive results can be obtained for $\mathtt {GML}^{\infty }$ , seen as a fragment of $\mathtt {FO}^{\infty }$ . First of all, we consider the (relative) expressiveness of $\mathtt {GML}^{\infty }$ , as a language for describing pointed Kripke models. We associate with $\mathtt {GML}^{\infty }$ a natural structural notion of equivalence between pointed models, to be called $\infty ,\#$ -bisimilarity, and we show that, with respect to this notion,

$$\begin{align*}\mathtt {GML}^{\infty } \text{ is the bisimulation-invariant fragment of } \mathtt {FO}^{\infty }.\end{align*}$$

That is, we prove that every $\mathtt {FO}^{\infty }$ -formula that is invariant under $\#,\infty $ -bisimulations, must be equivalent to some formula in $\mathtt {GML}^{\infty }$ . Our proof, which is game-theoretic in nature, basically follows the pattern laid out by Rosen’s generalisation [25] of van Benthem’s bisimulation invariance result for ordinary modal logic. More specifically, we extend recent work by Otto [23] who took a game-theoretical perspective on de Rijke’s bisimulation-invariance result for graded modal logic. To include the infinity quantifier and diamond, we use the Ehrenfeucht-style model comparison game for monotone generalised quantifiers as designed by Krawczyk and Krynicki [19].

We then move on to questions about axiomatisability and decidability. Taking a standard axiomatisation $\mathbf {G}$ for graded modal logic as a basis, we add some axioms and a derivation rule to capture the behaviour of the infinity diamond. Thus arriving at a logic $\mathbf {G^{\infty }}$ , we then show that

$$\begin{align*}\mathbf {G^{\infty }} \text{ is a sound and complete axiomatisation of the set of all } \mathtt {GML}^{\infty } \text{-validities},\end{align*}$$

where we call a $\mathtt {GML}^{\infty }$ -formula valid if it holds in every state of every Kripke model. To prove this result, we basically apply the canonical model method, which De Caro adapted to the setting of graded modal logic [9] by generalising the Kripke semantics for graded modal logic to that of models in which successors of a given state come with a certain weight. Our perspective on these weighted models will be coalgebraic [7]; that is, we will consider weighted models as coalgebras for a certain endofunctor $\mathsf {B}^{\infty }$ on the category with sets as objects and functions as arrows. This widening of perspective also allows us to prove that $\mathtt {GML}^{\infty }$ enjoys a small model property, a property that for obvious reasons does not make sense in the setting of Kripke models. Concretely, we will show that

$$\begin{align*}\text{every satisfiable } \mathtt {GML}^{\infty } \text{-formula is satisfiable in a weighted model of bounded size},\end{align*}$$

where “bounded” means that the size of the model is not just finite, but in fact bounded by some parameters of the formula. As an immediate corollary of the latter result, we then prove a decidability result for our logic:

$$\begin{align*}\text{it is decidable whether a given } \mathtt {GML}^{\infty } \text{-formula is satisfiable in a Kripke model}.\end{align*}$$

Finally, although we only mentioned our results for $\mathtt {GML}^{\infty }$ here, in each case we have an analogous result for $\mathtt {ML}^{\infty }$ .

In the next section we will introduce the syntax and semantics of the languages $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ ; we define the appropriate notions of bisimulation for these languages, we discuss the coalgebraic perspective on $\mathtt {GML}^{\infty }$ , and we review the logic $\mathtt {FO}^{\infty }$ and its Ehrenfeucht-style model comparison games. In Section 3 we prove that $\mathtt {GML}^{\infty }$ is the bisimulation invariant fragment of $\mathtt {FO}^{\infty }$ . We conclude this paper by proving, in Section 4, the other main results of the paper: completeness, the small coalgebra property, and decidability of the satisfiability problems for both $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ .

As mentioned above, the infinity diamond seems to have received little attention in the literature on modal logic; here we briefly discuss the references that we are aware of. In linear temporal logic, the formula $GFp$ may be used to express that p will be true infinitely often; the concept also occurs in branching time logics of the ctl variety, where the notation $\overset {\infty }{F}$ has been used for the infinitely often connective [10]. ² To the best of our knowledge, however, in this context this modality has not been investigated as such. Perhaps the first explicit mention of the infinity modality is in the paper [12] that initiated the Graded Modalities series. The modality features explicitly in the sixth paper of the series [13], in the context of an infinitary version of graded modal logic, where countable disjunctions and conjunctions are allowed. In this setting, $\lozenge ^{\infty }$ can be expressed by the other modalities: $\lozenge ^{\infty }\varphi \equiv \bigwedge _{n}\lozenge ^{n}\varphi $ , and because of the different nature of this infinitary language, the completeness result by Fattorosi-Barnaba and Grassotti has no direct bearing on our work. This is different in the case of the seventh Graded Modalities paper by Fattorosi-Barnaba and Balestrini, which discusses what is essentially our logic $\mathtt {ML}^{\infty }$ . The main result of [11] is a completeness result stating that the logic $\mathbf {K^{\infty }}$ that we define in Section 4 is a complete axiomatisation of the set of all $\mathtt {ML}^{\infty }$ -validities. As an interesting variation of our logic $\mathtt {ML}^{\infty }$ , we mention the work by van Benthem et al. [4]. They introduce a modality $\bullet $ which is interpreted in Kripke models by stating that $\bullet \varphi $ holds in a state if it has infinitely many reflexive successors where $\varphi $ holds. Among other things, the authors provide a finite axiomatisation and they show that the resulting logic has the Craig interpolation property.

Finally, this paper grew out of the M.Sc. thesis [2], written by the first author under the supervision of the second, which more or less covers the results on the logic $\mathtt {ML}^{\infty }$ that we report on.

2 Preliminaries

In this section we formally define the logics $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ , we introduce some of the basic concepts that will be used further on in the paper, and we formulate some of our main results. In Section 2.1 we introduce the languages $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ , as well as the basic syntactic and semantic concepts related to these languages. In Section 2.2 we adapt the well-known concept of bisimulation to account for the semantic behaviour of the $\lozenge ^{\infty }$ modality. In Section 2.3 we present the reader with an alternative, coalgebraic semantics for our languages, and we relate this to the standard Kripke semantics. We conclude this section with a brief introduction to the basic syntactic and semantic concepts related to the predicate logic $\mathtt {FO}^{\infty }$ .

2.1 Graded modal logic with the infinity diamond

In this subsection we provide some basic syntactic and semantic definitions concerning the modal logics $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ . The language of the latter logic will have a family of diamonds, each indexed by either a natural number or infinity; formally, we introduce this index set as follows.

Definition 2.1. We let $\mathbb {N}^{\infty }$ denote the set $\mathbb {N}^{\infty } \mathrel {:=} \mathbb {N} \cup \{ \infty \}$ , and we order this set by extending the standard order of the natural numbers in the obvious way, i.e., we declare every natural number to be strictly smaller than $\infty $ .

As a convention, we will use the Greek letters $\kappa ,\lambda $ for arbitrary elements of $\mathbb {N}^{\infty }$ , and lower case roman letters $k, l, m, \ldots $ for indices in $\mathbb {N}$ .

We can now define the languages $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ .

Definition 2.2. Given a set P of proposition letters, we define the language $\mathtt {GML}^{\infty }(P)$ as follows:

$$\begin{align*}\varphi \mathrel{::=} p \mid \neg\varphi \mid \varphi_{0}\lor\varphi_{1} \mid \lozenge^{\kappa}\varphi, \end{align*}$$

where $p \in P$ and $\kappa \in \mathbb {N}^{\infty }$ . The sets $\mathtt {ML}^{\infty }$ , $\mathtt {GML}$ and $\mathtt {ML}$ are defined as those fragments of $\mathtt {GML}^{\infty }$ where the occurrence of the modalities $\lozenge ^{\kappa }$ is restricted as follows:

$$\begin{align*}\begin{array}{|c|c|c|} \hline \mathtt{ML}^{\infty} & \mathtt{GML} & \mathtt{ML} \\ \hline \kappa\in \{ 1, \infty \} & \kappa\in\mathbb{N} & \kappa = 1 \\ \hline \end{array}\end{align*}$$

We will use the Boolean connectives $\land , \to $ and $\leftrightarrow $ as the standard abbreviations, and use modalities $\Box ^{\kappa }$ (for any $\kappa \in \mathbb {N}^{\infty }$ ), and $\lozenge ^{=k}$ (for any $k \in \mathbb {N}$ ), given by the following definition:

$$\begin{align*}\begin{array}{lll} \Box^{\kappa}\varphi &\mathrel{:=}& \neg\lozenge^{\kappa}\neg\varphi, \\ \lozenge^{=k}\varphi &\mathrel{:=}& \lozenge^{k}\varphi\land\neg\lozenge^{k+1}\varphi. \end{array}\end{align*}$$

We occasionally denote $\lozenge ^{1}$ and $\Box ^{1}$ simply as $\lozenge $ and $\Box $ , especially in the context of $\mathtt {ML}^{\infty }$ . Clearly $\Box ^{\kappa }$ is the (Boolean) dual of $\lozenge ^{\kappa }$ , and $\lozenge ^{=k}\varphi $ will have the meaning that the current state has exactly k successors where $\varphi $ holds.

In the sequel we will need three complexity measures for a $\mathtt {GML}^{\infty }$ -formula: size, depth and rank. The first two notions are standard, and the rank of a formula quantifies the “highest” modality that occurs in the formula (with $\lozenge ^{\infty }$ counting as $\lozenge ^{1}$ ):

Definition 2.3. Let $\varphi $ be some arbitrary but fixed $\mathtt {GML}^{\infty }$ -formula. The size $|\varphi |$ of $\varphi $ is the number of its subformulas (where the notion of subformula is defined in the standard way). The (modal) depth of $\varphi $ is the maximal height of a sequence of nested modalities occurring in $\varphi $ .

The rank of $\varphi $ , denoted by $\text {r}(\varphi )$ , is recursively defined as follows:

$$\begin{align*}\begin{array}{lll} \text{r}(p) & \mathrel{:=} & 0, \\ \text{r}(\neg\varphi) & \mathrel{:=} & \text{r}(\varphi), \\ \text{r}(\varphi_{0}\vee\varphi_{1}) & \mathrel{:=} & \max\{\text{r}(\varphi_{0}),\text{r}(\varphi_{1})\}, \\ \text{r}(\lozenge^{k}\varphi) & \mathrel{:=} & \max\{k,\text{r}(\varphi) \}, \\ \text{r}(\lozenge^{\infty}\varphi) & \mathrel{:=} & \max \{1,\text{r}(\varphi) \}. \end{array}\end{align*}$$

The rank of a finite set $\Sigma $ of formulas is simply defined as $\text {r}(\Sigma ) \mathrel {:=} \max \{ \text {r}(\varphi ) \mid \varphi \in \Sigma \}$ .

We can now introduce the semantics of $\mathtt {GML}^{\infty }$ . The intended semantics of this language is that of Kripke models.

Definition 2.4. A (Kripke) frame is a pair $(S,R)$ where $R \subseteq S \times S$ is a binary relation on S. Elements of S will be called states or worlds. For a fixed Kripke frame, the set $R(s)\mathrel {:=}\{t\in S\mid (s,t)\in R\}$ will denote the set of successors of s. A P-valuation on a set S is a map $V: P \to \wp (S)$ ; when the set P of proposition letters is understood, we will usually simply speak of a valuation. A (Kripke) model is a triple $\mathbb {S} = (S,R,V)$ such that $(S,R)$ is a Kripke frame, the underlying frame of $\mathbb {S}$ , and V is a valuation on S. Finally, a pointed model is simply a pair ( $\mathbb {S},s)$ consisting of a Kripke model $\mathbb {S}$ and a point s in $\mathbb {S}$ .

Definition 2.5. Let $\mathbb {S} = (S,R,V)$ be a Kripke model. By a straightforward induction on the complexity of formulas we define a satisfaction relation $\Vdash _{\mathbb {S}}$ between states and $\mathtt {GML}^{\infty }$ -formulas, where we write $\mathbb {S},s \Vdash \varphi $ rather than $s \Vdash _{\mathbb {S}} \varphi $ :

$$\begin{align*}\begin{array}{lll} \mathbb{S},s \Vdash p & \text{if} & s \in V(p), \\ \mathbb{S},s \Vdash \neg\varphi & \text{if} & \mathbb{S},s \not\Vdash \varphi, \\ \mathbb{S},s \Vdash \varphi_{0}\lor\varphi_{1} & \text{if} & \mathbb{S},s \Vdash \varphi_{0} \text{ or } \mathbb{S},s \Vdash \varphi_{1}, \\ \mathbb{S},s \Vdash \lozenge^{\kappa}\varphi. & \text{if} & | \{ t \in R(s) \mid \mathbb{S},t \Vdash \varphi \}| \geq \kappa. \end{array}\end{align*}$$

In case $\mathbb {S},s \Vdash \varphi $ we say that $\varphi $ is true at s (in $\mathbb {S}$ ) or that s satisfies $\varphi $ .

A formula $\varphi $ is satisfiable if it is satisfied at some state in some model, and valid if it is true at every state in every model.

We call two pointed models $(\mathbb {S},s)$ and ( $\mathbb {S}',s')$ $\mathtt {GML}^{\infty }$ -equivalent, and we denote this as $(\mathbb {S},s){\equiv }^{\infty ,\#}(\mathbb {S}',s')$ , if they satisfy the same set of $\mathtt {GML}^{\infty }$ -formulas. The relation ${\equiv }^{\infty }$ of $\mathtt {ML}^{\infty }$ -equivalence is defined analogously. More generally, given a fragment $\mathtt {L}$ of $\mathtt {GML}^{\infty }$ , we call $(\mathbb {S},s)$ and ( $\mathbb {S}',s')\ \mathtt {L}$ -equivalent if they satisfy the same $\mathtt {L}$ -formulas; in the case $\mathtt {L}$ consists of the atomic formulas we use the phrase atomic equivalence.

The dual notions of satisfiability and validity are among the key topics of interest in this paper. In Section 4 we will give fairly simple and intuitive finite axiomatisations for the set of validities of $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ , respectively. Here we already formulate the following decidability theorem, which a fortiori applies to $\mathtt {ML}^{\infty }$ since it is a fragment of $\mathtt {GML}^{\infty }$ .

Theorem 2.6 (Decidability of satisfiability)

It is decidable in elementary time whether a given $\mathtt {GML}^{\infty }$ -formula is satisfiable or not.

For a proof of this result, observe that it is an immediate corollary of Corollary 2.18 and Theorem 2.20.

2.2 Bisimilarity

In the previous subsection we introduced the modal logics $\mathtt {GML}^{\infty }$ and $\mathtt {ML}^{\infty }$ . We now see how to adapt the standard notion of bisimilarity between pointed models to account for the infinitary nature of these logics. To start with, it will be convenient to use the following notations.

Definition 2.7. Where X and Y are sets, and X is a subset of Y, we write $X \subseteq _{\omega } Y$ if X is finite, and $X \subseteq _{\infty } Y$ if X is infinite.

A suitable notion of bisimilarity for $\mathtt {GML}^{\infty }$ can be defined as follows.

Definition 2.8. Let $\mathbb {S}_{0} = (S_{0},R_{0},V_{0})$ and $\mathbb {S}_{1} = (S_{1},R_{1},V_{1})$ be two Kripke models. A relation $Z \subseteq S_{0} \times S_{1}$ is a $\infty ,\#$ -bisimulation if it satisfies the following conditions, for every pair $(w_{0},w_{1}) \in Z$ :

1. 1. $w_{1}$ and $w_{2}$ are atomically equivalent.

2. 2. For every $X_{0}\subseteq _{\omega } R_{0}(w_{0})$ there is an $X_{1} \subseteq _{\omega } R_{1}(w_{1})$ such that $|X_{0}|=|X_{1}|$ and for every $v_{1}\in X_{1}$ there is a $v_{0}\in X_{0}$ with $(v_{0},v_{1}) \in Z$ .

3. 3. For every $X_{1}\subseteq _{\omega } R_{1}(w_{1})$ there is an $X_{0} \subseteq _{\omega } R_{0}(w_{0})$ such that $|X_{0}|=|X_{1}|$ and for every $v_{0}\in X_{0}$ there is a $v_{1}\in X_{1}$ with $(v_{1},v_{0}) \in Z$ .

4. 4. For every $X_{0}\subseteq _{\infty } R_{0}(w_{0})$ there is an $X_{1} \subseteq _{\infty } R_{1}(w_{1})$ such that for every $v_{1}\in X_{1}$ there is a $v_{0}\in X_{0}$ with $(v_{0},v_{1}) \in Z$ .

5. 5. For every $X_{1}\subseteq _{\infty } R_{1}(w_{1})$ there is an $X_{0} \subseteq _{\infty } R_{0}(w_{0})$ such that for every $v_{0}\in X_{0}$ there is a $v_{1}\in X_{1}$ with $(v_{1},v_{0}) \in Z$ .

We say that two pointed models $(\mathbb {S}_{0},w_{0})$ and $(\mathbb {S}_{1},w_{1})$ are $\infty ,\#$ -bisimilar, denoted by , if there is a $\infty ,\#$ -bisimulation linking $w_{0}$ to $w_{1}$ .

For the language $\mathtt {ML}^{\infty }$ we can simplify the definition somewhat.

Definition 2.9. Let $\mathbb {S}_{0} = (S_{0},R_{0},V_{0})$ and $\mathbb {S}_{1} = (S_{1},R_{1},V_{1})$ be two Kripke models. A relation $Z \subseteq S_{0} \times S_{1}$ is a $\infty $ -bisimulation if it satisfies, for every pair $(w_{0},w_{1}) \in Z$ , the conditions 1, 4 and 5 of Definition 2.8, together with the standard back and forth conditions:

1. 6. For every $v_{0} \in R_{0}(w_{0})$ there is a $v_{1} \in R_{1}(w_{1})$ such that $(v_{0},v_{1}) \in Z$ .

2. 7. For every $v_{1} \in R_{1}(w_{1})$ there is a $v_{0} \in R_{0}(w_{0})$ such that $(v_{1},v_{0}) \in Z$ .

Two pointed models $(\mathbb {S}_{0},w_{0})$ and $(\mathbb {S}_{1},w_{1})$ are $\infty $ -bisimilar, denoted by , if there is a $\infty $ -bisimulation linking $w_{0}$ to $w_{1}$ .

It is one of the main goals of this paper to show that these notions of bisimilarity are indeed appropriate for the languages $\mathtt {GML}^{\infty }$ and $\mathtt {ML}^{\infty }$ . The first observation is that the formulas in these languages are indeed invariant for the given notions of bisimulation. The proof of this result is routine.

Proposition 2.10. Let $(\mathbb {S},w)$ and $(\mathbb {S}',w')$ be two pointed models. Then the following holds:

1. 1. If then $(\mathbb {S},w){\equiv }^{\infty ,\#}(\mathbb {S}',w')$ .

2. 2. If then $(\mathbb {S},w){\equiv }^{\infty }(\mathbb {S}',w')$ .

The above notions of bisimilarity can be equivalently approached from a game theoretic perspective, via a modification of the standard bisimilarity game.

Definition 2.11. Let $\mathbb {S}_{0} = (S_{0},R_{0},V_{0})$ and $\mathbb {S}_{1} = (S_{1},R_{1},V_{1})$ be two Kripke models; as a convention, when $\mathbb {S}_{i}$ is one of these two models, we write $\mathbb {S}_{-i}$ to denote the other. We define the bisimilarity game $\mathcal {B}^{\infty ,\#}(\mathbb {S}_{0},\mathbb {S}_{1})$ between two players, Spoiler (male) and Duplicator (female). A basic position in this game is a pair $(w_{0},w_{1})$ of states from $\mathbb {S}_{0}$ and $\mathbb {S}_{1}$ , respectively.

A single round of the game starts and ends with such a basic position, and consists of a short interaction between the two players, of the following kind.

• – Let $(w_{0},w_{1})$ be the starting position of the round.

• – Spoiler chooses a structure $\mathbb {S}_{i}$ and a subset $X_i \subseteq R_{i}(w_{i})$ .

• – Duplicator picks a subset $X_{-i} \subseteq R_{-i}(w_{-i})$ such that either $|X_{i}| = |X_{-i}| < \omega $ or $|X_{i}|,|X_{-i}| \geq \omega $ .

• – Spoiler chooses an element $u_{-i} \in X_{-i}$ .

• – Duplicator responds with an element $u_i \in X_i$ .

• – The new basic position is $(u_{0},u_{1})$ .

Spoiler wins a match of the game as soon as a basic position $(w_{0},w_{1})$ is reached consisting of two states that are not atomically equivalent, or if in some round Duplicator fails to come up with a matching set in her response to Spoiler’s first move. Duplicator wins a match of the game if, during some round of the match, Spoiler fails to pick a state in his second move. In addition, Duplicator also wins if she manages to survive for $\omega $ many rounds.

We write $\mathcal {B}^{\infty ,\#}(\mathbb {S}_{0},\mathbb {S}_{1})@(w_{0},w_{1})$ for the initialised version of the game which starts at position $(w_{0},w_{1})$ . A position $(w_{0},w_{1})$ is winning for a player if this player has a winning strategy in the initialised game $\mathcal {B}^{\infty ,\#}(\mathbb {S}_{0},\mathbb {S}_{1})@(w_{0},w_{1})$ , i.e., a way of playing that guarantees this player will win, no matter how their opponent plays.

Finally, we write $\mathcal {B}^{\infty }(\mathbb {S}_{0},\mathbb {S}_{1})$ for the variation of the game where Spoiler can only pick subsets that are either singletons or infinite.

The following proposition states that these games indeed provide an equivalent perspective on bisimilarity. The proof, which is routine, is left to the reader.

Proposition 2.12. Let $(\mathbb {S}_{0},w_{0})$ and $(\mathbb {S}_{1},w_{1})$ be two pointed models, then the following hold:

• • iff $(w_{0},w_{1})$ is a winning position for Duplicator in $\mathcal {B}^{\infty ,\#}(\mathbb {S} _{0},\mathbb {S}_{1})$ .

• • iff $(w_{0},w_{1})$ is a winning position for Duplicator in $\mathcal {B}^{\infty }(\mathbb {S} _{0},\mathbb {S}_{1})$

2.3 Coalgebraic perspective

In this section we extend the semantics of our graded modal logic to so-called weighted models. Intuitively, the idea underlying these structures is that, given a fixed state s, we assign a certain weight to every state t in the structure. Thus, Kripke models are a special case of weighted models where every state t receives either the value $1$ (indicating that t is a successor of s), or the weight $0$ (indicating that it is not). In the general case, weights can take any arbitrary values in the set $\mathbb {N}^{\infty }$ . Before defining the semantics of $\mathtt {GML}^{\infty }$ in such models, we need to define some arithmetic on the set $\mathbb {N}^{\infty }$ .

Definition 2.13. We extend the addition operation on the natural numbers to the set $\mathbb {N}^{\infty }$ by setting $\kappa + \lambda \mathrel {:=} \infty $ whenever $\infty \in \{ \kappa , \lambda \}$ . Moreover, this binary operation can be extended to a finitary operation $\sum $ on $\mathbb {N}^{\infty }$ in the obvious way, and subsequently we define, for any set $\{ \kappa _{i} \in \mathbb {N}^{\infty } \mid i \in I \}$ where I is infinite:

$$\begin{align*}\sum_{i \in I} \kappa_{i} \mathrel{:=} \left\{ \begin{array}{ll} \sum_{i\in I'} \kappa_{i}, & \text{if } I' \mathrel{:=} \{ i \in I \mid \kappa_{i} \neq 0 \} \text{ is finite}, \\ \infty, & \text{otherwise}. \end{array} \right. \end{align*}$$

Observe that with this definition we find that $\sum _{i \in I} \kappa _{i} = \infty $ if and only if $\infty $ occurs as one of the $\kappa _{i}$ or there are infinitely indices i for which $\kappa _{i}$ is non-zero.

We can now define weighted models as structures of the form $\mathbb {S} = (S,w,V)$ where S is a set of states, V is a valuation, and $w: W \times W \to \mathbb {N}^{\infty }$ is a function assigning a weight to every pair of states. The semantics of the graded modalities can then be given by putting $\mathbb {S},s \Vdash \lozenge ^{\kappa }\varphi $ if the total weight of all $\varphi $ -states, as seen from s, is at least $\kappa $ . In fact, this is exactly what we will do, but we will use the notation and terminology from the theory of coalgebra.

The theory of Universal Coalgebra [26] provides a mathematical framework for studying various kinds of state-based evolving systems such as finite state automata, Markov chains, or labelled transition systems, in a uniform manner. Kripke structures provide some further prime examples of coalgebra, and in fact the connection between modal logic and coalgebra is very tight [7]. Graded modal logic has been studied from this perspective since the work by D’Agostino and Visser [8].

Definition 2.14. Given a set S, we let $\mathsf {B}^{\infty }(S) \mathrel {:=} (\mathbb {N}^{\infty })^{S}$ denote the set of $\mathbb {N}^{\infty }$ -valued weight functions on S, that is, the collection of maps from S to $\mathbb {N}^{\infty }$ . A $\mathsf {B}^{\infty }$ -coalgebra is a pair $(S,\sigma )$ , where $\sigma : S \to \mathsf {B}^{\infty }(S)$ assigns, to every state $s \in S$ , a weight function, that we will denote as either $\sigma (s)$ or $\sigma _{s}$ . A $\mathsf {B}^{\infty }$ -model is a triple $(S,\sigma ,V)$ where $(S,\sigma )$ is a $\mathsf {B}^{\infty }$ -coalgebra and V is a valuation on S.

Remark. Although we do not stress this point in our paper, in order to fully understand and appreciate the coalgebraic perspective it is essential to realise that $\mathsf {B}^{\infty }$ is part of a functor on the category of sets. For readers with some category-theoretic background, we give a brief sketch of the approach. Let $\mathsf {Set}$ be the category taking sets as objects and functions as arrows, then $\mathsf {B}^{\infty }$ is set to be the $\mathsf {Set}$ -endofunctor such that for an arbitrary function $f: S \to S'$ , the map $\mathsf {B}^{\infty } f: \mathsf {B}^{\infty } (S) \to \mathsf {B}^{\infty }(S')$ is defined as follows. For an arbitrary weight function $w: S \to \mathbb {N}^{\infty }$ we define $(\mathsf {B}^{\infty } f)(w):S' \to \mathbb {N}^{\infty }$ to be

$$\begin{align*}(\mathsf{B}^{\infty} f)(w)(t') \mathrel{:=} \sum_{t\in f^{-1}(t')} w(t), \end{align*}$$

where $t\in S'$ .

This functorial perspective is used to define a natural notion of morphism between $\mathsf {B}^{\infty }$ -coalgebras: we say that a map $f: S \to S'$ is a morphism from one $\mathsf {B}^{\infty }$ -coalgebras $(S,\sigma )$ to another $(S',\sigma ')$ , if we have that $(\mathsf {B}^{\infty } f)\circ \sigma = \sigma ' \circ f$ .

This is all completely analogous to the coalgebraic perspective on Kripke structures. Kripke frames can be understood as coalgebras for the power set functor $\mathsf {P}$ ; here we identify a binary accessibility relation R on a set S with the function $\sigma _{R}$ from S to $\mathsf {P}(S)$ mapping any state $s \in S$ to the collection of its successors. It is then straightforward to verify that a map $f: S \to S'$ is a bounded morphism between the Kripke frames $(S,R)$ and $(S',R')$ if it satisfies $(\mathsf {P} f)\circ \sigma _{R} = \sigma _{R'} \circ f$ .

Making our earlier remarks precise, we show how $\mathsf {B}^{\infty }$ -models provide a natural interpretation for $\mathtt {GML}^{\infty }$ -formulas indeed.

Definition 2.15. Let $\mathbb {S} = (S,\sigma ,V)$ be a $\mathsf {B}^{\infty }$ -model. By a straightforward formula induction we define a truth relation $\Vdash $ between states of $\mathbb {S}$ and $\mathtt {GML}^{\infty }$ -formulas:

$$\begin{align*}\begin{array}{lcl} \mathbb{S},s \Vdash p & \text{if} & s \in V(p), \\ \mathbb{S},s \Vdash \neg\varphi & \text{if} & \mathbb{S},s \not\Vdash \varphi, \\ \mathbb{S},s \Vdash \varphi_{1} \lor \varphi_{2} & \text{if} & \mathbb{S},s \Vdash \varphi_{1} \text{ or } \mathbb{S},s \Vdash \varphi_{2}, \\ \mathbb{S},s \Vdash \lozenge^{\kappa}\varphi & \text{if} & \sum_{\mathbb{S},t \Vdash \varphi} \sigma_{s}(t) \geq \kappa. \end{array}\end{align*}$$

As we will see now, this approach in fact extends the Kripke semantics. We will identify a Kripke frame $(S,R)$ with the $\mathsf {B}^{\infty }$ -coalgebra $(S,\sigma _{R})$ , where $\sigma _{R}: S \to \mathsf {B}^{\infty }(S)$ is given by putting, for every $s \in S$

$$\begin{align*}\sigma_{R}(s)(t) \mathrel{:=} \left\{ \begin{array}{ll} 1, & \text{if } t \in R(s), \\ 0, & \text{otherwise}. \end{array} \right. \end{align*}$$

Introducing some notation, given a Kripke model $\mathbb {S} = (S,R,V)$ , we will write $\mathbb {S}^{\infty } \mathrel {:=} (S,\sigma _{R},V)$ . It is then not hard to see that the truth relations of the Kripke model and its coalgebraic incarnation coincide (cf. Proposition 2.17), so that we may say that $\mathsf {B}^{\infty }$ -coalgebras extend the Kripke semantics indeed.

Interestingly—in the opposite direction—we may encode $\mathsf {B}^{\infty }$ -coalgebras as Kripke models as well. To do so, we simply extend De Caro’s original encoding [9] to the setting with the infinity diamond.

Definition 2.16. Let $(S,\sigma )$ be some $\mathsf {B}^{\infty }$ -coalgebra, and let V be some valuation on S. We let $R_{\sigma }$ be the binary relation on the set $S \times \mathbb {N}$ given by

$$\begin{align*}\big( (s,k), (t,m) \big) \in R_{\sigma} \text{ if and only if } m < \sigma_{s}(t), \end{align*}$$

and we define the valuation $V_{\infty }$ on $S \times \mathbb {N}$ by putting

$$\begin{align*}V_{\infty}(p) \mathrel{:=} \{ (s,k) \in S \times \mathbb{N} \mid s \in V(p) \}. \end{align*}$$

Finally, given a $\mathsf {B}^{\infty }$ -model $\mathbb {S} \mathrel {:=} (S,\sigma ,V)$ , we define its associated Kripke model as the structure

$$\begin{align*}\mathbb{S}_{\infty} \mathrel{:=} (S \times \mathbb{N}, R_{\sigma},V_{\infty}). \end{align*}$$

Intuitively, the definition of $R_{\sigma }$ ensures that any state $(s,k)$ obtains, as its successors, as many copies of t as it is determined by the weight function $\sigma _{s}$ when applied to the state t. Based on this observation, one may easily prove the following equivalences between the two perspectives.

Proposition 2.17. Let $\varphi $ be a $\mathtt {GML}^{\infty }$ formula.

1. 1) For any Kripke model $\mathbb {S} = (S,R,V)$ , and any state $s \in S$ we have that

   $$\begin{align*}\mathbb{S},s \Vdash \varphi \text{ if and only if } \mathbb{S}^{\infty},s \Vdash \varphi. \end{align*}$$

2. 2) For any $\mathsf {B}^{\infty }$ -model $\mathbb {S} = (S,\sigma ,V)$ , any state $s \in S$ and any $k \in \mathbb {N}$ we have that

   $$\begin{align*}\mathbb{S},s \Vdash \varphi \text{ if and only if } \mathbb{S}_{\infty},(s,k) \Vdash \varphi. \end{align*}$$

Proof. Both items can be proved by a straightforward induction on the complexity of $\varphi $ . We omit the details.

As an immediate consequence of this, the set of Kripke-valid $\mathtt {GML}^{\infty }$ -formulas coincides with the collection of coalgebraic validities.

Corollary 2.18. For every $\mathtt {GML}^{\infty }$ -formula $\varphi $ :

(1) $$ \begin{align} \varphi \text{ is valid iff } \varphi \text{ is valid in every } \mathsf{B}^{\infty}\text{-coalgebra.} \end{align} $$

At a more conceptual level, we note that the constructions and equivalences discussed above reveal that in some cases $\mathsf {B}^{\infty }$ -coalgebras can serve as more compact, and perhaps even finite representations of Kripke structures. This raises the question whether any satisfiable $\mathtt {GML}^{\infty }$ -formula can perhaps be satisfied in a finite $\mathsf {B}^{\infty }$ -coalgebra, where we observe that the analogous question for Kripke models makes no sense at all.

The result below states that indeed we can establish a finite model property for coalgebraic models; we can even recursively bound the complexity of such a finite satisfying coalgebra in terms of the satisfiable formula. As a corollary of this, we can show that the satisfiability problem for $\mathtt {GML}^{\infty }$ -formulas is decidable. To formulate this we need the following size measures of $\mathsf {B}^{\infty }$ -coalgebras.

Definition 2.19. Let $\mathbb {S} = (S,\sigma ,V)$ be a finite $\mathsf {B}^{\infty }$ -coalgebra. We define its size $|\mathbb {S}|$ as the number of its states, $|\mathbb {S}| \mathrel {:=} |S|$ , and its weight $w(\mathbb {S})$ as the maximum number reached as a finite value of any weight function:

$$\begin{align*}w(\mathbb{S}) \mathrel{:=} \max \big( \mathbb{N} \cap \{ \sigma_{s}(t) \mid s,t \in S \} \big). \end{align*}$$

Theorem 2.20 (Small Model Property)

Let $\varphi $ be a $\mathtt {GML}^{\infty }$ -formula. If $\varphi $ is satisfiable, then it is satisfiable in some $\mathsf {B}^{\infty }$ -coalgebra of size at most $2^{|\varphi |}$ and weight at most $\text {r}(\varphi )$ .

For a proof of this theorem, we refer to Theorem 4.5. Observe that this result applies to $\mathtt {ML}^{\infty }$ since it is a fragment of $\mathtt {GML}^{\infty }$ .

2.4 First-order logic with the infinity quantifier

In this section we introduce the predicate logic $\mathtt {FO}^{\infty }$ , the extension of first-order logic with the infinity quantifier $\exists ^{\infty }$ . We may, of course, consider the language of $\mathtt {FO}^{\infty }$ over arbitrary signatures. In the context of this paper, however, we restrict attention to a signature that is tailored towards Kripke structures. That is, every proposition letter features as a unary predicate symbol, and in addition our signature has a binary predicate symbol R to denote the accessibility relation.

Having these restrictions in mind, we provide some basic syntactic and semantic definitions. Subsequently, we introduce some useful concepts that link the $\mathtt {FO}^{\infty }$ language with the $\mathtt {GML}^{\infty }$ modal language. We conclude this section by adapting the well-known Ehrenfeucht–Fraïssé game to account for the infinity quantifier.

Definition 2.21. Given a set P of proposition letters, and a disjoint set $\mathtt {iVar}$ of individual variables, we define the language $\mathtt {FO}^{\infty }(P)$ as follows:

$$\begin{align*}\varphi \mathrel{::=} p(x) \mid R(x,y) \mid x = y \mid \neg\varphi \mid (\varphi_{0}\lor\varphi_{1}) \mid \exists x\, \varphi \mid \exists^{\infty} x\, \varphi, \end{align*}$$

where $p \in P$ and $x,y \in \mathtt {iVar}$ .

We use the Boolean connectives $\land , \to $ and $\leftrightarrow $ as the standard abbreviations, and define $\forall $ and $\forall ^{\infty }$ as the Boolean duals of the quantifiers $\exists $ and $\exists ^{\infty }$ : $\forall x\, \varphi \mathrel {:=} \neg \exists x\, \neg \varphi $ , and $\forall ^{\infty } x\, \varphi \mathrel {:=} \neg \exists ^{\infty } x\, \neg \varphi $ . Furthermore, we extend various well-known syntactic notions, such as free and bound variables or quantifier depth, from first-order logic to $\mathtt {FO}^{\infty }$ in the obvious way.

The semantics of $\mathtt {FO}^{\infty }$ in Kripke models is defined as follows.

Definition 2.22. By induction on the complexity of an $\mathtt {FO}^{\infty }$ -formula $\varphi $ , we inductively define its meaning in a Kripke model $\mathbb {S} = (S,R,V)$ under an assignment $g: \mathtt {iVar} \to S$ , by means of the following truth relation $\models $ :

$$\begin{align*}\begin{array}{lll} \mathbb{S},g \models p(x) & \text{if} & g(x) \in V(p), \\ \mathbb{S},g \models R(x,y) & \text{if} & (g(x),g(y)) \in R, \\ \mathbb{S},g \models x=y & \text{if} & g(x) = g(y), \\ \mathbb{S},g \models \neg\varphi & \text{if} & \mathbb{S},g \not\models \varphi, \\ \mathbb{S},g \models (\varphi_{0}\lor\varphi_{1}) & \text{if} & \mathbb{S},g \models \varphi_{0} \text{ or } \mathbb{S},g \models \varphi_{1}, \\ \mathbb{S},g \models \exists x\, \varphi & \text{if} & \text{there is an } s \in S \text{ such that } \mathbb{S},g[x\mapsto s] \models \varphi, \\ \mathbb{S},g \models \exists^{\infty} x\, \varphi & \text{if} & \text{there are infinitely many } s \in S \text{ such that } \mathbb{S},g[x\mapsto s] \models \varphi. \end{array}\end{align*}$$

Here $g[x\mapsto s]$ denotes the assignment that is as g except that it maps x to s.

It is easy to see that the only variables on which the meaning of a formula $\varphi $ depends, are the free ones of $\varphi $ . We adopt the standard notational convention that, where $\overline {x} = x_{0}\cdots x_{k-1}$ , we write $\varphi (\overline {x})$ to indicate that the free variables of $\varphi $ are among $x_{0},\ldots ,x_{k-1}$ . We will be particularly interested in formulas with a single free variable, since these can naturally be interpreted in pointed Kripke models, and may thus be compared with modal formulas.

Definition 2.23. Let $\varphi (x) \in \mathtt {FO}^{\infty }$ be some formula. Given a Kripke model $\mathbb {S} = (S,R,V)$ , we write $\mathbb {S} \models \varphi [s]$ to denote that $\mathbb {S}, g \models \varphi $ , for some/any assignment g such that $g(x) = s$ . Where $\psi $ is a $\mathtt {GML}^{\infty }$ -formula, we call $\varphi $ and $\psi $ equivalent, notation: $\varphi \equiv \psi $ , if we have that $\mathbb {S} \models \varphi [s]$ iff $\mathbb {S},s \Vdash \psi $ , for every pointed model $(\mathbb {S},s)$ .

Definition 2.24. Let E be some equivalence relation on the class of pointed models. We call an $\mathtt {FO}^{\infty }$ formula $\varphi (x)\ E$ -invariant if we have $\mathbb {S}\vDash \varphi [s]$ iff $\mathbb {S}'\vDash \varphi [s']$ for any pair $(\mathbb {S},s), (\mathbb {S}',s')$ of E-equivalent pointed Kripke models.

We shall be particularly interested in the set of -invariant $\mathtt {FO}^{\infty }$ -formulas. There is an obvious way to extend the standard translation from modal to first-order logic, to a translation that maps an arbitrary $\mathtt {GML}^{\infty }$ -formula $\varphi $ to an equivalent $\mathtt {FO}^{\infty }$ -formula $\varphi '(x)$ . This shows that $\mathtt {GML}^{\infty }$ corresponds to some fragment of $\mathtt {FO}^{\infty }$ , and clearly this fragment consists of formulas that are all -invariant.

What is not obvious, however, is that this fragment in fact contains, up to equivalence, all $\mathtt {FO}^{\infty }$ -formulas $\varphi (x)$ that are -invariant. This expressive completeness result is the content of the next bisimulation-invariance theorem.

Theorem 2.25. Let $\varphi (x)$ be an $\mathtt {FO}^{\infty }$ formula. Then $\varphi $ is -invariant if and only if it is equivalent to some $\mathtt {GML}^{\infty }$ -formula. Similarly, $\varphi $ is -invariant if and only if it is equivalent to some $\mathtt {ML}^{\infty }$ -formula.

As mentioned already, our proof of Theorem 2.25 will be game-theoretic in nature. For this purpose we adapt the well-known Ehrenfeucht–Fraïssé games for first-order logic, to account for the semantic behaviour of the infinity quantifier. This game can be seen as the adaptation to our specific setting of the Ehrenfeucht-style model comparison game for arbitrary monotone generalised quantifiers originating with Krawczyk and Krynicki [19], and discussed in more detail in Väänänen [28].

Definition 2.26. Let $\mathbb {S}_{0} = (S_{0},R_{0},V_{0})$ and $\mathbb {S}_{1} = (S_{1},R_{1},V_{1})$ be two Kripke models. Two k-tuples $\overline {u}_{0} = u_{0,0}u_{0,1}\cdots u_{0,k-1}$ and $\overline {u}_{1} = u_{1,0}u_{1,1}\cdots u_{1,k-1}$ are locally isomorphic if we have, for all $i,j$ , that $u_{0,i} = u_{0,j}$ iff $u_{1,i} = u_{1,j}$ , that $u_{0,i} \in V_{0}(p)$ iff $u_{1,i} \in V_{1}(p)$ , for all $p \in P$ , and that $R_{0}u_{0,i}u_{0,j}$ iff $R_{1}u_{1,i}u_{1,j}$ . The concatenation of two tuples $\overline {u}$ and $\overline {v}$ will usually be denoted by simple juxtaposition (as in $\overline {u}\,\overline {v}$ ), but for clarity we may also use the symbol “ $\cdot $ ” as an explicit concatenation operator (as in $\overline {u}\cdot \overline {v}$ ). A configuration over $\mathbb {S}_{0}$ and $\mathbb {S}_{1}$ is a pair $(\overline {u}_{0},\overline {u}_{1})$ consisting, for some k, of a tuple $\overline {u}_{0} \in S_{0}^{k}$ and a tuple $\overline {u}_{1} \in S_{1}^{k}$ .

Definition 2.27. Let $\mathbb {S}_{0} = (S_{0},R_{0},V_{0})$ and $\mathbb {S}_{1} = (S_{1},R_{1},V_{1})$ be two Kripke models; as a convention, when $\mathbb {S}_{i}$ is one of these two models, we write $\mathbb {S}_{-i}$ to denote the other. We define the game $\mathcal {E}^{\infty }_k(\mathbb {S}_{0},\mathbb {S}_{1})$ between two players, Spoiler (male) and Duplicator (female). A position in this game is a configuration over $\mathbb {S}_{0}$ and $\mathbb {S}_{1}$ . The game starts at some initial configuration $(\overline {s}_{0},\overline {s}_{1})$ and consists of k rounds. A single round of the game consists of a short interaction between the two players, of the following kind.

First Spoiler chooses to perform one of the following types of moves:

1. 1. First-order move; the round then consists of the following moves:

   • – Spoiler chooses a structure $\mathbb {S}_{i}$ and an element $u_i \in S_i$ ;

   • – Duplicator responds with an element $u_{-i} \in S_{-i}$ .

2. 2. Second-order move; the round now consists of the following moves:

   • – Spoiler chooses a structure $\mathbb {S}_{i}$ and an infinite set $U_i \subseteq S_i$ ;

   • – Duplicator responds with an infinite set $U_{-i} \subseteq S_{-i}$ ;

   • – Spoiler chooses an element $u_{-i} \in U_{-i}$ ;

   • – Duplicator responds with an element $u_i \in U_i$ .

The sequences $\overline {u}_{0} \in S_0^n$ and $\overline {u}_{1} \in S_1^n$ of elements chosen up to round n are then extended to $\overline {u}^{\prime }_{0} \mathrel {:=} \overline {u}_{0}\cdot u_{0} \in S_{0}^{n+1}$ and $\overline {u}^{\prime }_{1} \mathrel {:=} \overline {u}_{1}\cdot u_{1} \in S_{1}^{n+1}$ . Duplicator wins a match of this game if, after the final k-th round, the resulting configuration $(\overline {s}_{0}\overline {u}_{0},\overline {s}_{1}\overline {u}_{1})$ consists of locally isomorphic tuples.

Note that the only items that are recorded in a play of this game are the objects picked by the players, not the subsets, and note as well that there are no constraints on the internal structure of the infinite sets chosen by the players. In particular, Duplicator does not have to establish an isomorphism between the sets picked by Spoiler and by herself.

In our context we will mainly be interested in the versions of this Ehrenfeucht–Fraïssé game that are played on pointed Kripke models.

Definition 2.28. Let $(\mathbb {S},s)$ and $(\mathbb {S}',s')$ be two pointed Kripke models. We let $\mathcal {E}^{\infty }_k(\mathbb {S},\mathbb {S}')@(s,s')$ denote the k-round Ehrenfeucht–Fraïssé game on $\mathbb {S}$ and $\mathbb {S}'$ that starts from the initial configuration $(s,s')$ . In this context we define a k-configuration to be a pair $(\overline {u},\overline {u}')$ of $k+1$ -tuples such that $u_{0} = s$ and $u^{\prime }_{0} = s^{\prime }$ .

If Duplicator has a winning strategy in this initialized game, we write $\mathbb {S},s \mathrel {\cong ^{\infty }_{k}} \mathbb {S}',s'$ .

Note that since the Ehrenfeucht–Fraïssé game on pointed models has an initial configuration consisting of 1-tuples, the configuration reached after k moves of the game is indeed what we defined above as a k-configuration.

We conclude this subsection by mentioning the following adequacy result for $\mathtt {FO}^{\infty }$ . For a proof we refer to Väänänen [28], where a more general result (Theorem 10.46) is stated and proved.

Proposition 2.29. Let $(\mathbb {S},s)$ and $(\mathbb {S}',s')$ be two pointed Kripke structures. Then the following are equivalent, for every n:

1. (a) $\mathbb {S},s \mathrel {\cong ^{\infty }_{n}} \mathbb {S}',s$ ;

2. (b) $\mathbb {S} \models \varphi [s]$ iff $\mathbb {S}' \models \varphi [s']$ , for every $\varphi (x)\in \mathtt {FO}^{\infty }$ of quantifier depth $\leq n$ .

3 Bisimulation invariance

3.1 Introduction

In this section we prove our main expressiveness result, Theorem 2.25, which characterises $\mathtt {GML}^{\infty }$ as the -invariant fragment of $\mathtt {FO}^{\infty }$ , and $\mathtt {ML}^{\infty }$ as its -fragment. We will focus on the case of $\mathtt {GML}^{\infty }$ , the proof details for the case of $\mathtt {ML}^{\infty }$ can be found in [2].

Bisimulation invariance theorems are model-theoretic characterisation theorems, i.e., results that link certain semantic properties to the syntactic shape of formulas. This line of research started with van Benthem’s seminal result, which identifies basic modal logic as the bisimulation invariant fragment of first-order logic [3]. This result has been extended in many directions; for instance, de Rijke was the first to prove a similar result for graded modal logic [24]. Van Benthem’s and de Rijke’s proofs are rooted in classical model theory, with a prominent role for the notion of compactness.

Our proof will be game-theoretic in nature, following the proof strategy that was initiated by Rosen [25], who gave an alternative proof of van Benthem’s theorem which does not rely on compactness of first-order logic (and which transfers as well to the setting of finite model theory). Otto [23], applying the game-theoretic method to graded modal logic, recently obtained a result that applies in the settings of both general and finite models. Our approach can be seen as an extension of Otto’s approach to include the infinity quantifier (with the note that for obvious reasons it does not make sense to study the logics of our interest in the setting of finite models). For more information on the game-theoretic approach we refer to Goranko and Otto’s handbook article [16].

Before diving into the proof details, we sketch an overview of the proof. First of all, we will stratify the language $\mathtt {GML}^{\infty }$ into layers:

$$\begin{align*}\mathtt{GML}^{\infty} = \bigcup_{q,n} \mathtt{GML}^{\infty}_{q,n}, \end{align*}$$

where $\mathtt {GML}^{\infty }_{q,n}$ consists of those formula in $\mathtt {GML}^{\infty }$ of depth at most q and rank at most n. Each fragment $\mathtt {GML}^{\infty }_{q,n}$ comes with an associated bounded notion of bisimilarity, , and the point of this stratification lies in the fact that each set $\mathtt {GML}^{\infty }_{q,n}$ is finite up to logical equivalence. This means that for each equivalence class C of there is a characteristic formula $\chi _{C} \in \mathtt {GML}^{\infty }_{q,n}$ such that any pointed model satisfies $\chi _{C}$ iff it belongs to C.

The key observation in the proof of Theorem 2.25 is then that

(2)

where $n = 3^{\mathit {qd}(\varphi )}$ , $\mathit {qd}(\varphi )$ being the quantifier depth of $\varphi $ . As we will see, it easily follows from (2) that any bisimulation-invariant formula $\varphi (x)$ is equivalent to the $\mathtt {GML}^{\infty }_{n,n}$ -formula $\bigvee \chi _{C}$ , where we take the disjunction over all cells C of that contain a pointed model satisfying $\varphi $ .

For the proof of (2) we develop some model theory for $\mathtt {FO}^{\infty }$ and $\mathtt {GML}^{\infty }$ . In particular, we will first show that every bisimulation-invariant $\mathtt {FO}^{\infty }$ -formula $\varphi (x)$ is local, in the sense that its truth only depends on a certain neighbourhood of the point referred to by x. Our second model-theoretic result states that for tree models, we may “upgrade” the relation to the game-based indistinguishability relation $\mathrel {\cong ^{\infty }_{n}}$ of Definition 2.28. It then follows from the adequacy of Ehrenfeucht–Fraïssé games (Proposition 2.29) that a bisimulation-invariant $\mathtt {FO}^{\infty }$ -formula $\varphi (x)$ of quantifier depth n is -invariant indeed.

In the final subsection we will then see how all these observations can be assembled in order to prove Theorem 2.25.

3.2 A stratification of the language

As mentioned in the introduction to this section, we will start with stratifying the language $\mathtt {GML}^{\infty }$ into layers.

Definition 3.1. We let $\mathtt {GML}^{\infty }_{q,n}$ consist of those formula in ${\mathtt {GML}^{\infty }}$ that have depth at most q and rank at most n.

As was observed by Otto [23] for graded modal logic (i.e., without the infinity diamond), in order to stratify the language $\mathtt {GML}^{\infty }$ into layers that are finite up to logical equivalence, it does not suffice to confine attention to the modal depth of formulas: one needs to take their rank into consideration as well. We leave the (straightforward) verification of the following proposition as an exercise to the reader.

Proposition 3.2. For each $q,n$ the set $\mathtt {GML}^{\infty }_{q,n}$ is finite, up to logical equivalence.

We will adapt the bisimilarity game of Definition 2.11 to the setting of these fragments, by restricting the size of the sets that Spoiler can pick, as well as the length of the game.

Definition 3.3. The -bisimilarity game, with $q,n \in \mathbb {N}$ , is the version of the bisimilarity game of Definition 2.11 where (i) Spoiler can only pick subsets that are either infinite or of size $\leq n$ , and (ii) instead of (potentially) lasting infinitely many rounds, the game now finishes after q many rounds.

As in our previous definitions, two pointed models $(\mathbb {S},s),(\mathbb {S}',s')$ are -bisimilar, denoted by , if Duplicator has a winning strategy in this version of the game, initialised at position $(s,s')$ .

The following result highlights the close relation between the set of $\mathtt {GML}^{\infty }_{q,n}$ -formulas and the bisimilarity equivalence relation .

Theorem 3.4. Fix two natural numbers $q,n\in \mathbb {N}$ . For any pointed Kripke model $(\mathbb {S},s)$ there is a $\mathtt {GML}^{\infty }_{q,n}$ -formula $\chi _{q,n}^{\mathbb {S},s}$ such that the following are equivalent, for any pointed Kripke model $(\mathbb {S}',s')$ :

1. 1. ,

2. 2. $(\mathbb {S}',s') \,{\equiv }_{q,n\,}^{\#,\infty } (\mathbb {S},s)$ ,

3. 3. $(\mathbb {S}',s')\Vdash \chi _{q,n}^{\mathbb {S},s}$ .

We skip the proof of this result, which proceeds via a routine induction on the modal depth n.

Note that in particular, Theorem 3.4 states that every -equivalence class of pointed Kripke models is characterised by a single $\mathtt {GML}^{\infty }_{q,n}$ formula. Furthermore, by our earlier observation that the set ${\equiv }_{q,n}^{\#,\infty }$ is finite up to logical equivalence, we find that the equivalence relation has finite index. As a corollary of these two observations, we obtain the following result, which we will need in the proof of our bisimulation invariance theorem. Given an equivalence relation E on the class of pointed models, we call a class of pointed models $K E$ -saturated if it is a union of E-cells, or, equivalently: if we have $(\mathbb {S},s) \in K$ iff $(\mathbb {S}',s') \in K$ , whenever $(\mathbb {S},s)$ and $(\mathbb {S}',s')$ are equivalent, according to E.

Proposition 3.5. Let q and n be two natural numbers, and let K be a -saturated class of pointed models. Then there is a formula $\chi _{K} \in \mathtt {GML}^{\infty }_{q,n}$ such that $\mathbb {S},s \Vdash \chi _{K}$ iff $(\mathbb {S},s)$ belongs to K, for any pointed model $(\mathbb {S},s)$ .

Proof. Given a cell C of , we fix some formula $\chi _{C}$ in $\mathtt {GML}^{\infty }_{q,n}$ , as given by Theorem 3.4; that is, $\chi _{C}$ characterises the pointed models in C.

Let $q,n$ and K be as in the formulation of the proposition. Define $\chi _{K} \mathrel {:=} \bigvee \chi _{C}$ , where we take the disjunction over all cells C of that contain a pointed model in K. Observe that the formula $\chi _{K}$ is well formed since the relation has finite index. We claim that $\chi _{K}$ characterises K, in the sense that, for any pointed model $(\mathbb {S},s)$ :

$$\begin{align*}(\mathbb{S},s) \text{ belongs to } K \text{ iff } \mathbb{S},s \Vdash \chi_{K}. \end{align*}$$

To see this, fix a pointed model $(\mathbb {S},s)$ , and let C be its equivalence class under the relation . It follows by Theorem 3.4 that $\mathbb {S},s \Vdash \chi _{C}$ .

If $(\mathbb {S},s)$ belongs to K then by definition of $\chi _{K}$ the formula $\chi _{C}$ will be one of the disjuncts of $\chi _{K}$ , so that we find $\mathbb {S},s \Vdash \chi _{K}$ as required. Conversely, if $\mathbb {S},s \Vdash \chi _{K}$ then by definition of $\chi _{K}$ we have that $\mathbb {S},s \Vdash \chi _{C'}$ for some -cell $C'$ which contains a pointed model $(\mathbb {S}',s')$ in K. It follows from $\mathbb {S},s \Vdash \chi _{C'}$ that $C' = C$ , and so both $(\mathbb {S},s)$ and $(\mathbb {S}',s')$ belong to this class. This means that , and from this we find $(\mathbb {S},s)$ in K by the assumption that K is -saturated.

3.3 Locality for bisimulation-invariant $\mathtt {FO}^{\infty }$ formulas

One of the key concepts that Rosen uses in his proof is that of locality: the property that the meaning of a first-order formula $\varphi (x)$ in a structure $\mathbb {S}$ only depends on a small neighbourhood of (the point associated with) x. Our goal here will be to show that this property extends to formulas involving the infinity quantifier, at least to the ones that are bisimulation invariant.

The notion of locality is defined in terms of Gaifman distance.

Definition 3.6. Let $\mathbb {S} = (S,R,V)$ be a Kripke model. Where $E \subseteq S \times S$ is the union of R and its converse, we define the Gaifman distance $\mathit {gaif}(s,t)$ between two points s and t to be $n \in \mathbb {N}$ if n is the length of the shortest E-path linking s to t, and we set $\mathit {gaif}(s,t) \mathrel {:=} \infty $ if there is no such E-path. Given a state $s \in S$ and a natural number n, the n-neighbourhood $N^{\mathbb {S}}(s,n)$ of s consists of those states t in $\mathbb {S}$ such that $\mathit {gaif}(s,t) \leq n$ ; we let $\mathbb {B}^{\mathbb {S}}(s,n)$ denote the induced substructure on $N^{\mathbb {S}}(s,n)$ .

An $\mathtt {FO}^{\infty }$ formula $\varphi $ is n-local if we have $\mathbb {S}\vDash \varphi (s)$ iff $\mathbb {S}'\vDash \varphi (s')$ , for any two pointed Kripke models $(\mathbb {S},s)$ and $(\mathbb {S}',s')$ such that $\mathbb {B}^{\mathbb {S}}(s,n)$ and $\mathbb {B}^{\mathbb {S}'}(s',n)$ are isomorphic.

We will now prove that every bisimulation-invariant $\mathtt {FO}^{\infty }$ -formula $\varphi (x)$ is $3^{q}$ -local, where q is the quantifier depth of $\varphi $ . In fact, we will prove a slightly stronger statement (as in the case of the bisimulation invariance results for first-order logic): it turns out that the only invariance property that we need to prove locality concerns disjoint unions. We assume that the reader is familiar with this model-theoretic construction (the precise definition can be found in [5]). It is easy to see that a pointed model is -bisimilar to its representation inside a disjoint union; from this it follows that bisimulation invariance implies invariance under disjoint unions.

Proposition 3.7. Let $\varphi (x) \in \mathtt {FO}^{\infty }$ be invariant under taking disjoint unions. Then $\varphi $ is $3^{q}$ -local, where $q = \mathit {qd}(\varphi )$ .

Proof. Fix a formula $\varphi (x) \in \mathtt {FO}^{\infty }$ of quantifier depth q, and assume that $\varphi $ is invariant under taking disjoint unions. Define $n \mathrel {:=} 3^{q}$ , and let $(\mathbb {S},s)$ be an arbitrary pointed model. In order to prove the proposition, by invariance under taking disjoint unions it obviously suffices to prove that

(3) $$ \begin{align} \mathbb{S} \uplus \mathbb{D} \models \varphi[s] \text{ iff } \mathbb{B} \uplus \mathbb{D} \models \varphi[s], \end{align} $$

where $\mathbb {B} \mathrel {:=} \mathbb {B}^{\mathbb {S}}(s,n)$ and $\mathbb {D}$ is the disjoint union of q many copies of $\mathbb {S}$ and q many copies of $\mathbb {B}$ . As mentioned, our proof of (3) will be game-theoretic in nature. In view of Proposition 2.29 it suffices to show the following:

(4) $$ \begin{align} \text{Duplicator has a winning strategy in } \texttt{EF}_{q}^{\infty}(\mathbb{S} \uplus \mathbb{D}, \mathbb{B} \uplus \mathbb{D})@(s,s). \end{align} $$

To formulate our proof of (4), we need to introduce some further terminology and notation. To start with, we need some more detail in our notation for the models $\mathbb {S} \uplus \mathbb {D}$ and $\mathbb {B} \uplus \mathbb {D}$ . For $i \in \{-q,\ldots ,q\}$ we let $\mathbb {S}_{i}$ be the isomorphic copy of $\mathbb {S}$ based on the set $S_{i} = S \times \{i\}$ , where the projection map $\pi _{i}: S_{i} \to S$ is the witnessing isomorphism, and similarly for $\mathbb {B}_{i}$ . We identify $\mathbb {S}_{0}$ with $\mathbb {S}$ and $\mathbb {B}_{0}$ with $\mathbb {B}$ , and define

$$\begin{align*}\mathbb{D} \mathrel{:=} \biguplus_{-q \leq i < 0} \mathbb{S}_{i} \;\uplus\; \biguplus_{0 < i \leq q} \mathbb{B}_{i}, \end{align*}$$

so that we may think of $\mathbb {S} \uplus \mathbb {D}$ as the structure $\biguplus _{-q \leq i \leq 0} \mathbb {S}_{i} \;\uplus \; \biguplus _{0 < i \leq q} \mathbb {B}_{i}$ , and of $\mathbb {B} \uplus \mathbb {D}$ as the structure $\biguplus _{-q \leq i < 0} \mathbb {S}_{i} \;\uplus \; \biguplus _{0 \leq i \leq q} \mathbb {B}_{i}$ . We will refer to a point u in $\mathbb {S} \uplus \mathbb {D}$ as being $\mathbb {K}$ -type, with $\mathbb {K} \in \{ \mathbb {S},\mathbb {B} \}$ , if u belongs to $\mathbb {K}_{i}$ for some $i\in \{-q,..q\}$ .

Given a k-configuration $(\overline {u},\overline {u}')$ arising during a match of the game, we let $N_{k}(\overline {u})$ and $N_{k}(\overline {u}')$ be the sets

$$\begin{align*}N_{k}(\overline{u}) \mathrel{:=} \bigcup_{i} N^{\mathbb{S}\uplus\mathbb{D}}(u_{i},3^{q-k}), \quad N^{\prime}_{k}(\overline{u}^{\prime}) \mathrel{:=} \bigcup_{i} N^{\mathbb{B}\uplus\mathbb{D}}(u^{\prime}_{i},3^{q-k}), \end{align*}$$

respectively. In other words, $N_{k}(\overline {u})$ is the union of the $3^{q-k}$ -neighbourhoods of the different worlds in $\overline {u}$ . In particular, every point in $N_{k}(\overline {u})$ is, at most, at a distance $3^{q-k}$ from one of the worlds in $\overline {u}$ . Analogous observations apply to $N^{\prime }_{k}(\overline {u}^{\prime })$ .

The key observation in the proof of (4) is that Duplicator can maintain the condition that, where $(\overline {u},\overline {u}')$ is any configuration reached during a play of $\texttt {EF}_{q}^{\infty }(\mathbb {S} \uplus \mathbb {D}, \mathbb {B} \uplus \mathbb {D})@(s,s)$ ,

• (†) there is a local isomorphism $f: N_{k}(\overline {u}) \to N^{\prime }_{k}(\overline {u}^{\prime })$ such that $f(u_{i}) = u^{\prime }_{i}$ , for all i.

It should be clear that this condition holds at the start of the game, where $k = 0$ .

Now assume that, inductively, for some $k<q$ the condition (†) holds for some k-configuration $(\overline {u},\overline {u}')$ , witnessed by some local isomorphism f. We need to prove that to any challenge of Spoiler, Duplicator has a response that guarantees the resulting $k+1$ -configuration to again satisfy (†). We show this by distinguishing cases, as to the kind of move Spoiler makes.

• Case 1. First assume that Spoiler makes a first-order move. In this case we proceed very much in the same way as Goranko and Otto in [16]. Without loss of generality we may assume that he picks an element, say, u, of the structure $\mathbb {S} \uplus \mathbb {D}$ ; then we need to identify a point $u'$ in $\mathbb {B} \uplus \mathbb {D}$ as a suitable reply for Duplicator. We make a further case distinction as to whether u is close to one of the points in the existing tuple $\overline {u}$ or not.

  • Case 1a. $\mathit {gaif}(u,u_{i}) \leq 2 \cdot 3^{q-(k+1)}$ for some $i \in \{0,\ldots ,k\}$ . The crucial observation in this case is that we have $N_{k+1}(\overline {u}\cdot u) \subseteq N_{k}(\overline {u})$ ; the verification of this statement is a simple exercise in Gaifman metric. We then simply define $u' \mathrel {:=} f(u)$ , and it is straightforward to check that f restricts to a local isomorphism from $N_{k+1}(\overline {u}\cdot u)$ to $N^{\prime }_{k+1}(\overline {u}^{\prime }\cdot u^{\prime })$ . Since we have $f(u_{i}) = u^{\prime }_{i}$ by assumption and $f(u) = u'$ by definition, this shows that indeed Duplicator can keep the condition (†) for one more round.

  • Case 1b. $\mathit {gaif}(u,u_{i})> 2 \cdot 3^{q-(k+1)}$ for all $i \in \{0,\ldots ,k\}$ . The crucial statement is now that the set $N^{\mathbb {S}\uplus \mathbb {D}}(u,3^{q-(k+1)})$ does not overlap with any set $N^{\mathbb {S}\uplus \mathbb {D}}(u_{i},3^{q-(k+1)})$ , so that $N_{k+1}(\overline {u}\cdot u)$ is the disjoint union of the sets $\bigcup _{i} N^{\mathbb {S}\uplus \mathbb {D}}(u_{i},3^{q-(k+1)})$ and $N^{\mathbb {S}\uplus \mathbb {D}}(u,3^{q-(k+1)})$ . We will assume that u is an $\mathbb {S}$ -type point of $\mathbb {S}\uplus \mathbb {D}$ (the case where u is $\mathbb {B}$ -type is dealt with analogously). That is, u belongs to $\mathbb {S}_{j}$ for some j, and we may write $u = (\pi _{j}(u),j)$ with $\pi _{j}(u)$ in $\mathbb {S}$ .

    Since $\overline {u}'$ comprises at most $k+1$ elements, where $k < q$ , $\mathbb {D}$ contains q distinct copies of $\mathbb {S}$ , and the initial state $u^{\prime }_{0}$ does not belong to $\mathbb {D}$ (but to $\mathbb {B}$ ), the target structure $\mathbb {B} \uplus \mathbb {D}$ will have a “fresh” copy of $\mathbb {S}$ , so to speak. That is, we may consider some r such that $\mathbb {S}_{r}$ contains none of the $u^{\prime }_{i}$ . We now define $u' \mathrel {:=} (\pi _{j}(u),r)$ ; in other words, we use the obvious isomorphism between $\mathbb {S}_{j}$ and $\mathbb {S}_{r}$ to find $u'$ . Now consider the following map $f'$ on $N_{k+1}(\overline {u}\cdot u)$ :

    (5) $$ \begin{align} f'(s) \mathrel{:=} \left\{ \begin{array}{ll} f(s), & \text{if } s \in \bigcup_{i} N^{\mathbb{S}\uplus\mathbb{D}}(u_{i},3^{q-(k+1)}), \\[2mm] (\pi_{j}(s),r), & \text{if } s \in N^{\mathbb{S}\uplus\mathbb{D}}(u,3^{q-(k+1)}). \end{array} \right. \end{align} $$
    It is then a routine exercise to verify that $f'$ is well defined, and that it provides the required local isomorphism between $N_{k+1}(\overline {u}\cdot u)$ and $N^{\prime }_{k+1}(\overline {u}^{\prime }\cdot u^{\prime })$ . Since again we have $f^{\prime }(u_{i}) = u^{\prime }_{i}$ by assumption and $f'(u) = u'$ by definition, it follows that in this case as well, Duplicator can keep the condition (†) for one more round.

• Case 2. Now assume that Spoiler makes a second-order move. Without loss of generality we may assume that he picks an infinite subset, say, U, of the structure $\mathbb {S}\uplus \mathbb {D}$ . Similar to Case 1, we make a further case distinction, but now as to whether infinitely many elements of U are close to one of the points in the existing tuple $\overline {u}$ or not.

  • Case 2a. There are infinitely many $u \in U$ such that $\mathit {gaif}(u,u_{i}) \leq 2 \cdot 3^{q-(k+1)}$ for some $i \in \{0,\ldots ,k\}$ .

    Let $X \subseteq U$ be the set of all these elements, then the key observation—as in the first-order move case—is that for each $u \in X$ we have $N_{k+1}(\overline {u}\cdot u) \subseteq N_{k}(\overline {u})$ . Let

    $$\begin{align*}U' \mathrel{:=} f[X] \end{align*}$$
    be Duplicator’s response to Spoiler’s move U. Since f is a bijection between $N_{k}(\overline {u})$ and $N^{\prime }_{k}(\overline {u}^{\prime })$ , we immediately see that $U'$ is an infinite subset of $N^{\prime }_{k}(\overline {u}')$ . Now suppose that, continuing the match, Spoiler picks an element $u' \in U'$ ; then by definition there is a $u \in X$ such that $u' = f(u)$ , and Duplicator will pick this u as her response to Spoiler’s move $u'$ . As in Case 1 above, it is then straightforward to verify that the restriction of f to the set $N_{k+1}(\overline {u}\cdot u)$ witnesses that Duplicator has maintained (†) for one more round.

  • Case 2b. There are infinitely many $u \in U$ such that $\mathit {gaif}(u,u_{i})> 2 \cdot 3^{q-(k+1)}$ for all $i \in \{0,\ldots ,k\}$ .

    Let $X \subseteq U$ be the set of all these elements, then the key observation is, as in Case 1b, that for each $u \in X$ we have

    $$\begin{align*}N_{k+1}(\overline{u}\cdot u) \;=\; \bigcup_{i} N^{\mathbb{S}\uplus\mathbb{D}}(u_{i},3^{q-(k+1)}) \;\uplus\; N^{\mathbb{S}\uplus\mathbb{D}}(u,3^{q-(k+1)}). \end{align*}$$
    Furthermore, by the pigeonhole principle, X must contain either infinitely many $\mathbb {S}$ -type points or infinitely many $\mathbb {B}$ -type points. We assume the first (again, the other case is very similar). For $j \in \{-q,\ldots ,0\}$ , let $X_{j}$ be the set of points in X that belong to $\mathbb {S}_{j}$ ; then, once more by the pigeonhole principle, there is an index j such that $X_{j}$ is infinite. As in Case 1b we may then take some r such that $\mathbb {S}_{r}$ contains none of the $u^{\prime }_{i}$ . We are now ready to define Duplicator’s response to Spoiler’s move U:
    $$\begin{align*}U' \mathrel{:=} \{ (\pi_{j}(u),r) \mid u \in X_{j} \}. \end{align*}$$
    That is, again we use the obvious isomorphism between $\mathbb {S}_{j}$ and $\mathbb {S}_{r}$ to find $U'$ in $\mathbb {S}_{r}$ as the counterpart of $X_{j}$ in $\mathbb {S}_{j}$ . Clearly then, $U'$ is infinite, so that it constitutes a legitimate move for Duplicator. Now assume that Spoiler continues the match by picking an element $u' \in U$ . Then by definition $u'$ is of the form $u' = (\pi _{j}(u),r)$ for some $u \in X_{j}$ , and since $X_{j} \subseteq U$ , Duplicator may pick this element u as her response to Spoiler.

    As discussed in Case 1b, it is now straightforward to verify that the map $f'$ as defined in (5), is a local isomorphism from $N_{k+1}(\overline {u}\cdot u)$ to $N^{\prime }_{k+1}(\overline {u}^{\prime }\cdot u^{\prime })$ that witnesses the fact that Duplicator has carried the condition (†) one round further.

This finishes the proof of (4), and, as discussed, this suffices to prove the proposition.

3.4 Upgrading

As we saw in the introduction to this section, the second result on which the proof of the key observation (2) rests, is that for tree models, the relation may be “upgraded” to the game-based indistinguishability relation $\mathrel {\cong ^{\infty }_{n}}$ of Definition 2.28. This observation is the content of Theorem 3.9, which we will state and prove in this subsection.

Recall that a tree is a structure $(T,R)$ such that, for some fixed node r, every node t is reachable from r by a unique finite path. The node r, which is in fact uniquely determined by this property, is called the root of the tree. We will call a pointed Kripke model $(\mathbb {T},r)$ a tree model if $\mathbb {T}$ is based on a tree with root r.

To formulate and prove Theorem 3.9 we need to introduce some concepts related to tree models.

Definition 3.8. Let $\mathbb {T}$ be a tree model with root r. We use the terms successor/child and predecessor/parent in their usual meaning, and we let the ancestor (descendant) relation be the reflexive-transitive closure of the predecessor (successor) relation. We use ${\downarrow }(u)$ to denote the set of ancestors of u.

The height $h(\mathbb {T})$ of $\mathbb {T}$ is defined as the supremum of the heights of its nodes, where the height $h(u)$ of a node u is defined as its distance to r. Given a tree of finite height, we define the depth $d(u)$ of a node u as the maximal distance of u to any descendant which is a leaf of $\mathbb {T}$ .

Finally, given two nodes u and v in $\mathbb {T}$ , we let $\mathit {lca}(u,v)$ denote the last common ancestor of u and v.

Observe that the root r of a tree of height l is an ancestor of every node u and satisfies $h(r) = 0$ and $d(r) = l$ , and that we have $h(u) + d(u)\leq l$ for any node u. The ancestor relation $R^{*}$ is a partial order on T, which restricts to a linear order on any set of the form ${\downarrow }(u)$ . The least common ancestor map obviously satisfies the conditions $\mathit {lca}(u,u) = u$ , and $\mathit {lca}(u,v) = \mathit {lca}(v,u)$ , for all nodes $u,v$ . It is also easily verified that $u \in {\downarrow }(v)$ iff $\mathit {lca}(u,v) = u$ . Finally, if $\mathit {lca}(u,v_{0})$ and $\mathit {lca}(u,v_{1})$ have the same height, then they must be identical.

Theorem 3.9. Let $(\mathbb {T}, r)$ and $(\mathbb {T}',r')$ be two tree models of height q. Then implies $\mathbb {T}, r \mathrel {\cong ^{\infty }_{q}} \mathbb {T}',r'$ .

Clearly, the goal of our proof for this theorem will be to supply Duplicator with a winning strategy in the Ehrenfeucht–Fraïssé game of length q, between two -equivalent tree models of height q. In the next definition we introduce the notion of q-companionship, which will be a key notion with which Duplicator will link the nodes in the two respective tree models.

Definition 3.10. Let $\mathbb {T}$ and $\mathbb {T}'$ be tree models with roots $r, r'$ , respectively, and let $q \geq h(\mathbb {T})$ . We say that two worlds t in $\mathbb {T}$ and $t'$ in $\mathbb {T}'$ are q-companions, if $h(t) = h(t')$ and for all $u \in {\downarrow }(t)$ and $u' \in {\downarrow }(t')$ with $h(u) = h(u')$ we have .

Here are some basic observations about the notion. First note that nodes can only be q-companions if they have the same height and their respective ancestors are, one by one, also q-companions. In fact, if u and $u'$ are q-companions, then there is a bijection $f: {\downarrow }(u)\to {\downarrow }(u')$ mapping every predecessor v of u to a q-companion $f(v)$ of $u'$ of the same height. The bisimilarity condition on these ancestors becomes stronger for nodes that are closer to the respective roots, to the effect that companions of height q (which must be leaves of the tree) are only required to satisfy the same proposition letters, while the two roots are q-companions iff they are -related. Furthermore, the following observation will turn out to be quite useful.

Lemma 3.11. For any $q>0$ , when restricted to pairs $(\mathbb {T},t)$ where $\mathbb {T}$ is a tree of height at most q, the relation of being q-companions is an equivalence relation of finite index.

Proof. It is almost immediate from the definition that the relation of being q-companions is an equivalence relation. A routine inductive argument shows that this equivalence relation has finite index if we restrict to nodes of arbitrary but fixed height. From this the proposition is immediate.

The following lemma states a very useful back-and-forth property for the q-companionship relation.

Lemma 3.12. Let $\mathbb {T}$ and $\mathbb {T}'$ be two rooted tree-like structures of height q, and let t in $\mathbb {T}$ and $t'$ in $\mathbb {T}'$ be q-companions. Then the following hold.

1. 1. Every descendant v of t has a q-companion $v'$ which is a descendant of $t'$ .

2. 2. If t has infinitely many descendants, all belonging to the same q-companion class, then $t'$ has infinitely many descendants that all belong to this class as well.

Proof. Let $\mathbb {T},\mathbb {T}',t$ and $t'$ be as in the formulation of the lemma.

For the proof of item 1 we first consider the special case where v is a successor of t. By Theorem 3.4 there is a formula $\chi \in \mathtt {GML}^{\infty }_{q-h(v),q}$ characterising the -cell of $(\mathbb {T},v)$ . It follows from $\mathbb {T},v \Vdash \chi $ that $\mathbb {T},t \Vdash \lozenge \chi $ . Observe that the formula $\lozenge \chi $ belongs to the set $\mathtt {GML}^{\infty }_{(q-h(v))+1,q} = \mathtt {GML}^{\infty }_{q-h(t),q}$ , where the equality holds as $h(t) = h(v)-1$ . By the q-companionship of t and $t'$ we obtain that $\mathbb {T}',t'\Vdash \lozenge \chi $ , so that $t'$ must have a successor $v'$ such that $\mathbb {T}', v' \Vdash \chi $ . It is then immediate by Theorem 3.4 that , and since t and $t'$ are q-companions it easily follows that v and $v'$ must be q-companions as well.

The general case, where v is an arbitrary (not necessarily one-step) descendant of t, is then easily derived from the special case via a straightforward induction on the distance from t to v.

For the proof of item 2, let V be an infinite set of nodes in $\mathbb {T}$ that all belong to the same q-companion class. Clearly then all nodes in V have the same height, a number that we will denote as $h(V)$ . Furthermore, since all nodes in V are q-companions of one another, there is a formula $\chi \in \mathtt {GML}^{\infty }_{q-h(V),q}$ characterising the -cell of the nodes in V. This means in particular that $\mathbb {T},v \Vdash \chi $ for all $v \in V$ .

Now consider an arbitrary common ancestor u of all nodes in V; it is easy to see that u has the same distance to each node in V, so that it makes sense to talk about the distance $d(u,V)$ of u to the set V. We will prove, by induction on this distance, that u has a q-companion $u'$ which has infinitely many descendants that all belong to the q-companion class of V. Clearly this suffices to prove item 2.

In the base step of this induction we assume that $d(u,V) = 1$ ; that is, $V \subseteq R(u)$ . Since V is infinite this means that $\mathbb {T},u \Vdash \lozenge ^{\infty } \chi $ . Now observe that as $\chi $ belongs to the set $\mathtt {GML}_{q - h(V),q}^{\infty ,q}$ , we find that $\lozenge ^{\infty } \chi \in \mathtt {GML}_{(q - h(V)) + 1,q}^{\infty } = \mathtt {GML}_{q - h(u),q}^{\infty }$ . From this and the assumption on u and $u'$ it follows that $\mathbb {T}',u' \Vdash \lozenge ^{\infty } \chi $ . In other words, there is an infinite set $V'$ of successors of $u'$ , such that each $v'\in V'$ satisfies the characteristic formula $\chi $ . By Theorem 3.4 this means that , for each $v' \in V'$ and $v \in V$ , and since the predecessor $u'$ of any such $v'$ is a q-companion of the predecessor u of any such v, we find that every $v' \in V'$ is a q-companion of every $v \in V$ . But then we are done, since $V'$ is an infinite set of descendants of $u'$ .

For the inductive step, assume that $d(u,V) = k + 1$ . We make a case distinction.

First assume that u has a successor w such that $|V \cap R^{k}(w)|$ is infinite. By (the proof of) item 1, $u'$ has a successor $w'$ which is a q-companion of w. Clearly we have $d(w,V) = d(u,V) -1$ , so that we may apply the inductive hypothesis to w. This yields an infinite set $V'$ of descendants of $w'$ , all belonging to the same q-companion class as the nodes in V. It is not hard to see that this set $V'$ meets the required conditions with respect to u and V as well.

If, on the other hand, u has no successor w such that $|V \cap R^{k}(w)|$ is infinite, then it must have an infinite set W of successors, each of which has at least one descendant in V. Without loss of generality we may assume that all nodes in W are q-companions of one another (if not, by Lemma 3.11 W would have an infinite subset with this property, and we could continue with this subset). This means in particular that the nodes in W belong to the same cell of the equivalence relation . Writing $\psi \in \mathtt {GML}^{\infty }_{q-(h(u)+1),q}$ for the characteristic formula of this equivalence class, we clearly have that u satisfies the formula $\lozenge ^{\infty }\psi $ . But since this formula belongs to the set $\mathtt {GML}^{\infty }_{q-h(u),q}$ , it must hold at the q-companion $u'$ of u as well, i.e., there is an infinite set $W'$ of successors of $u'$ , all satisfying the formula $\psi $ . As before we may derive from this that every $w' \in W'$ is a q-companion of every $w \in W$ . But then by item 1 every $w' \in W'$ has a descendant $v^{\prime }_{w^{\prime }}$ that is a q-companion of some descendant in V of some successor w of u. From this we easily derive that the set $V^{\prime } \mathrel {:=} \{ v^{\prime }_{w^{\prime }} \mid w^{\prime } \in W^{\prime } \}$ has the required properties—note that the set is infinite since $W'$ is infinite and $\mathbb {T}^{\prime }$ is a tree model.

Where the q-companion relation concerns pairs of single nodes and their respective ancestors, to provide Duplicator with a winning strategy in the Ehrenfeucht–Fraïssé game we will compare tuples of (not necessarily related) points, and the subtrees that they induce.

Definition 3.13. Let $\mathbb {T} = (T,R)$ be a tree, and let, for $k\geq 1$ , the k-tuple $\overline {u} = (u_{0},u_{1},\ldots ,u_{k-1})$ be such that $u_{0}$ is the root of $\mathbb {T}$ . Then we define $T_{\overline {u}} \mathrel {:=} \bigcup _{0\leq i<k}{\downarrow }(u_{i})$ and we let $\mathbb {T}_{\overline {u}}$ denote the subtree of $\mathbb {T}$ based on the set $T_{\overline {u}}$ ; we call $\mathbb {T}_{\overline {u}}$ the subtree of $\mathbb {T}$ that is induced by $\overline {u}$ .

Let $\mathbb {T}$ and $\mathbb {T}'$ be two tree models and let $\overline {u}$ and $\overline {u}'$ be two k-tuples of nodes in, respectively, $\mathbb {T}$ and $\mathbb {T}'$ , such that $k \geq 1$ and $u_{0}$ and $u^{\prime }_{0}$ are, respectively, the roots of $\mathbb {T}$ and $\mathbb {T}'$ . We say that $\overline {u}$ and $\ \overline {u}'$ are q-similar, notation: $\mathbb {T},\overline {u} \approx ^{\downarrow }_{q} \mathbb {T}',\overline {u}'$ , if there is an isomorphism f from $\mathbb {T}_{\overline {u}}$ to $\mathbb {T}^{\prime }_{\overline {u}^{\prime }}$ such that $f(u_{i}) = u^{\prime }_{i}$ , for all i, and x and $f(x)$ are q-companions, for all x in $\mathbb {T}_{\overline {u}}$ .

The main observation in the proof of Theorem 3.9 is that Duplicator can make sure that any configuration arising during a play of the game will consist of two q-similar tuples, provided, of course, that the starting configuration meets this condition. The following lemma is the key result here; it states that Duplicator can maintain the q-similarity condition on configurations for one single round, systematically defending herself from any attack by Spoiler. Recall that we write $X \subseteq _{\omega } Y$ if X is a finite subset of Y.

Lemma 3.14. Let $\mathbb {T},\mathbb {T}'$ be two rooted tree-like structures of height q, and let, for some $0 \leq k < q$ , $(\overline {u},\overline {u}')$ be a k-configuration such that $\mathbb {T},\overline {u} \approx ^{\downarrow }_{q} \mathbb {T}',\overline {u}'$ . Then the following hold.

1. 1. For every u in $\mathbb {T}$ there is a $u'$ in $\mathbb {T}'$ such that $\mathbb {T},\overline {u}\cdot u \approx ^{\downarrow }_{q} \mathbb {T}',\overline {u}^{\prime }\cdot u^{\prime }$ .

2. 2. For every $U \subseteq _{\omega } \mathbb {T}$ there is a set $U' \subseteq _{\omega } \mathbb {T}'$ such that for every $u' \in U'$ there is a $u \in U$ with $\mathbb {T},\overline {u}\cdot u \approx ^{\downarrow }_{q} \mathbb {T}',\overline {u}^{\prime }\cdot u^{\prime }$ .

Proof. Let $\mathbb {T},\mathbb {T}',\overline {u}$ and $\overline {u}'$ be as in the formulation of the lemma. Write $\overline {u} = u_{0}\cdots u_{k}$ and $\overline {u}^{\prime } = u^{\prime }_{0}\cdots u^{\prime }_{k}$ , and recall that $u_{0}$ and $u^{\prime }_{0}$ are the roots of $\mathbb {T}$ and $\mathbb {T}^{\prime }$ , respectively. Let $f: \mathbb {T}_{\overline {u}} \to \mathbb {T}^{\prime }_{\overline {u}^{\prime }}$ be an isomorphism witnessing the q-similarity of $\overline {u}$ and $\overline {u}'$ .

We first prove item 1. Let u be an arbitrary node in $\mathbb {T}$ . The case where u is actually a node of $\mathbb {T}_{\overline {u}}$ is easily dealt with by taking $u' \mathrel {:=} f(u)$ , so assume otherwise.

Consider the set

$$\begin{align*}X_{u} \mathrel{:=} \{ \mathit{lca}(u_{i},u) \mid 0 \leq i \leq k \}. \end{align*}$$

Since u does not belong to $T_{\overline {u}}$ , clearly each node in $X_{u}$ is a proper ancestor of u, and $X_{u}$ is linearly ordered by the ancestor relation. In particular, $X_{u}$ has a last element in this order, which we shall denote as $d_{u}$ . Let $Y_{u}$ be the set of nodes $u_{i}$ in $\overline {u}$ for which $d_{u} \neq u_{i}$ but $d_{u} = \mathit {lca}(u_{i},u)$ . If $Y_{u} = \emptyset $ it must be the case that for some i, $d_{u} = u_{i}$ while $d_{u} \not \in {\downarrow }(u_{j})$ for any $u_{j}\neq u_{i}$ . This case can be easily dealt with using Lemma 3.12(1), so in the sequel we assume that $Y_{u}$ is not empty. Note that $u_{0}$ , being the root of $\mathbb {T}$ , does not belong to $Y_{u}$ .

Consider the set $R(d_{u})$ of successors of $d_{u}$ . For each $x \in Y_{u} \cup \{ u \}$ we let $z_{x}$ denote the unique successor of $d_{u}$ which is an ancestor of x, and define $Z_{Y} \mathrel {:=} \{ z_{y} \mid y \in Y_{u} \}$ . It follows from the assumptions that $Z_{Y} \neq \emptyset $ and that $u_{0}, z_{u} \not \in Z_{Y}$ . Furthermore we obviously have $|Z_{Y}| \leq |Y_{u}|$ , and since $Y_{u} \subseteq \{ u_{i} \mid 0 < i \leq k \}$ we may use the assumption $k<q$ to obtain that $|Z_{Y}| < q$ .

Now we claim that $f(d_{u})$ has a successor $z_{u}'$ which is a q-companion of $z_{u}$ , but is not of the form $f(z)$ for any $z \in Z_{Y}$ . To see this, let $\chi \in \mathtt {GML}^{\infty }_{q-h(z_{u}),q}$ be a characteristic formula of the -cell of $z_{u}$ , and let m be the number of elements of $Z_{Y}$ that satisfy $\chi $ . Obviously then we have $\mathbb {T},d_{u} \Vdash \lozenge ^{\geq m+1}\chi $ , and since $m \leq |Z_{Y}| < q$ , the formula $\lozenge ^{\geq m+1}\chi $ belongs to the set $\mathtt {GML}^{\infty }_{(q- h(z_{u}))+1,q} = \mathtt {GML}^{\infty }_{q-h(u),q}$ . Since $d_{u}$ and $f(d_{u})$ are q-companions, the formula $\lozenge ^{\geq m+1}\chi $ must be preserved, so that $f(d_{u})$ must satisfy $\lozenge ^{\geq m+1}\chi $ as well. Hence $f(d)$ has at least $m+1$ successors satisfying $\chi $ . Using the facts that f is an isomorphism between $\mathbb {T}_{\overline {u}}$ and $\mathbb {T}^{\prime }_{\overline {u}^{\prime }}$ and that $\mathbb {T},z \Vdash \chi $ iff $\mathbb {T}',f(z) \Vdash \chi $ for all $z \in R(u)$ , we may conclude that $|\{ z' \in R'(f(d_{u})) \cap f[Z_{Y}] \mid \mathbb {T}',z' \Vdash \chi \}| = m$ . That is, there are exactly m successors of $f(d_{u})$ that are in the image of $f[Z_{Y}]$ and make $\chi $ true. But then there must a successor $z_{u}'$ of $f(d)$ that satisfies $\chi $ but does not belong to the set $f[Z_{Y}]$ . This node $z_{u}'$ is then the successor of $f(d_{u})$ that we are looking for (Figure 1).

Fig. 1 Lemma 3.14(1).

To finish the proof of the first item, observe that as $z_{u}$ and $z_{u}'$ are q-companions, it follows from Lemma 3.12(1) that $z^{\prime }_{u}$ has a descendant $u'$ which is a q-companion of u. It is then a fairly routine exercise to check that we may extend f to an isomorphism $g: \mathbb {T}_{\overline {u}\cdot u} \to \mathbb {T}^{\prime }_{\overline {u}^{\prime }\cdot u^{\prime }}$ which satisfies in addition that $g(z_{u}) = z^{\prime }_{u}$ and $g(u) = u'$ and that x and $g(x)$ are q-companions, for every x in $\mathbb {T}_{\overline {u}\cdot u}$ . This suffices to show that $\mathbb {T},\overline {u}\cdot u \approx ^{\downarrow }_{q} \mathbb {T}^{\prime },\overline {u}'\cdot u^{\prime }$ .

We now turn to the proof of item 2. Let U be some infinite subset of $\mathbb {T}$ . From the constraints on the set $U'$ that we are looking for, it follows that instead of working with U we may work with any subset of U that is guaranteed to be infinite—we will use this observation repeatedly (without explicit reference). For instance, by Lemma 3.11 we may without loss of generality assume that all nodes in U are q-companions of one another.

Similarly, since $T_{\overline {u}}$ is finite we may, without loss of generality assume that $U \cap T_{\overline {u}} = \emptyset $ . In addition, we may assume that all nodes in U have the same height and belong to the same q-companion class. Then for each $u \in U$ we define the set $X_{u}$ , the node $d_{u}$ , and the set $Y_{u}$ , exactly as in the proof of the first item. Since each $d_{u}$ belongs to the (finite) set of nodes of $\mathbb {T}_{\overline {u}}$ , and each $Y_{u}$ is a subset of the finite set $\{ u_{i} \mid 0 < i \leq k \}$ , we may without loss of generality assume that $d_{u} = d_{v}$ and $Y_{u} = Y_{v}$ , for all $u,v \in U$ . Hence we may drop subscripts and simply write d and Y. If $Y = \emptyset $ it must be the case that $d = u_{i}$ for some i, and as in the proof of item 1 we leave it for the reader to check that this case can be easily dealt with using Lemma 3.12 (in this case with item (2)).

As in the proof of item 1 of this lemma, we now focus on the set $R(d)$ of direct successors of d. For $x \in Y \cup U$ , we define $z_{x}$ to be the unique element of $R(d)$ which is an ancestor of x, and we set $Z_{Y} \mathrel {:=} \{ z_{y} \mid y \in Y \}$ and $Z_{U} \mathrel {:=} \{ z_{u} \mid u \in U \}$ . Similarly as before we have that $Z_{Y} \cap Z_{U} = \emptyset $ and $|Z_{Y}| < q$ . We now make a case distinction.

If $Z_{U}$ is finite, then we may without loss of generality assume that it is a singleton, say, $Z_{U} = \{ z \}$ where z is an ancestor of every $u \in U$ (Figure 2). In the same way as in the proof of item 1, we may show that $f(d)$ has a successor $z'$ which is a q-companion of z. It then follows by Lemma 3.12(2) that $\mathbb {T}'$ contains an infinite collection $U'$ of nodes that are all descendants of $z'$ and q-companions of the nodes in U. From this it is easily verified that any $u' \in U'$ and any $u \in U$ satisfy $\mathbb {T},\overline {u}\cdot u \approx ^{\downarrow }_{q} \mathbb {T}^{\prime },\overline {u}^{\prime }\cdot u^{\prime }$ , and this certainly suffices to prove the statement of item 2.

Fig. 2 Lemma 3.14(2) case a.

If, on the other hand, $Z_{U}$ is infinite (Figure 3), our first observation is that all nodes in $Z_{U}$ belong to the same q-companion class: this easily follows from the assumption (discussed above) that all nodes $u \in U$ are q-companions of one another. Define $\chi \in \mathtt {GML}^{\infty }_{q-h(z),q}$ as the characteristic formula of the -cell of some/any $z \in Z_{U}$ , then we have $\mathbb {T},d \Vdash \lozenge ^{\infty }\chi $ . From this we may use the q-companionship of d and $f(d)$ to derive that $\mathbb {T}',f(d) \Vdash \lozenge ^{\infty }\chi $ , so that $f(d)$ has an infinite set $W'$ of successors that all satisfy the formula $\chi $ . From this it readily follows that each $w' \in W'$ is a q-companion of each $z \in Z_{U}$ . Then by Lemma 3.12 each $w' \in W'$ has a descendant $u^{\prime }_{w^{\prime }}$ which is a q-companion of the nodes in U. Finally, it is a routine exercise to show that the set $U^{\prime } \mathrel {:=} \{ u^{\prime }_{w^{\prime }} \mid w^{\prime } \in W^{\prime }\}$ meets all the conditions as specified in the lemma.

Fig. 3 Lemma 3.14(2) case b.

Lemma 3.14 gives us all the necessary ingredients to prove Theorem 3.9.

Proof of Theorem 3.9

Fix some natural number $q \geq 1$ , let $\mathbb {T}$ and $\mathbb {T}'$ be tree models of height q, with roots r and $r'$ , respectively, and assume that . Obviously then, r and $r'$ are q-companions, and from this we readily see that, seen as two $1$ -tuples, they are q-similar: $\mathbb {T},r\approx ^{\downarrow }_{q}\mathbb {T}',r'$ . It then follows from successive applications of Lemma 3.12 that in the Ehrenfeucht–Fraïssé game $\texttt {EF}_{q}^{\infty }$ between $\mathbb {T},r$ and $\mathbb {T}',r'$ , Duplicator has a strategy ensuring that every configuration, that is reached in a match of this game, will consist of two q-similar tuples. Playing such a strategy, Duplicator thus guarantees that the final q-configuration $(\overline {u},\overline {u}')$ will be such that $\mathbb {T},\overline {u} \approx ^{\downarrow }_{q} \mathbb {T}',\overline {u}'$ . That is, there is a isomorphism f from $\mathbb {T}_{\overline {u}}$ to $\mathbb {T}^{\prime }_{\overline {u}^{\prime }}$ such that $f(u_{i}) = u^{\prime }_{i}$ , for all i; in particular then, f is a local isomorphism from $\overline {u}$ to $\overline {u}^{\prime }$ . In other words, any such strategy is a winning strategy for her.

This finishes the proof of Theorem 3.9.

3.5 Proof of bisimulation invariance theorem

We can now collect all the results we obtained in the previous subsections and prove the bisimulation invariance theorem.

Proof of Theorem 2.25

We focus on the forward direction of the proof. The backwards direction can be easily proved by induction on the complexity of the formula $\psi $ .

Fix some bisimulation invariant formula $\mathtt {FO}^{\infty }$ formula $\varphi (x)$ , and let q be its quantifier depth. Define $n \mathrel {:=} 3^{q}$ , then it follows from Proposition 3.7 that $\varphi $ is n-local. We first prove that $\varphi $ is -invariant (cf. (2)).

For that purpose, let $\mathbb {S},s$ and $\mathbb {S}',s'$ be two pointed Kripke models such that . We will prove that

(6) $$ \begin{align} \mathbb{S} \models \varphi[s] \text{ if and only if } \mathbb{S}' \models \varphi[s']. \end{align} $$

For a proof of (6), let $\mathbb {U}_{\infty }(\mathbb {S},s)$ be the unravelling of $(\mathbb {S},s)$ . That is, $\mathbb {U}_{\infty }(\mathbb {S},s)$ is a tree model whose states are the finite paths of $\mathbb {S}$ that start with s, and whose accessibility relation and valuation are defined in the obvious way. We refer to [5] for the details, and leave it for the reader to verify that , an observation that we will refer to below as (bisimulation invariance).

We let $\mathbb {U}_{n}(\mathbb {S},s)$ be the structure that is based on the n-neighbourhood of s in $\mathbb {U}_{\infty }(\mathbb {S},s)$ —this structure is sometimes referred to as the n-unravelling of $(\mathbb {S},s)$ , since its states correspond to the paths in $\mathbb {S}$ of length at most n that start at s. It follows by locality that $\mathbb {U}_{\infty }(\mathbb {S},s) \models \varphi [s]$ iff $\mathbb {U}_{n}(\mathbb {S},s) \models \varphi [s]$ , and of course a similar observation applies to the unravellings of $(\mathbb {S}',s')$ .

Furthermore, it is not hard to see that implies . From this we may derive by Theorem 3.9 that $\mathbb {U}_{n}(\mathbb {S},s),s \mathrel {\cong ^{\infty }_{n}} \mathbb {U}_{n}(\mathbb {S}',s'),s'$ , and so by Proposition 2.29 we find that $\mathbb {U}_{n}(\mathbb {S},s) \models \varphi [s]$ iff $\mathbb {U}_{n}(\mathbb {S}',s') \models \varphi [s']$ (*).

Now consider the following chain of equivalences:

$$ \begin{align*} \mathbb{S} \models \varphi[s] \text{ iff } & \mathbb{U}_{\infty}(\mathbb{S},s) \models \varphi[s] & \text{(bisimulation invariance)} \\ \text{ iff } & \mathbb{U}_{n}(\mathbb{S},s) \models \varphi[s] & \text{(locality, Theorem 2.25)} \\ \text{ iff } & \mathbb{U}_{n}(\mathbb{S}',s') \models \varphi[s'] & \text{((*) above)} \\ \text{ iff } & \mathbb{U}_{\infty}(\mathbb{S}',s') \models \varphi[s'] & \text{(locality, Theorem 2.25)} \\ \text{ iff } & \mathbb{S}' \models \varphi[s']. & \text{(bisimulation invariance)} \end{align*} $$

This finishes the proof of (6).

But if $\varphi $ is -invariant, then the class of pointed models satisfying $\varphi $ is -saturated (i.e., a union of -cells). It is then immediate from Proposition 3.5 that $\varphi $ is equivalent to some formula in $\mathtt {GML}^{\infty }_{n,n}$ .

4 Completeness and small model property

In this section we will prove two results for our logic: the Small Model Property (Theorem 2.20) and a completeness result (Theorem 4.2). In our proofs we will use coalgebras for a set functor $\mathsf {B}^{\bullet }$ which is closely related to the infinitary bag functor $\mathsf {B}^{\infty }$ .

For an overview of the section: in the first subsection we define and discuss the axiomatisation $\mathbf {G^{\infty }}$ , and we formulate our completeness result. In Section 4.2 we introduce the set functor $\mathsf {B}^{\bullet }$ and its coalgebras. Here we also formulate the main theorem of the section, Theorem 4.5, which states that any $\mathtt {GML}^{\infty }$ -formula $\varphi $ is derivable iff it is valid in, respectively, the classes of all Kripke frames, all $\mathsf {B}^{\infty }$ -coalgebras, all $\mathsf {B}^{\infty }$ -coalgebras of bounded size, and all $\mathsf {B}^{\bullet }$ -coalgebras. In the subsequent subsections we then prove the two nontrivial implications of this theorem: in Section 4.3 we prove $\mathbf {G^{\infty }}$ to be complete for the class of $\mathsf {B}^{\bullet }$ -coalgebras, and in Section 4.4 we establish a filtration lemma which shows that any formula that is satisfiable in a $\mathsf {B}^{\bullet }$ -coalgebra is also satisfiable in a $\mathsf {B}^{\infty }$ -coalgebra of bounded size.

4.1 The axiomatisation $\mathbf {G^{\infty }}$

In this subsection we will introduce an axiomatisation for the set of $\mathtt {GML}^{\infty }$ -validities, that is, the formulas that are valid in every Kripke frame.

Since the axiomatisation problem for graded modal logic has been addressed already [7, 11], we can take this as our starting point. The standard axiomatisation $\mathbf {G}$ for graded modal logic consists of the following axioms:

1. 1. all classical propositional tautologies,

2. 2. $\Box ^{k}\varphi \leftrightarrow \neg \lozenge ^{k}\neg \varphi $ ,

3. 3. $\Box ^{1}(\varphi \to \psi )\to (\lozenge ^{k}\varphi \to \lozenge ^{k}\psi )$ , for every $k\in \mathbb {N}$ ,

4. 4. $\lozenge ^{k+1}\varphi \to \lozenge ^{k}\varphi $ , for every $k\in \mathbb {N}$ ,

5. 5. $\neg \lozenge ^{1}(\varphi \land \psi ) \land \lozenge ^{=k_{1}}\varphi \land \lozenge ^{=k_{2}}\psi \to \lozenge ^{=(k_{1}+k_{2})}(\varphi \vee \psi )$ , for every $k_{1},k_{2}\in \mathbb {N}$ .

In addition, $\mathbf {G}$ has the following derivation rules:

• • modus ponens: from $\varphi $ and $\varphi \to \psi $ derive $\psi $ ;

• • $\Box $ -necessitation: from $\varphi $ derive $\Box \varphi $ .

Most of these axioms are fairly obvious. The Dual axiom 2 syntactically captures the Boolean duality between the $\lozenge ,\Box $ modalities as it was semantically described in Definition 2.2. Axiom 3 expresses the monotonicity of the graded modalities, while axiom 4 concerns the relative strength of the counting modalities, basically stating that “at least $k+1$ ” implies “at least k.” Finally, axiom 5 states that we may add the numbers of two disjoint groups of successors.

The logic $\mathbf {G}$ is defined as the smallest set of $\mathtt {GML}$ -formulas that contains the previous axioms and is closed under the inference rules described above. As mentioned, for this axiomatisation soundness and completeness has been proved [9, 12], so that $\mathbf {G}$ consists exactly of the set of $\mathtt {GML}$ -validities.

To capture the behaviour of the infinity modality $\lozenge ^{\infty }$ as well, we extend the logic $\mathbf {G}$ with the following axioms:

1. 6. $\Box ^{\infty }\varphi \leftrightarrow \neg \lozenge ^{\infty }\neg \varphi $ ,

2. 7. $\lozenge ^{\infty }\varphi \to \lozenge ^{k}\varphi $ , for every $k\in \mathbb {N}$ ,

3. 8. $\Box ^{\infty }(\varphi \to \psi )\to (\Box ^{\infty }\varphi \to \Box ^{\infty }\psi )$ .

Furthermore, we add the following derivation rule:

• • $\Box ^{\infty }$ -necessitation: from $\varphi $ derive $\Box ^{\infty }\varphi $ .

Definition 4.1. $\mathbf {G^{\infty }}$ is the smallest set of $\mathtt {GML}^{\infty }$ -formulas which contains the axioms 1–8 above, and is closed under the derivation rules of modus ponens and of necessitation, for both $\Box $ and $\Box ^{\infty }$ . A formula $\varphi $ is called a theorem of $\mathbf {G^{\infty }}$ or derivable in $\mathbf {G^{\infty }}$ if it belongs to $\mathbf {G^{\infty }}$ , notation: $\vdash _{\mathbf {G^{\infty }}} \varphi $ (or simply $\vdash \varphi $ , if no confusion is likely). The formula $\varphi $ is derivable from a set of formulas $\Gamma $ if there are finitely many formulas $\psi _{1},\ldots ,\psi _{n}$ in $\Gamma $ such that the formula $(\psi _{1} \land \cdots \land \psi _{n}) \to \varphi $ is derivable in $\mathbf {G^{\infty }}$ . A set $\Gamma $ of $\mathtt {GML}^{\infty }$ -formulas is $\mathbf {G^{\infty }}$ -consistent if $\bot $ is not derivable from it.

Here are some intuitions on the new axioms and derivation rule. Axiom 6 extends the duality expressed in axiom 2 to account for the $\lozenge ^{\infty }$ case. Axiom 7 can be interpreted as an extension of axiom 4 to include the infinite case, expressing that the existence of infinitely many successors of a certain kind implies the existence of an unbounded finite number of these successors. To complete the axiomatisation we make sure that the infinity box is a normal modality. This is done by including the K-axiom 8 and the necessitation rule for $\Box ^{\infty }$ . As a consequence of this, the infinity diamond distributes over disjunctions:

$$\begin{align*}\vdash_{\mathbf{G^{\infty}}} \lozenge^{\infty} (p \lor q) \leftrightarrow (\lozenge^{\infty} p \lor \lozenge^{\infty} q). \end{align*}$$

We conclude this subsection by stating one of the main results of this paper, the soundness and completeness theorem for the $\mathtt {GML}^{\infty }$ -logic $\mathbf {G^{\infty }}$ :

Theorem 4.2 (Soundness and Completeness)

The logic $\mathbf {G^{\infty }}$ is sound and complete with respect to the class of all Kripke frames. That is, for an arbitrary $\mathtt {GML}^{\infty }$ -formula $\varphi $ we have

$$\begin{align*}\vdash_{\mathbf{G^{\infty}}} \text{ iff } \varphi \text{ is valid in every Kripke frame}. \end{align*}$$

Remark. Let $\mathbf {K^{\infty }}$ be the normal bimodal logic for $\mathtt {ML}^{\infty }$ that we obtain by adding the axioms 6 and 8, as well as the necessitation rule for $\Box ^{\infty }$ to the basic modal logic $\mathbf {K}$ . It was proved by Fattorosi-Barnaba and Balestrini [11], and (independently) by the first author [2], that $\mathbf {K^{\infty }}$ is a sound and complete axiomatisation for the set of all $\mathtt {ML}^{\infty }$ -formulas that are valid in every Kripke frame.

4.2 $\mathsf {B}^{\bullet }$ -coalgebras

In this section we introduce the auxiliary structures that play a major role in the proof of the completeness theorem and the small model property, viz., the $\mathsf {B}^{\bullet }$ -coalgebras. These structures are very similar in nature to the $\mathsf {B}^{\infty }$ -coalgebras introduced in Section 2, the difference being that the functor $\mathsf {B}^{\bullet }$ admits a weight $\omega $ in between the finite numbers and $\infty $ . This new weight $\omega $ allows us to make a subtle difference in the semantics of the infinity diamond, and thus enables us to take care of sets of the form

$$\begin{align*}\{\lozenge^{k} \varphi \mid k\in\mathbb{N}\}\cup\{\neg\lozenge^{\infty}\varphi\} \end{align*}$$

which may be consistent (for instance if $\varphi $ is a proposition letter) but are never satisfiable.

Definition 4.3. We define $\mathbb {N}^{\omega ,\infty } \mathrel {:=} \mathbb {N} \cup \{ \omega , \infty \}$ , and extend the ordering $<$ of $\mathbb {N}^{\infty }$ to this set by putting $n < \omega $ for all $n \in \mathbb {N}$ , as well as $\omega < \infty $ . We will also need to introduce some arithmetic in $\mathbb {N}^{\omega ,\infty }$ ; we first define a binary addition $\oplus $ using the following table:

$$\begin{align*}\begin{array}{l|ccc} \oplus & n & \omega & \infty \\ \hline m & m+n & \omega & \infty \\ \omega & \omega & \omega & \infty \\ \infty & \infty & \infty & \infty \end{array} \end{align*}$$

We now extend this binary addition to an infinitary operation as follows:

$$\begin{align*}\bigoplus_{i \in I} \kappa_{i} \mathrel{:=} \left\{ \begin{array}{ll} \infty, & \text{if } \kappa_{i} = \infty \text{ for some } i \in I, \\ \sum_{i\in I'} \kappa_{i}, & \text{if } I' \mathrel{:=} \{ i \in I \mid \kappa_{i} \neq 0 \} \text{ is finite}, \\ \omega, & \text{otherwise}. \end{array} \right. \end{align*}$$

Note that the difference between the two operations $\sum _{i\in I}$ and $\bigoplus _{i\in I}$ lies in the particular case where we add infinitely many non-zero natural numbers $k_{i}$ : this will give $\sum _{i\in I}k_{i} = \infty $ but $\bigoplus _{i\in I} k_{i} = \omega $ .

The set functor $\mathsf {B}^{\bullet }$ is defined very similarly to $\mathsf {B}^{\infty }$ , and the same holds for $\mathsf {B}^{\bullet }$ -coalgebras and $\mathsf {B}^{\bullet }$ -models.

Definition 4.4. For a set S, we define $\mathsf {B}^{\bullet } S \mathrel {:=} S \to \mathbb {N}^{\omega ,\infty }$ , and for a function $f: S \to S'$ , we define the map $(\mathsf {B}^{\bullet } f): \mathsf {B}^{\bullet }(S) \to \mathsf {B}^{\bullet }(S')$ by putting

$$\begin{align*}(\mathsf{B}^{\bullet} f)(\mu): s' \mapsto \bigoplus_{s \in f^{-1}(s')} \mu(s). \end{align*}$$

A $\mathsf {B}^{\bullet }$ -coalgebra is a pair $(S,\sigma )$ such that $\sigma : S \to \mathsf {B}^{\bullet }(S)$ assigns a $\mathsf {B}^{\bullet }$ -weight function to each state $s \in S$ . A $\mathsf {B}^{\bullet }$ -model is a triple $\mathbb {S} = (S,\sigma ,V)$ such that $(S,\sigma )$ is a $\mathsf {B}^{\bullet }$ -coalgebra and V is a valuation on S.

In these models we interpret formulas in the language $\mathtt {GML}^{\infty }$ using the obvious definitions for the atomic formulas and Boolean connectives, while the modalities are interpreted using the following clause:

$$\begin{align*}\mathbb{S},s \Vdash^{\bullet} \lozenge^{\kappa} \varphi \text{ iff } \kappa \leq \bigoplus_{t \Vdash^{\bullet} \varphi} \sigma_{s}(t). \end{align*}$$

Therefore, this means that in a $\mathsf {B}^{\bullet }$ -model we have

$$\begin{align*}\mathbb{S},s \Vdash^{\bullet} \lozenge^{\infty} \varphi \text{ iff } \mathbb{S},t \Vdash^{\bullet} \varphi \text{ for some } t \text{ with } \sigma_{s}(t) = \infty. \end{align*}$$

Recall that in a $\mathsf {B}^{\infty }$ -model, on the other hand, we can also have $\mathbb {S},s \Vdash \lozenge ^{\infty }\varphi $ if there are infinitely many t such that $\mathbb {S},t \Vdash \varphi $ but $0 < \sigma _{s}(t) < \infty $ for all t.

The $\mathsf {B}^{\bullet }$ -coalgebras may not be very interesting in their own right. However, they do provide the pivotal semantics which link the notions of Kripke validity, derivability and validity in small $\mathsf {B}^{\infty }$ -coalgebras, as is witnessed by the following theorem.

Theorem 4.5. The following are equivalent, for every formula $\varphi \in \mathtt {GML}^{\infty }$ :

1. 1. $\varphi $ is valid (i.e., valid in every Kripke frame);

2. 2. $\varphi $ is valid in every $\mathsf {B}^{\infty }$ -coalgebra;

3. 3. $\varphi $ is valid in every $\mathsf {B}^{\infty }$ -coalgebra of size at most $2^{|\varphi |}$ and weight at most $\text {r}(\varphi )$ ;

4. 4. $\varphi $ is valid in every $\mathsf {B}^{\bullet }$ -coalgebra;

5. 5. $\varphi $ is a theorem of $\mathbf {G^{\infty }}$ .

Proof. The implication from (1) to (2) follows by Corollary 2.18, and the implication from (2) to (3) is trivial. The implications from (3) to (4) and from (4) to (5) will be proved in the Sections 4.4 and 4.3, respectively. Finally, the implication from (5) to (1) states that our axiomatisation is sound. The verification of this statement is a routine exercise which we leave to the reader.

4.3 Completeness for $\mathsf {B}^{\bullet }$ -coalgebras

In this subsection we prove one implication of Theorem 4.5, which corresponds to the completeness of our axiom system $\mathbf {G^{\infty }}$ for the class of $\mathsf {B}^{\bullet }$ -coalgebras.

Theorem 4.6 (Completeness for $\mathsf {B}^{\bullet }$ -coalgebras)

The following holds, for every formula $\varphi \in \mathtt {GML}^{\infty }$ :

(7) $$ \begin{align} \mbox{ if } \varphi \text{ is valid in every } \mathsf{B}^{\bullet}\text{-coalgebra,} \mbox{ then } \varphi \text{ is a theorem of } \mathbf{G^{\infty}}. \end{align} $$

We will prove Theorem 4.6 using a canonical model construction, somewhat similar to the proof of De Caro in [9] for graded modal logic.

For the rest of the section fix a countably infinite set P of proposition letters. Define a set $\Gamma \subseteq \mathtt {GML}^{\infty }(P)$ to be maximally consistent if $\Gamma $ is consistent and it does not have a proper consistent extension $\Delta \subseteq \mathtt {GML}^{\infty }(P)$ . We shall abbreviate “maximal consistent set” as MCS. We let C denote the set of all maximally consistent sets of formulas, and we define the canonical valuation $V^{c}$ in the usual way, that is, $V^{c}(p) \mathrel {:=} \{ \Phi \in C \mid p \in \Phi \}$ .

For the definition of the $\mathsf {B}^{\bullet }$ -coalgebra map $\gamma : C \to \mathsf {B}^{\bullet }(C)$ , consider two MCSs $\Phi $ and $\Psi $ . We say that $\Psi $ has finite multiplicity for $\Phi $ if there is some $n \in \mathbb {N}$ and some formula $\psi \in \Psi $ such that $\lozenge ^{=n}\psi \in \Phi $ . Clearly, in the situation where such an n exists, there is a unique minimal one; we will refer to this number as the multiplicity of $\Psi $ for $\Phi $ and denote it as $\mu _{\Phi }(\Psi )$ . We now define the map $\gamma : C \to (C \to \mathbb {N}^{\omega ,\infty })$ as follows:

$$\begin{align*}\gamma_{\Phi}(\Psi) \mathrel{:=} \left\{ \begin{array}{ll} \infty, & \text{if } \lozenge^{\infty}\psi \in \Phi, \text{ for all } \psi \in \Psi, \\ \mu_{\Phi}(\Psi), & \text{if } \Psi \text{ has finite multiplicity for } \Phi, \\ \omega, & \text{otherwise}. \end{array} \right. \end{align*}$$

It is not difficult to see that for any two MCSs $\Phi $ and $\Psi $ :

$$\begin{align*}\gamma_{\Phi}(\Psi)=\omega\text{ if and only if } \{\lozenge^{k}\psi\mid k\in\mathbb{N}\}\cup\{\neg\lozenge^{\infty}\psi\}\subseteq\Phi\text{ for some }\psi\in\Psi. \end{align*}$$

We shall refer to the triple $\mathbb {C} \mathrel {:=} (C,\gamma ,V^{c})$ as the canonical $\mathsf {B}^{\bullet }$ -model.

The crux of the proof of Theorem 4.6 is the following Truth Lemma.

Proposition 4.7. Let $\Phi $ be a $\mathbf {G^{\infty }}$ -MCS. Then we have

$$\begin{align*}\mathbb{C},\Phi \Vdash^{\bullet} \varphi \text{ iff } \varphi \in \Phi, \end{align*}$$

for all formulas $\varphi \in \mathtt {GML}^{\infty }$ .

In order to prove the Truth Lemma we need some auxiliary facts that can easily be verified.

Fact 1. Let $\Phi $ be a $\mathbf {G^{\infty }}$ -MCS, and let $\varphi $ be some $\mathtt {GML}^{\infty }$ -formula. Then:

1. 1) if $\lozenge ^{1}\varphi \in \Phi $ then there is some $\mathbf {G^{\infty }}$ -MCS $\Psi $ with $\varphi \in \Psi $ and $\gamma _{\Phi }(\Psi )\geq 1$ ;

2. 2) if $\lozenge ^{\infty }\varphi \in \Phi $ then there is some $\mathbf {G^{\infty }}$ -MCS $\Psi $ with $\varphi \in \Psi $ and $\gamma _{\Phi }(\Psi )=\infty $ .

Fact 2. Let $\Psi _{0},\ldots ,\Psi _{k}$ be a collection of distinct maximal $\mathbf {G^{\infty }}$ -consistent sets. For every $i\leq k$ we can find a $\mathtt {GML}^{\infty }$ formula $\alpha _{i}$ such that $\alpha _{i}\in \Psi _{j}$ if and only if $i=j$ .

The key proposition in our proof of the Truth Lemma is the following observation.

Proposition 4.8. Let $\Phi $ be a maximal $\mathbf {G^{\infty }}$ -consistent set of formulas and let $\kappa $ be any value in $\mathbb {N}^{\infty }$ . Then we have

$$\begin{align*}\lozenge^{\kappa}\varphi\in\Phi \text{ iff } \bigoplus_{\Psi\ni\varphi} \gamma_{\Phi}(\Psi)\geq \kappa \end{align*}$$

for all formulas $\varphi \in \mathtt {GML}^{\infty }$ .

Proof. This proof is an adaptation of Theorem 1 in De Caro’s completeness proof [7]. Hence, rather than giving a detailed proof we confine ourselves to a sketch. In the sequel we will abbreviate $m_{\Psi } \mathrel {:=} \gamma _{\Phi }(\Psi )$ . The proof is based on a case distinction. Case $\kappa =0 $ : This case is trivial since the formula $\lozenge ^{0}\varphi $ , being equivalent to $\top $ , belongs to every MCS, while on the other hand every $\bigoplus $ -type sum in $\mathbb {N}^{\omega ,\infty }$ is at least as big as $0$ .

Case $\kappa \in \{ 1, \infty \}$ : The forward direction follows directly from Fact 1. For the opposite direction, suppose that $\bigoplus _{\Psi \ni \varphi } m_{\Psi } \geq \kappa $ , then by definition of $\bigoplus $ there must be at least one MCS $\Psi $ such that $m_{\Psi }\geq \kappa $ . It now follows from the definition of $\gamma _{\Phi }$ that $\lozenge ^{\kappa }\varphi \in \Phi $ .

Case $\kappa = n\in \mathbb {N}\backslash \{0,1\}$ : Let I be the collection of MCSs $\Psi $ such that $\varphi \in \Psi $ and $m_{\Psi } \geq 1$ . If $m_{\Psi } \geq n$ for some $\Psi \in I$ , then the result is obvious. Thus we examine the case where $m_{\Psi } < n$ for every $\Psi \in I$ . We make a further distinction as to the size of I.

• Subcase: I is finite. For each $\Psi \in I$ we let $\alpha _{\Psi }$ be some formula as in Fact 2 and $\beta _{\Psi }$ the defining formula that makes $\Psi $ have multiplicity $m_{\Psi }$ for $\Phi $ (as described above). Then, defining $\psi _{\Psi }$ to be $\alpha _{\Psi }\wedge \beta _{\Psi }\wedge \varphi $ , we may easily prove that:

  1. 1. $\lozenge ^{= m_{\Psi }}\psi _{\Psi }\in \Phi $ , for all $\Psi $ in I,

  2. 2. $\vdash \neg (\psi _{\Psi } \land \psi _{\Theta })$ , for any distinct $\Psi $ and $\Theta $ in I,

  3. 3. $\vdash \bigvee _{\Psi \in I}\psi _{\Psi }\rightarrow \varphi $ .

  Combining the observations 1 and 2 with Axiom 5, one may verify that $\lozenge ^{=m}\bigvee _{\Psi \in I}\psi _{\Psi }\in \Phi $ , where $m \mathrel {:=} \sum _{\Psi \in I} m_{\Psi }$ . Furthermore, if we let $\theta $ be the formula $\bigwedge _{\Psi \in I} \neg (\alpha _{\Psi }\vee \beta _{\Psi })$ , the following facts easily follow:

  1. 4. $\vdash \varphi \leftrightarrow \big ((\varphi \wedge \theta ) \vee \bigvee _{\Psi \in I}\psi _{\Psi }\big )$ ,

  2. 5. $\neg \lozenge (\varphi \wedge \theta )\in \Phi $ .

  If we now combine observation 5 and the fact that $\lozenge ^{=m}\bigvee _{\Psi \in I}\psi _{\Psi }\in \Phi $ with Axiom 5, we obtain that $\lozenge ^{=m} \big ((\varphi \wedge \theta ) \vee \bigvee _{\Psi \in I}\psi _{\Psi }\big )\in \Phi $ . Based on this and observation 4 one may conclude that $\lozenge ^{=m}\varphi \in \Phi $ . From this it easily follows that

  $$\begin{align*}\lozenge^{n}\varphi \in \Phi \text{ iff } n \leq m. \end{align*}$$
  Furthermore, since I is a finite set, and $m_{\Psi }$ is a natural number for every $\Psi \in I$ , we find that
  $$\begin{align*}\bigoplus_{\Psi\ni\varphi} \gamma_{\Phi}(\Psi) = \bigoplus_{\Psi\in I} \gamma_{\Phi}(\Psi) = \sum_{\Psi\in I}\gamma_{\Phi}(\Psi) = \sum_{\Psi\in I} m_{\Psi} = m. \end{align*}$$
  From the above two observations the statement of the proposition readily follows.

• Subcase: I is infinite. In this case we find $\bigoplus _{\Psi \ni \varphi } \gamma _{\Phi }(\Psi ) = \omega $ , so that we need to prove that $\lozenge ^{n}\varphi \in \Phi $ . For this purpose we take some set $J \subseteq I$ of size n, and define $m' \mathrel {:=} \sum _{\Psi \in J} m_{\Psi }$ . Then clearly we have $n \leq m'$ . Using similar reasoning as before, we may find a family $\{ \psi _{\Psi } \mid \Psi \in J \}$ of formulas satisfying the items 1–3 above, with J replacing I. Defining $\varphi ' \mathrel {:=} \bigvee _{\Psi \in J}\psi _{\Psi }$ , we may show, again as above, that $\lozenge ^{=m'}\varphi '\in \Phi $ . But then since $\vdash \varphi ' \to \varphi $ and $n \leq m'$ we find $\lozenge ^{n}\varphi \in \Phi $ as required.

This finishes the proof of Proposition 4.8.

As we will see now, the Truth Lemma and, based on that, the Completeness Theorem itself are immediate consequences of Proposition 4.8.

Proof of Proposition 4.7

We prove the Truth Lemma by a routine induction on the formula $\varphi $ , taking care of the cases for the modalities using Proposition 4.8.

Proof of Theorem 4.6

We prove the completeness theorem by showing that every consistent formula is satisfiable in a $\mathsf {B}^{\bullet }$ -model. Let $\varphi $ be a $\mathtt {GML}^{\infty }$ -formula that is consistent with respect to the proof system $\mathbf {G^{\infty }}$ . By a routine Lindenbaum-type construction we may obtain an MCS $\Gamma $ containing the formula $\varphi $ , so that by the Truth Lemma $\varphi $ is actually true at $\Gamma $ in the canonical $\mathsf {B}^{\bullet }$ -model. In particular then, $\varphi $ is satisfiable in a $\mathsf {B}^{\bullet }$ -model.

4.4 Filtrations: from $\mathsf {B}^{\bullet }$ -coalgebras to small $\mathsf {B}^{\infty }$ -coalgebras

In this subsection we provide the proof of the remaining implication of Theorem 4.5, viz., the statement that validity in bounded-size $\mathsf {B}^{\infty }$ -coalgebras implies validity in all $\mathsf {B}^{\bullet }$ -coalgebras. In fact, we will prove the contrapositive statement.

Theorem 4.9. Let $\varphi $ be some formula in $\mathtt {GML}^{\infty }$ . If $\varphi $ is satisfiable in some $\mathsf {B}^{\bullet }$ -model, then $\varphi $ is satisfiable in a $\mathsf {B}^{\infty }$ -model of size at most $2^{|\varphi |}$ and rank $\text {r}(\varphi )$ .

Our proof will be based on a filtration argument, that is, we will show that $\mathsf {B}^{\bullet }$ -models can be quotiented to finite $\mathsf {B}^{\infty }$ -models. Our definition of the filtrated model involves choice functions, an idea originating from the literature on coalgebra. We need the notion of a closed set of formulas.

Definition 4.10. A set $\Sigma $ of $\mathtt {GML}^{\infty }$ -formulas is closed if it is closed under taking subformulas and single negations (that is, if $\varphi \in \Sigma $ is not of the form $\neg \psi $ then $\neg \varphi $ also belongs to $\Sigma $ ).

As usual the filtration of a model will be based on the quotient of the domain of the model under a natural equivalence relation induced by a closed set of formulas.

Definition 4.11. Let $\mathbb {S} = (S,\sigma ,V)$ be a $\mathsf {B}^{\bullet }$ -model. We define the equivalence relation $\equiv _{\Sigma }$ on S by putting $s \equiv _{\Sigma } s'$ iff we have that $\mathbb {S},s \Vdash ^{\bullet } \varphi \Leftrightarrow \mathbb {S},s' \Vdash ^{\bullet } \varphi $ , for all $\varphi \in \Sigma $ .

In the remainder of this section we fix a finite closed set $\Sigma $ , so that we may write $\equiv $ instead of $\equiv _{\Sigma }$ without confusion. Recall that a choice function on a collection P of nonempty subsets of a set S is any map $c: P \to S$ such that $c(X) \in X$ , for all $X \in P$ . We are now ready for the definition of a filtration.

Definition 4.12. Let $\mathbb {S} = (S,\sigma ,V)$ be a $\mathsf {B}^{\bullet }$ -model. The equivalence class of $s \in S$ under the relation $\equiv $ will be denoted as $\overline {s}$ , and we write $\overline {S} \mathrel {:=} \{ \overline {s} \mid s \in S\}$ . The valuation $\overline {V}$ is given by putting $\overline {V}(p) \mathrel {:=} \{ \overline {s} \mid s' \in V(p), \text { for some } s' \equiv s \}$ .

Given a choice function $c: \overline {S} \to S$ , we define the map $\sigma ^{c}: \overline {S} \to \mathsf {B}^{\infty }(\overline {S})$ as follows:

$$\begin{align*}\sigma^{c}_{\overline{s}}(\overline{t}) \mathrel{:=} \left\{\hspace{-3pt}\begin{array}{ll} \infty, & \text{if } \sigma_{c(\overline{s})}(t') = \infty, \text{ for some } t' \in\overline{t}, \\ \min\big\{ \text{r}(\Sigma), \bigoplus_{t'\equiv t}\sigma_{c(\overline{s})}(t') \big\}, & \text{otherwise}. \end{array} \right. \end{align*}$$

Any $\mathsf {B}^{\infty }$ -model of the form $\overline {\mathbb {S}} = (\overline {S},\sigma ^{c},\overline {V})$ is called a $\Sigma $ -filtration of $\mathbb {S}$ .

In words, the weight function $\sigma ^{c}$ of the filtrated model is defined as follows. In principle, for the weight of a state $\overline {t}$ according to a state $\overline {s}$ we would like to take the $\bigoplus $ -sum of the weights of all the members of $\overline {t}$ , according to the chosen element $c(\overline {s}) \in \overline {s}$ . This candidate for the weight $\sigma ^{c}_{\overline {s}}(\overline {t})$ is capped off, however, by the finitary modal rank of $\Sigma $ .

The key result about this construction is that the natural quotient map (i.e., the one sending any state to its $\equiv $ -cell) preserves the truth of all formulas in $\Sigma $ .

Proposition 4.13 (Filtration Lemma)

Let $\Sigma $ be a finite, closed set of $\mathtt {GML}^{\infty }$ -formulas, let $\mathbb {S}$ be a $\mathsf {B}^{\bullet }$ -model, and let $\overline {\mathbb {S}}$ be a $\Sigma $ -filtration of $\mathbb {S}$ . Then we have

$$\begin{align*}\mathbb{S},s \Vdash^{\bullet} \varphi \text{ iff } \overline{\mathbb{S}},\overline{s} \Vdash \varphi, \end{align*}$$

for all $\varphi \in \Sigma $ and all $s \in S$ .

Proof. This proposition is proved by induction on the complexity of $\varphi $ . Let c be the choice function inducing the filtration.

• Case $\varphi = \lozenge ^{k}\psi $ , with $k \in \mathbb {N}$ . First assume that $\mathbb {S},s \Vdash ^{\bullet } \lozenge ^{k}\psi $ . Since $\lozenge ^{k}\psi \in \Sigma $ and $s \equiv c(\overline {s})$ , we find that $\mathbb {S},c(\overline {s}) \Vdash ^{\bullet } \lozenge ^{k}\psi $ . Now, we can distinguish two different cases. First suppose that $\sigma ^{c}_{\overline {s}}(\overline {t}) \geq \text {r}(\Sigma )$ , for some $\overline {t} \Vdash \psi $ . Since $k \leq \text {r}(\Sigma )$ we are automatically done, as we immediately obtain that $\mathbb {S},\overline {s} \Vdash \lozenge ^{k}\psi $ .We may thus focus on the case where $\sigma ^{c}_{\overline {s}}(\overline {t})$ is strictly smaller than $\text {r}(\Sigma )$ , for all $\overline {t}$ in $\overline {S}$ such that $\overline {\mathbb {S}},\overline {t} \Vdash \psi $ . This means in particular that $\sigma ^{c}_{\overline {s}}(\overline {t})$ is finite, and by the definition of $\sigma ^{c}$ , that

  $$\begin{align*}\sigma^{c}_{\overline{s}}(\overline{t}) = \bigoplus_{t' \equiv t} \sigma_{c(\overline{s})}(t') = \sum_{t' \equiv t} \sigma_{c(\overline{s})}(t'), \end{align*}$$
  for every such state $\overline {t}$ .

  Furthermore, it follows from the induction hypothesis and the definition of the relation $\equiv $ that $\mathbb {S},t' \Vdash ^{\bullet } \psi $ for all $t' \in \overline {t}$ such that $\overline {\mathbb {S}},\overline {t} \Vdash \psi $ . Thus we find that

  (8) $$ \begin{align} \sum_{\overline{t}\Vdash\psi} \sigma^{c}_{\overline{s}}(\overline{t}) = \sum_{\overline{t}\Vdash\psi} \sum_{t'\in\overline{t}}\sigma_{c(\overline{s})}(t') = \sum_{t' \Vdash^{\bullet} \psi} \sigma_{c(\overline{s})}(t') \geq k, \end{align} $$
  where the latter inequality holds simply because $\mathbb {S},c(\overline {s}) \Vdash ^{\bullet } \lozenge ^{k}\psi $ . But from (8) it is immediate that $\overline {\mathbb {S}},\overline {s} \Vdash \lozenge ^{k}\psi $ .

  For the opposite direction, assume that $\overline {\mathbb {S}}, \overline {s} \Vdash \lozenge ^{k}\psi $ , and suppose for a contradiction that $\mathbb {S},c(\overline {s}) \not \Vdash ^{\bullet } \lozenge ^{k}\psi $ , i.e., that

  $$\begin{align*}\sum_{u\Vdash^{\bullet}\psi} \sigma_{c(\overline{s})}(u) < k. \end{align*}$$

  Consider an arbitrary $\overline {t} \in \overline {S}$ such that $\overline {\mathbb {S}},\overline {t} \Vdash \psi $ . By the inductive hypothesis, any $t'$ in $\overline {t}$ satisfies $\mathbb {S},t' \Vdash ^{\bullet }\psi $ . From this it is immediate that

  $$\begin{align*}\sum_{t'\equiv t} \sigma_{c(\overline{s})}(t') \leq \sum_{u\Vdash^{\bullet}\psi}\sigma_{c(\overline{s})}(u)<k. \end{align*}$$
  Combining these two observations with the (obvious) fact that $k \leq \text {r}(\Sigma )$ we obtain that
  $$\begin{align*}\sum_{t'\equiv t} \sigma_{c(\overline{s})}(t') < \text{r}(\Sigma). \end{align*}$$
  Hence, by the definition of $\sigma ^{c}$ , we obtain that
  $$\begin{align*}\sigma^{c}_{\overline{s}}(\overline{t}) = \sum_{t'\equiv t} \sigma_{c(\overline{s})}(t'). \end{align*}$$
  Since this holds for every $\overline {t} \in \overline {S}$ such that $\overline {\mathbb {S}},\overline {t} \Vdash \psi $ , we may conclude that
  $$\begin{align*}\sum_{\overline{t}\Vdash\psi} \sigma^{c}_{\overline{s}}(\overline{t}) = \sum_{u\Vdash^{\bullet}\psi}\sigma_{c(\overline{s})}(u) < k, \end{align*}$$
  contradicting our assumption that $\overline {\mathbb {S}}, \overline {s} \Vdash \lozenge ^{k}\psi $ .

  We thus have $\mathbb {S},c(\overline {s}) \Vdash ^{\bullet } \lozenge ^{k}\psi $ , and from this and the fact that $s \equiv c(\overline {s})$ it follows that $\mathbb {S},s \Vdash ^{\bullet } \lozenge ^{k}\psi $ .

• Case $\varphi = \lozenge ^{\infty }\psi $ . First assume that $\mathbb {S},s \Vdash ^{\bullet } \lozenge ^{\infty }\psi $ , then by definition of $\equiv $ it follows that $\mathbb {S},c(\overline {s}) \Vdash ^{\bullet } \lozenge ^{\infty }\psi $ . By the semantics there must be a state $t \in \mathbb {S}$ such that $\mathbb {S},t \Vdash ^{\bullet } \psi $ and $\sigma _{c(\overline {s})}(t) = \infty $ . From the latter fact and by the definition of $\sigma ^{c}$ , it is immediate that $\sigma ^{c}_{\overline {s}}(\overline {t}) = \infty $ , while we may use the inductive hypothesis to find that $\overline {\mathbb {S}},\overline {t} \Vdash \psi $ . From this we can derive that $\overline {\mathbb {S}},\overline {s} \Vdash \lozenge ^{\infty }\psi $ .

  For the opposite direction, assume that $\overline {\mathbb {S}},\overline {s} \Vdash \lozenge ^{\infty }\psi $ . Since $\overline {S}$ is finite, this can only be the case if there is a state $\overline {t} \in \overline {S}$ such that $\sigma ^{c}_{\overline {s}}(\overline {t}) = \infty $ and $\overline {\mathbb {S}}, \overline {t} \Vdash \psi $ . Then the inductive hypothesis yields that $\mathbb {S}, t \Vdash ^{\bullet } \psi $ , and by the definition of $\sigma ^{c}$ we have that $\sigma _{c(\overline {s})}(t') = \infty $ , for some $t' \in S$ such that $t' \equiv t$ . It then follows from $t' \equiv t$ that $\mathbb {S}, t' \Vdash ^{\bullet } \psi $ , so that $\mathbb {S}, c(\overline {s}) \Vdash ^{\bullet } \lozenge ^{\infty } \psi $ by the semantics in $\mathsf {B}^{\bullet }$ -models; finally we conclude from $s \equiv c(\overline {s})$ that $\mathbb {S},s \Vdash ^{\bullet } \lozenge ^{\infty }\psi $ , as required.

This finishes the proof of the Filtration Lemma.

The proof of Theorem 4.9 is an immediate corollary of the Filtration Lemma.

Proof of Theorem 4.9

Let $\varphi \in \mathtt {GML}^{\infty }$ be satisfiable in some $\mathsf {B}^{\bullet }$ -model $\mathbb {S}$ , say, $\mathbb {S},s \Vdash ^{\bullet } \varphi $ . Define $\Sigma $ as the closure of $\varphi $ , that is, the smallest closed set containing $\varphi $ , and let c be an arbitrary choice function on the set of $\equiv _{\Sigma }$ -cells. It follows from the Filtration Lemma that $\varphi $ is satisfiable at the state $\overline {s}$ of the filtrated model $\overline {\mathbb {S}} = (\overline {S},\sigma ^{c},\overline {V})$ . Finally, it is straightforward to verify that $\overline {\mathbb {S}}$ is a $\mathsf {B}^{\infty }$ -model of the required size and weight.

Acknowledgment

The authors are grateful to the anonymous referees for various helpful suggestions to improve the presentation of the paper.