Ehrenfeucht–Fraïssé for FO.

We review the classical Ehrenfeucht–Fraïssé analysis of the expressive power of $\mathsf {FO}$ over relational structures. The underlying game, like the bisimulation game, is a two-player game, that serves to probe, in this case, levels of equivalence w.r.t. first-order logic for matched tuples of elements over these two structures. Positions in the game over relational structures ${\mathfrak {A}},{\mathfrak {A}}'$ are pairs $(\mathbf {a};\mathbf {a}')$ with marked tuples $\mathbf {a}$ of elements in ${\mathfrak {A}}$ and $\mathbf {a}'$ of elements in ${\mathfrak {A}}'$ of the same finite length; we may think of $\mathbf {a}$ and $\mathbf {a}'$ as tuples of elements that are pebbled with pairs of matching pebbles so as to match the components of $\mathbf {a}$ to the components of $\mathbf {a}'$ . In a single round, player I positions one pebble of the next pair of pebbles in either ${\mathfrak {A}}$ or ${\mathfrak {A}}'$ , and player II must position its match in the opposite structure. This takes the game from position $(\mathbf {a};\mathbf {a}')$ to some successor position $(\mathbf {a},a;\mathbf {a}',a')$ . Player II loses in position $(\mathbf {a};\mathbf {a}')$ if ${\mathfrak {A}}\!\restriction \! \mathbf {a}, \mathbf {a} \not \simeq {\mathfrak {A}}'\!\restriction \! \mathbf {a}', \mathbf {a}'$ , i.e. if the pebbled match does not define an isomorphism between the induced substructures over these elements. If no such position is reached by the end of the game, II wins. A winning strategy for II in the n-round game starting from position $(\mathbf {a};\mathbf {a}')$ over ${\mathfrak {A}}$ and ${\mathfrak {A}}'$ guarantees that ${\mathfrak {A}},\mathbf {a} \equiv _n {\mathfrak {A}}',\mathbf {a}'$ (n-elementary equivalence), which means that $\mathbf {a}$ in ${\mathfrak {A}}$ and $\mathbf {a}'$ in ${\mathfrak {A}}'$ are indistinguishable by $\mathsf {FO}$ -formulae of quantifier rank up to n. Denoting the equivalence relation defined in terms of a winning strategy for II in the n-round game by $\simeq _n$ :

(1) $$ \begin{align} {\mathfrak{A}},\mathbf{a} \simeq_n {\mathfrak{A}}',\mathbf{a}' \quad \Rightarrow \quad {\mathfrak{A}},\mathbf{a} \equiv_n {\mathfrak{A}}',\mathbf{a}'. \end{align} $$

For structures ${\mathfrak {A}}$ and ${\mathfrak {A}}'$ in a finite relational signature, the classical Ehrenfeucht–Fraïssé theorem states that the converse implication also holds, so that (1) becomes an equivalence, which characterises levels of elementary equivalence in terms of the associated back-and-forth game.

The precise correspondence in the Ehrenfeucht–Fraïssé theorem witnesses how the positioning of a next pebble pair in a round of the game for $\mathsf {FO}$ probes the behaviour of the currently matched tuples w.r.t. a single further $\forall /\exists $ -quantification over elements – corresponding to an increase of $1$ in terms of quantifier rank. The corresponding game for $\mathsf {MSO}$ will additionally allow I to probe equivalence w.r.t. $\forall /\exists $ -quantification over subsets, and game positions correspondingly record a match between elements and subsets. In our specific context we shall exploit parallels beween the $\mathsf {FO}$ -game involving both sorts of our relational models and the $\mathsf {MSO}$ -game over the first sort.

Ehrenfeucht–Fraïssé for MSO.

We consider two ordinary structures ${\mathfrak {A}},{\mathfrak {A}}'$ in the same relational signature, with (single-sorted) universes $A,A'$ . To capture the expressiveness of $\mathsf {MSO}$ over these, game positions now consist of pairings $(\mathbf {P},\mathbf {a};\mathbf {P}',\mathbf {a}')$ where $\mathbf {a}$ and $\mathbf {a}'$ are tuples of elements of the same finite length from A and $A'$ , and $\mathbf {P}$ and $\mathbf {P}'$ are tuples of subsets of A and $A'$ of the same finite length. The condition that II must maintain in order not to lose in position $(\mathbf {P},\mathbf {a};\mathbf {P}',\mathbf {a}')$ over ${\mathfrak {A}},{\mathfrak {A}}'$ now is

$$\begin{align*}({\mathfrak{A}},\mathbf{P})\!\restriction\!\mathbf{a},\mathbf{a} \simeq ({\mathfrak{A}}',\mathbf{P}')\!\restriction\!\mathbf{a}',\mathbf{a}'. \end{align*}$$

This means that the elements matched by the pebble pairs mark out isomorphic induced substructures in the expansions of ${\mathfrak {A}}$ by the unary predicates $\mathbf {P}$ and of ${\mathfrak {A}}'$ by $\mathbf {P}'$ . These expansions may be seen as colourings produced in second-order moves in which $\mathbf {P}$ and $\mathbf {P}'$ were matched, which are probed (just as in the first-order $\mathsf {FO}$ game) by the match in pebbled elements $\mathbf {a}$ and $\mathbf {a}'$ produced in first-order moves. In each round, I determines whether to play it in first- or second-order mode, and correspondingly makes a choice of either an element or a subset on the ${\mathfrak {A}}$ -side or on the ${\mathfrak {A}}'$ -side; II must respond likewise on the opposite side. Depending on the mode of this round, it may overall lead from $(\mathbf {P},\mathbf {a};\mathbf {P}',\mathbf {a}')$ to $(\mathbf {P},\mathbf {a},a;\mathbf {P}',\mathbf {a}',a')$ (with a new pair of pebbled elements $(a,a')$ for first-order round) or to $(\mathbf {P},P,\mathbf {a};\mathbf {P}',P',\mathbf {a}')$ (with a new pair of subsets or a new colour for elements, $(P,P')$ for a second-order round).

A winning strategy for II for n rounds of this game starting from position $(\mathbf {P},\mathbf {a};\mathbf {P}',\mathbf {a}')$ over ${\mathfrak {A}}$ and ${\mathfrak {A}}'$ now guarantees that ${\mathfrak {A}},\mathbf {P},\mathbf {a} \equiv _n^{\mathsf {MSO}} {\mathfrak {A}}',\mathbf {P}',\mathbf {a}'$ , i.e. indistinguishability by $\mathsf {MSO}$ -formulae of quantifier rank up to n.Footnote ⁸ Denoting the equivalence relation defined in terms of a winning strategy for II in this n-round game for $\mathsf {MSO}$ by $\simeq _n^{\mathsf {MSO}}$ , the general result analogous to (1) above is

(2) $$ \begin{align} {\mathfrak{M}},\mathbf{m} \simeq_n^{\mathsf{MSO}} {\mathfrak{M}}',\mathbf{m}' \quad \Rightarrow \quad {\mathfrak{M}},\mathbf{m} \equiv_n^{\mathsf{MSO}} {\mathfrak{M}}',\mathbf{m}', \end{align} $$

and, again, the converse implication is also true over finite relational signatures.

First-order interpretations in an exploded view.

Consider an epistemic model ${\mathbb {M}} = (W,(\Sigma _a)_{a\in \mathcal {A}},V)$ with locally full two-sorted relational encoding ${\mathfrak {M}} := {\mathfrak {M}}^{\mathsf {lf}}({\mathbb {M}}) = (W,S, (E_a)_{a \in \mathcal {A}},(P_i)_{i\in I})$ , where

$$\begin{align*}S = \bigcup \bigl\{ \wp([w]_a) \colon w\in W, a\in\mathcal{A} \bigr\}, \end{align*}$$

where $[w]_a = \sigma _a(w) = R_a[w]$ . We also consider the natural restrictions-cum-reducts ${\mathbb {M}}\!\restriction \! [w]_a$ and ${\mathfrak {M}}\!\restriction \![w]_a$ for any combination of $w \in W$ and $a \in \mathcal {A}$ :

$$\begin{align*}{\mathbb {M}}\!\restriction\![w]_a := \bigl( [w]_a, \Sigma_a \!\restriction\![w]_a, V \!\restriction\![w]_a \bigr) \end{align*}$$

will be referred to as an a-local structure or just local structure and is treated as inquisitive model for the single agent a with constant $\Sigma _a$ . The relational encoding

$$\begin{align*}{\mathfrak{M}}\!\restriction\![w]_a := \bigl( [w]_a, \wp([w]_a), E_a \!\restriction\![w]_a, (P_i \!\restriction\![w]_a) \bigr) \end{align*}$$

of this local structure arises as the induced substructure of the reduct of ${\mathfrak {M}}$ that eliminates all other agents; this restriction is two-sorted and full, as the domain for the second sort, the restriction of S to $\wp ([w]_a)$ comprises all of $\wp ([w]_a)$ since ${\mathfrak {M}} = {\mathfrak {M}}^{\mathsf {lf}}({\mathbb {M}})$ is locally full. So each ${\mathfrak {M}}\!\restriction \![w]_a$ is a full relational encoding of the single-agent, single-equivalence-class inquisitive epistemic model ${\mathbb {M}}\!\restriction \! [w]_a$ . In order to analyse the expressive power of first-order logic over ${\mathfrak {M}}$ , we look at an “exploded view” $\mathsf {I}({\mathfrak {M}})$ of ${\mathfrak {M}}$ , which represents ${\mathfrak {M}}$ as the conglomerate of these restrictions ${\mathfrak {M}}\!\restriction \! [w]_a$ , with their interconnections charted in a core structure representing the underlying Kripke frame. The concrete format of such an exploded view would admit quite some variations. What matters for us is first-order interpretability of ${\mathfrak {M}}$ itself within $\mathsf {I}({\mathfrak {M}})$ : as indicated in Figure 2, we want to apply these representations to suitably prepared models $\hat {{\mathfrak {M}}}$ so as to argue for $\equiv _q$ at the level of $\hat {{\mathfrak {M}}}/ \hat {{\mathfrak {M}}}'$ on the basis of $\equiv _{q+d}$ at the level of the $\mathsf {I}(\hat {{\mathfrak {M}}})/\mathsf {I}(\hat {{\mathfrak {M}}}')$ for some fixed constant d. We first discuss suitable representations $\mathsf {I}({\mathfrak {M}})$ for arbitrary locally full relational epistemic models of the form ${\mathfrak {M}} = {\mathfrak {M}}^{\mathsf {lf}}({\mathbb {M}})$ but note that they will only be used for specifically prepared bisimilar partner structures as in Figure 2; it is also important to note that the $\mathsf {I}(\cdot )$ -images are not themselves relational encodings of inquisitive models. Figure 3 illustrates the structural ingredients in the format that we choose for this exploded view $\mathsf {I}({\mathfrak {M}})$ of ${\mathfrak {M}}$ . The two-sorted structure $\mathsf {I}({\mathfrak {M}})$ , from which ${\mathfrak {M}}$ itself can be retrieved by first-order means, involves (see below for details):

• – a core part within the first sort, which represents the underlying multi-agent $S5$ Kripke frame on the set of worlds W, with relation symbols $R_a$ for accessibility w.r.t. agent $a \in \mathcal {A}$ as in the induced Kripke frame;

• – a halo of attached disjoint external copies of each one of the two-sorted local structures ${\mathfrak {M}}\!\restriction \! [w]_a$ , one for each equivalence class of worlds w.r.t. to agents $a \in \mathcal {A}$ ; ${\mathfrak {M}}\!\restriction \! [w]_a$ carries the natural restrictions of the relations in ${\mathfrak {M}}$ but with inquisitive assignment just for agent a (see above);

  

  Figure 3 Structural layout of the exploded view $\mathsf {I}({\mathfrak {M}})$ of ${\mathfrak {M}}$ ; selectively displayed are the representations of intersecting local structures ${\mathfrak {M}}\!\restriction \! [w]_a$ , ${\mathfrak {M}}\!\restriction \! [w]_{a'}$ w.r.t. agents a and $a'$ , with one element each from their (full powerset) second sorts. Here $\alpha = [w]_a$ and $\alpha '= [w]_{a'}$ contribute two overlapping local structures, whose disjoint (tagged) representations each contribute the full power set of their first sort to disjoint (tagged) representations in the second sort; displayed as particular elements of the second sort are $s_\alpha $ for some $s \subset \alpha $ (as part of the representation of the a-local structure ${\mathfrak {M}}\!\restriction \![w]_a$ ) and the full set $\alpha ' \subset \alpha '$ (as part of the representation of the $a'$ -local structure ${\mathfrak {M}}\!\restriction \![w]_{a'}$ ).

• – with additional unary marker predicates $P_a$ for the a-local components and a binary relation $R_I$ for the identification between worlds in the core part and their instances in local component structures in the halo.

The first part of the disjoint union underlying $\mathsf {I}({\mathfrak {M}})$ forms the core (fully in the first sort), the remaining parts (all truly two-sorted) form the halo, with the interpretation of $R_I$ as the only link between the otherwise disjoint pieces:

$$\begin{align*}\mathsf{I}({\mathfrak{M}}) := \displaystyle \bigl( (W, (R_a)_{a \in \mathcal{A}}) \;\oplus \!\! \!\!\!\!\! \!\!\bigoplus_{a\in\mathcal{A},[w]_a \in W/R_a} \!\! \!\! \!\! \!\! \!\! {\mathfrak{M}}\!\restriction\![w]_a\; , (P_a)_{a\in\mathcal{A}}\, ,\, R_I \bigr). \end{align*}$$

We think of the disjoint union of the restrictions ${\mathfrak {M}}\!\restriction \![w]_a$ as realised over a-tagged versions of $[w]_a$ with elements $u_a$ for $u \in [w]_a$ for the first sort and $[w]_a$ -tagged elements $s_\alpha $ for $s \in \wp ([w]_a)$ in the second sort for $\alpha = [w]_a \in W/R_a$ . More formally these can be realised over universes $[w_a] \times \{ a \}$ and $\wp ([w]_a) \times \{ \alpha \}$ , but we use notation like $u_a$ instead of $(u,a)$ for better readability.Footnote ¹⁰ The interpretations for $E_a$ and the valuation V are just restricted over $[w]_a$ as indicated above. The core structure $(W,(R_a))$ in the first-sort of $\mathsf {I}({\mathfrak {M}})$ is the underlying Kripke frame on the set of worlds W with the modal accessibility relations (representations of the $\sigma _a$ as equivalence relations)

$$\begin{align*}R_a \;:=\; \{ (w,w') \in W^2 \colon w' \in \sigma_a(w) \}, \end{align*}$$

that make up this $S5$ frame; its domain W also serves to supply the markers to relate any $v \in W$ with its multiple copies in the local structures ${\mathfrak {M}}\!\restriction \! [w]_a$ through $R_I$ ; the extra unary relation symbols $P_a$ carve out the subset of a-tagged copies $w_a$ of worlds $w \in W$ ,

$$\begin{align*}\begin{array}{r@{}l} P_a &:= \{ u_a \colon u \in [w]_a \}, \\ R_I &:= \{ (w,w_a) \colon w \in W, a \in \mathcal{A} \}. \end{array} \end{align*}$$

One may read the index I for “incidence” or “identification” of worlds with their multiple incarnations; the subset W of the first sort of $\mathsf {I}({\mathfrak {M}})$ precisely serves as a set of world labels that relate copies of the corresponding w:

i.e. iff there is some $v \in W$ for which , which implies that $v=u=u'$ and that $[w]_a = [v]_a$ and $[w']_{a'} = [v]_{a'}$ for this $v = u = u'$ .

The world-pointed model ${\mathfrak {M}},w$ is naturally represented by the world-pointed exploded view, $\mathsf {I}({\mathfrak {M}}),w$ with distinguished world w in the core of $\mathsf {I}({\mathfrak {M}})$ . In the state-pointed ${\mathfrak {M}},s$ with nonempty state $s \in S$ , s need not be directly represented as an element of the second sort in any local structure, as in general we only require $\wp (s) \subset S$ (cf. Definition 2.12). But we may reduce this scenario to the world-pointed case by the introduction of an extra (dummy) agent as follows.Footnote ¹¹ For non-trivial $s \subset W$ where $\wp (s) \subset S$ let $\mathcal {A}_s := \mathcal {A} \,\dot {\cup }\, \{ s \}$ and consider the expansion of ${\mathfrak {M}}$ to ${\mathfrak {M}}_s := ({\mathfrak {M}}, E_s)$ based on the relational encoding of the trivial inquisitive assignment

$$\begin{align*}\Sigma_s \colon w \mapsto \left\{ \begin{array}{ll} \wp(s) & \text{ for } w \in s \\ \wp(\{ w\}) & \text{ for } w \not\in s, \end{array}\right. \end{align*}$$

whose induced $\sigma _s$ and $R_s$ partition W into singleton equivalence classes $[w]_s = \{ w \}$ for $w \notin s$ and the single, potentially non-trivial equivalence class $[w]_s = s$ , for any $w \in s$ . So the exploded view of ${\mathfrak {M}}_s$ has, for non-trivial s, an extra part for the s-local structure ${\mathfrak {M}}_s\!\restriction \! [w]_s$ which provides a representation of s, both as a set of worlds in its first sort, and as the $\subseteq $ -maximal element in its second sort. So s is $\mathsf {FO}$ -definably available in $\mathsf {I}({\mathfrak {M}}_s)$ in the s-local structure ${\mathfrak {M}}_s\!\restriction \! [w]_s$ , marked out either by the parameter $s = s_{\alpha _s}$ , $\alpha _s := [w]_s$ , of the second sort, or by any choice of a parameter $w_s$ , $w \in s$ , in the second sort.

We note that passage to ${\mathfrak {M}}_s$ is safe also w.r.t. bisimulation equivalences for state-pointed models in the sense that ${\mathfrak {M}},s \sim {\mathfrak {M}}',s'$ implies that , i.e. that for any $w \in s$ there is some $w' \in s'$ such that and vice versa; and similarly for every level of $\sim ^n$ . So we give the following definition.

The exploded views $\mathsf {I}({\mathfrak {M}},w)$ and $\mathsf {I}({\mathfrak {M}},s)$ are such that the evaluation of any $\mathsf {FO}$ -formula in a single free first- or second-sort variable over ${\mathfrak {M}},w$ or ${\mathfrak {M}},s$ translates into the evaluation of a corresponding first-order formula over $\mathsf {I}({\mathfrak {M}},w)$ and $\mathsf {I}({\mathfrak {M}},s)$ , respectively. Indeed, there is a uniform syntactic translation to this effect, a phenomenon that generally applies for first-order interpretations. In our case, we rely on the uniform $\mathsf {FO}$ interpretability of ${\mathfrak {M}}$ within its exploded view $\mathsf {I}({\mathfrak {M}})$ , together with the $\mathsf {FO}$ -definable access to the relevant assignment w or s: $w \in W$ is an element of the first sort of $\mathsf {I}({\mathfrak {M}},w)$ ; and $s \not =\emptyset $ is represented by the maximal element in the second sort of its local component structure.Footnote ¹² In fact, for locally full inquisitive relational models ${\mathfrak {M}}$ , the two-sorted structures ${\mathfrak {M}}$ and their exploded views $\mathsf {I}({\mathfrak {M}})$ are uniformly first-order interpretable within one another (bi-interpretable). The following summarises the use we want to make of interpretability in the context of the upgrading scheme as indicated in Figure 2.

Claim 3.3. Due to $\mathsf {FO}$ -interpretability of any locally full relational model ${\mathfrak {M}},w$ in $\mathsf {I}({\mathfrak {M}},w)$ , or of ${\mathfrak {M}},s$ in $\mathsf {I}({\mathfrak {M}},s)$ , there is a constant d such that $(q+d)$ -elementary equivalence between the exploded views of two such models implies q-elementary equivalence between the original relational models. For instance in the world-pointed case, any first-order of quantifier rank up to q in a world-variable has a uniform translation of quantifier rank at most $q+d$ such that iff . It follows that for any pair of world-pointed locally full inquisitive relational models ${\mathfrak {M}},w$ and ${\mathfrak {M}}',w'$

$$\begin{align*}\mathsf{I}({\mathfrak{M}},w) \equiv_{q+d} \mathsf{I}({\mathfrak{M}}',w') \quad \Rightarrow \quad {\mathfrak{M}},w \equiv_q {\mathfrak{M}}',w'; \end{align*}$$

and similarly for formulae in a state variable and state-pointed locally full relational epistemic models.

Proofsketch.

All the relevant structural information about ${\mathfrak {M}}$ is easily imported to the sub-universe W of the first sort in $\mathsf {I}({\mathfrak {M}})$ . This sub-universe itself is $\mathsf {FO}$ definable in $\mathsf {I}({\mathfrak {M}})$ as the projection of $R_I$ to its first component; the valuation V at $w \in W$ is imported from any one of the elements in $R_I[w]$ ; the relational encoding $E_a[w]$ of the inquisitive assignment $\Sigma _a(w)$ is similarly imported through backward translation of $E_a(w_a)$ from any one of the $w_a \in R_I[w] \cap P_a$ via set-wise passage to $R_I$ -predecessors:

$$\begin{align*}v \in s \in \Sigma_a(w) \quad\text{ iff }\quad v \in (R_I \circ \in)^{-1}(E_a[w_a]), \end{align*}$$

for $w_a \in R_I[w] \cap P_a$ . Compare Figure 3 to see how especially this relationship between elements and subsets of the core part can be traced in the representation of the a-local structure ${\mathfrak {M}}\!\restriction \![w]_a$ in the halo of $\mathsf {I}({\mathfrak {M}})$ . All these relations are therefore uniformly first-order definable within the exploded views $\mathsf {I}({\mathfrak {M}})$ , and the maximal quantifier rank in corresponding $\mathsf {FO}$ -formulae can serve as the value d for the transfer claim. For the non-trivially state-pointed case, similarly, the distinguished state s (and its entire powerset) is accessible in the component structure ${\mathfrak {M}}_s\!\restriction \! [w]_s$ for any $w \in s$ in $\mathsf {I}({\mathfrak {M}},s)$ .

For the upgrading argument according to Figure 2 we shall therefore eventually establish $\equiv _q$ -equivalence of, for instance world-pointed inquisitive relational models,

(3) $$ \begin{align} {\mathfrak{M}},w \equiv_q {\mathfrak{M}}',w', \end{align} $$

where q is the quantifier rank of the given bisimulation invariant , based on the assumption that ${\mathfrak {M}},w \sim ^\ell {\mathfrak {M}}',w'$ for suitable $\ell = \ell (q)$ . The above preparation allows us to reduce this to showing

(4) $$ \begin{align} \mathsf{I}({\mathfrak{M}},w)= \mathsf{I}({\mathfrak{M}}),w \equiv_{q+d} \mathsf{I}({\mathfrak{M}}'),w' = \mathsf{I}({\mathfrak{M}}',w'). \end{align} $$

In fact we also only need to establish (3) or (4) for ${\mathfrak {M}}$ and ${\mathfrak {M}}'$ from some subclass of the class of all epistemic relational models that represents the corresponding class (of all or just all finite such models) up to bisimulation equivalence. E.g. in the finite model theory version for the world-pointed case, it suffices to show that, for any two finite epistemic models ${\mathbb {M}},w$ and ${\mathbb {M}}',w'$ that are $\ell $ -bisimilar, there are bisimilar companions $\hat {{\mathbb {M}}},\hat {w} \sim {\mathbb {M}},w$ and $\hat {{\mathbb {M}}}',\hat {w}' \sim {\mathbb {M}}',w'$ such that

(5) $$ \begin{align} \mathsf{I}(\hat{{\mathbb {M}}},\hat{w}) = \mathsf{I}({\mathfrak{M}}^{\mathsf{lf}}(\hat{{\mathbb {M}}})),\hat{w} \equiv_{q+d} \mathsf{I}({\mathfrak{M}}^{\mathsf{lf}}(\hat{{\mathbb {M}}}')),\hat{w}' = \mathsf{I}(\hat{{\mathbb {M}}}',\hat{w}'). \end{align} $$

The remaining work towards this upgrading argument, therefore, focuses on the construction of suitable bisimilar companions. Suitability here means that (5) can be established by Ehrenfeucht–Fraïssé arguments for $\mathsf {FO}$ and – for auxiliary arguments concerning the restrictions ${\mathfrak {M}} \!\restriction \! [w]_a$ as main building blocks of the $\mathsf {I}({\mathfrak {M}})$ – for $\mathsf {MSO}$ .

The Ehrenfeucht–Fraïssé argument for suitably prepared epistemic models is facilitated by the observation that $\sim $ -invariance implies invariance under disjoint unions for epistemic models, and that the passage to exploded views is compatible with such disjoint unions. The following definition of disjoint unions is the natural one for inquisitive models.

Clearly, ${\mathbb {M}},w \sim {\mathbb {M}} \,\oplus \, \mathbb {L},w$ and ${\mathbb {M}},s \sim {\mathbb {M}} \,\oplus \, \mathbb {L},s$ for any world- or state-pointed epistemic models ${\mathbb {M}},w$ or ${\mathbb {M}},s$ and plain $\mathbb {L}$ . But while the disjoint union of epistemic models or of their relational encodings cannot be strictly disjoint, because of the special rôle of the empty information state $\emptyset $ , this little problem is overcome in their exploded views.

Observation 3.5. Passage to the exploded view of epistemic models is compatible with disjoint unions in the sense that

$$\begin{align*}\mathsf{I}({\mathbb {M}}_1 \oplus {\mathbb {M}}_2)= \mathsf{I}({\mathbb {M}}_1) \oplus \mathsf{I}({\mathbb {M}}_2), \end{align*}$$

and similarly with a distinguished world or state parameter from ${\mathbb {M}}_1$ say.

FO-equivalence and Gaifman locality.

We review some relevant technical background on Gaifman locality and its use towards establishing levels of first-order equivalence between relational structures, with a view to applying these techniques to show $\mathsf {I}(\hat {{\mathfrak {M}}}, \cdot \, ) \equiv _{q+d} \mathsf {I}(\hat {{\mathfrak {M}}}' , \cdot \, )$ in the situation of Figure 2, for suitably pre-processed models $\hat {{\mathfrak {M}}}, \cdot \, \,{\sim ^n}\, \hat {{\mathfrak {M}}}' , \cdot \, $ . The relational structures in question interpret just unary and binary relations. Correspondingly, Gaifman distance over their (two-sorted) universes is just ordinary graph distance w.r.t. the symmetrizations of the binary relations. This establishes a natural distance measure between elements, in our case across both sorts, worlds and information states.Footnote ¹³ For an element b of the relational structure ${\mathfrak {B}}$ and $\ell \in {\mathbb {N}}$ , the set of elements at distance up to $\ell $ from b is the $\ell $ -neighbourhood of b, denoted as

$$\begin{align*}N^\ell(b) = \{ b' \in B \colon d(b,b') \leq \ell \}. \end{align*}$$

A first-order formula in a single free variable x (of either sort) is $\ell $ -local if its semantics at $b \in {\mathfrak {B}}$ depends just on the induced substructure ${\mathfrak {B}}\!\restriction \! N^\ell (b)$ on the $\ell $ -neighbourhood $N^\ell (b)$ . In other words, is $\ell $ -local if, and only if, it is logically equivalent to its relativisation to the $\ell $ -neighbourhood of x, i.e., to the formula obtained by explicitly restricting all quantifiers in to the $\ell $ -neighbourhood of x (which is possible provided the underlying relational signature is finite). We refer to as the $\ell $ -localisation of . A finite set of elements of the relational structure ${\mathfrak {B}}$ is said to be $\ell $ -scattered if the $\ell $ -neighbourhoods of any two distinct members are disjoint. A basic local sentence is a sentence that asserts, for some formula and some $m \geq 1$ , the existence of an $\ell $ -scattered set of m elements that each satisfy the $\ell $ -localisation . Gaifman’s theorem [Reference Ebbinghaus and Flum11, Reference Gaifman and Stern12], in the case that we are interested in, asserts that any first-order formula in a single free variable x is logically equivalent to a boolean combination of $\ell $ -local formulae for some $\ell $ and some basic local sentences. We shall focus on the following levels of Gaifman equivalence.

The following is an immediate corollary of Gaifman’s classical theorem [Reference Ebbinghaus and Flum11, Reference Gaifman and Stern12], also in the case of our two-sorted structures and for distinguished elements of either sort.

We can use these results from classical first-order model theory in order to simplify the upgrading task: in effect we may replace the target levels $\equiv _q$ from Figure 1, or $\equiv _{q+d}$ in Figure 2 by $\equiv _r^{\scriptscriptstyle (\ell )}$ for exploded views, for appropriate $\ell $ and r. Compare Figure 4 for the following argument. On the basis of interpretability, $\equiv _q$ over $\hat {{\mathfrak {M}}}/\hat {{\mathfrak {M}}}'$ follows from $\equiv _{q+d}$ over $\mathsf {I}(\hat {{\mathfrak {M}}})/\mathsf {I}(\hat {{\mathfrak {M}}})'$ as illustrated in Figure 2, which in turn is implied by a suitable level of $\equiv _{r,m}^{\scriptscriptstyle (\ell )}$ over these. Up to bisimilarity, we may replace models $\hat {{\mathfrak {M}}}$ and $\hat {{\mathfrak {M}}}'$ by disjoint sums with a model

$$\begin{align*}{\mathfrak{X}} \;:=\; m \!\otimes\! \hat{{\mathfrak{M}}} \;\oplus\; m\!\otimes\!\hat{{\mathfrak{M}}}' \end{align*}$$

consisting of m many disjoint copies of each of $\hat {{\mathfrak {M}}}$ and $\hat {{\mathfrak {M}}}'$ (and similarly, using $\hat {{\mathfrak {M}}}_{\hat {s}}$ and in the non-trivially state-pointed case). The purpose of this modification is simply to trivialise the contribution of basic local sentences about scattered sets of size up to m towards $\equiv _{r,m}^{\scriptscriptstyle (\ell )}$ . By compatibility of the exploded view with disjoint sums, $\equiv _{r,m}^{\scriptscriptstyle (\ell )}$ and $\equiv _{r}^{\scriptscriptstyle (\ell )}$ coincide for the exploded views of these augmented structures, which further reduces the issue to the $\ell $ -local equivalence

(6) $$ \begin{align} \mathsf{I}(\hat{{\mathfrak{M}}},\cdot) \;\equiv_{r}^{\scriptscriptstyle (\ell)}\; \mathsf{I}(\hat{{\mathfrak{M}}}',\cdot), \end{align} $$

in both the world-pointed and the state-pointed case, as illustrated in Figure 4.

Figure 4 Upgrading for relational epistemic models, refined by Proposition 3.7.

The following summarises these considerations, which pave the way towards establishing the compactness property which we have seen to be equivalent to our main theorem. We can always assume that the underlying signature is the signature of the given first-order formula, hence finite.

Towards the criteria in Proposition 3.8, we exploit the representation of the relevant models in their exploded views. These allow us to view an inquisitive epistemic model ${\mathbb {M}}$ as a network of interconnected a-local structures ${\mathbb {M}}\!\restriction \! [w]_a$ that are linked through shared worlds. The individual mono-modal a-local structures, where two-sortedness reflects the higher-order nature of the inquisitive assignment, can be managed well in isolation. The interaction between these a-local structures, for different agents a in the global pattern of overlapping a-classes, on the other hand, is essentially reflected in the single-sorted $S5$ -Kripke structure ${\mathfrak {K}}({\mathbb {M}})$ that forms the core part of the exploded view $\mathsf {I}({\mathbb {M}})$ in the first sort. The desired upgrading argument for Proposition 3.8 calls for a strategy in the r-round first-order Ehrenfeucht–Fraïssé game over the $\ell $ -neighbourhoods of exploded views of two suitable pre-processed n-bisimilar models. Their nature as conglomerates of interconnected a-local structures allows us to divide concerns strategically as follows:

• – a-local concerns in suitably regularised local structures: the analysis of the $\mathsf {FO}$ -game over these two-sorted structures largely reduces to $\mathsf {MSO}$ -analysis over their first sorts; local pre-processing towards a normalisation of the inquisitive assignments will support that analysis.

• – the actual Ehrenfeucht–Fraïssé game in the $\ell $ -neighbourhoods, involving the connectivity pattern of links between a-local component structures; for that, global pre-processing towards local acyclicity in the connectivity patterns supports an analysis based on tree-like hypergraphs.

And indeed, the structure of our exploded views is precisely designed for this purpose. Due to suitable global pre-processing the core parts will be locally tree-like, and the general format of the exploded view as illustrated in Figure 3 retains this tree-likeness because local structures are connected only through the core; and the tentacles into the second sort, which each belong to just one local structure, will have been tamed by local pre-processing. Both the local and the global pre-processing need to respect bisimulation equivalence, i.e. rely on the construction of suitable bisimilar companions within the class $\mathcal {C}$ at hand.

3.3.1 Local pre-processing.

Since $\Sigma _a$ is constant across the single equivalence class $[w]_a$ , bisimulation – for this single-agent structure – equivalence collapses to its second level $\sim ^1$ . W.r.t. a fixed set of basic propositions each bisimulation type of such a structure is characterised by the collection of propositional types realised overall in its worlds and in the information states in its inquisitive assignment. In particular, multiplicities of these propositional types do not matter at all, neither overall nor in any individual information state: any positive number of realisations is as good as just a single one, so that multiplicities can be uniformly boosted to avoid distinguishing features at the level of $\mathsf {FO}$ .

The natural restrictions-cum-reducts ${\mathbb {M}}\!\restriction \![w]_a$ ignore the inquisitive structure induced by agents $b \not = a$ , and fall into one of these global $\sim ^1$ -equivalence classes. All the remaining complexity of multi-agent inquisitive $S5$ structures arises from the overlapping of a-classes for different $a \in \mathcal {A}$ , i.e. from the manner in which the various local structures ${\mathbb {M}}\!\restriction \! [u]_a$ or their relational encodings ${\mathfrak {M}}\!\restriction \! [w]_a$ overlap. In order to freeze the manner in which the local structures on individual a-classes are stitched together, we endow the ${\mathbb {M}}\!\restriction \! [w]_a$ with colourings of their worlds that prescribe their bisimulation types in the global structure ${\mathbb {M}}$ . For different purposes we use different granularities for this colouring. The finest one of interest is the colouring based on the full bisimulation-type in ${\mathbb {M}}$ , with colour set $C = W/{\sim }$ , the set of $\sim $ -equivalence classes of worlds in ${\mathbb {M}}$ . This is the colouring that needs to be respected in passage to fully bisimilar partner structures like $\hat {{\mathfrak {M}}},\hat {w} \sim {\mathfrak {M}},w$ in the vertical axes in Figure 4.

Coarser colourings are induced by the ${\sim ^m}$ -type, for a fixed finite level m, with colour set $C = W/{{\sim ^m}}$ . These may also be obtained via the natural projection that identifies all $\sim $ -types that fall into the same ${\sim ^m}$ -class. Successive coarsenings of this kind will inform the strategy analysis towards establishing levels of $\mathsf {FO}$ -indistinguishability like $\hat {{\mathfrak {M}}},\hat {w} \,\oplus {\mathfrak {X}} \; \equiv ^{\scriptscriptstyle (\ell )}_r \hat {{\mathfrak {M}}}',\hat {w}' \,\oplus {\mathfrak {X}}$ on the basis of ${\mathfrak {M}},w \sim ^n {\mathfrak {M}}',w'$ across the horizontal axes in Figure 4. Moreover, the relevant granularity m will be dependent on the distance from the distinguished worlds or states, just as control over levels of bisimilarity decreases with the depth of the exploration. But this granularity m will be uniformly bounded by the initial level n of n-bisimilarity in ${\mathfrak {M}},w \sim ^n {\mathfrak {M}}',w'$ or ${\mathfrak {M}},s \sim ^n {\mathfrak {M}}',s'$ .

Formally, a colouring of worlds by any colour set C can be encoded as a propositional assignment, for new atomic propositions $c \in C$ . Unlike propositional assignments in general, these propositions will be mutually exclusive, so as to partition the set of worlds. To reduce conceptual overhead, we encode colourings as functions

$$\begin{align*}\begin{array}[t]{rcl} \rho \colon W &\rightarrow& C \\ w &\mapsto& \rho(w) \end{array} \quad \text{ instead of } \quad \begin{array}[t]{rcl} V \colon C &\rightarrow& \wp(W) \\ c &\mapsto& V(c) = \{w \colon \rho(w) = c\}, \end{array} \end{align*}$$

and correspondingly write, e.g., $(W, (\Sigma _a)_{a \in \mathcal {A}}, \rho )$ for the inquisitive epistemic model with the colouring $\rho \colon W \rightarrow C$ that assigns to each world its $\sim $ -class:

$$\begin{align*}\begin{array}[t]{rcl} \rho \colon \; W &\longrightarrow& C := W/{\sim} \\ \rule{0em}{3ex} w & \longmapsto & [w]_{\sim} = \{ u \in W \colon {\mathbb {M}},u \sim {\mathbb {M}},w \}. \end{array} \end{align*}$$

The coarser colouring based on ${\sim ^m}$ -types is correspondingly formalised in the inquisitive epistemic model $({\mathbb {M}}, (\Sigma _a)_{a \in \mathcal {A}}, \rho _m)$ , with the colouring $\rho _m \colon W \rightarrow W/{{\sim ^m}}$ . Clearly the $\sim $ -colouring $\rho $ refines the ${\sim ^m}$ -colouring $\rho _m$ , and $\rho _n$ refines $\rho _m$ for $m<n$ . In particular, all levels refine $\rho _0$ , which determines each world’s original propositional type as induced by V in ${\mathbb {M}}$ .

Finiteness of the set of colours $W/{\sim }$ for the $\sim $ -colouring $\rho $ is guaranteed over each individual finite model ${\mathbb {M}}$ (or across pairs of finite models ${\mathbb {M}}$ and ${\mathbb {M}}'$ to be compared). But also over possibly infinite models the sets of colurs $W/{{\sim ^m}}$ for the ${\sim ^m}$ -colourings $\rho _m$ are uniformly finitely bounded across all models in a finite signature, for each finite level m.

Interestingly, a local $\sim $ - or ${\sim ^m}$ -structure can be modified considerably without changing its bisimulation type. We now want to achieve local structures

• – that realise every bisimulation type of worlds locally with high multiplicity; this leads to the notion of richness in Definition 3.11;

• – whose inquisitive assignment $\Sigma _a$ is normalised w.r.t. to the structure of the inquisitive state within $\wp ([w]_a)$ so as to suppress $\mathsf {FO}$ -definable distinctions that are not governed by any level of ${\sim ^m}$ ; this leads to the notion of regularity in Definition 3.13.

Regularity.

Unlike the merely quantitative flavour of richness, regularity imposes qualitative constraints on the structure of the family of information states in $\Sigma _a(w)$ . It requires a modification of the local inquisitive assignment and is not obtained in a covering. The idea is to normalise the downward closed family of information states in within the boolean algebra $\wp ([w]_a)$ of subsets of $[w]_a$ as much as possible. This normalisation needs to preserve the bisimulation type as encoded in the colouring $\rho $ . It must also be geared towards passage to the coarser picture induced by increasingly lower levels of m-bisimulation as encoded in the $\rho _m.^{14}$ . Passage to some suitable degree of regularity should be thought of as a local modification of the representation, rather than the epistemic content, of the inquisitive assignment. Indeed, bisimilarity is rather robust under changes in the actual composition of the inquisitive assignment in ${\mathbb {M}}$ . By the inquisitive epistemic nature of ${\mathbb {M}}$ , $\Sigma _a$ has constant value on $[w]_a$ and is a downward closed collection of subsets of $[w]_a$ such that . The only additional invariant imposed on up to $\sim $ stems from the associated colouring $\rho $ of worlds by their $\sim $ -types in $C = W/{\sim }$ ; for the inquisitive assignment this invariant concerns the colour combinations in

Note that is downward closed in $\wp (C)$ . Not only the collection of bisimulation types in the set of worlds $[w]_a$ , but also in the information states of the inquisitive assignment is fully determined by . Up to bisimulation, can be replaced by any inquisitive epistemic assignment with .

Similar remarks apply to finite levels ${\sim ^m}$ relative to the colouring $\rho _m$ with values in $W/{{\sim ^m}}$ , and for analogously defined . Clearly is fully determined by , so that for all admissible variations . But crucially, due to the coarsening, colour combinations $\rho _m(s_i)$ for infomation states may coincide even if $\rho (s_1) \not = \rho (s_2)$ . So the constraint that implies that some colour combinations in may have to appear in more than one $\subset $ -maximal element of and hence must be realised in at least that many $\subset $ -maximal elements of any admissible .Footnote ¹⁴

The assignment we choose will therefore be obtained from an upper bound $\kappa $ for the possibly unavoidable multiplicity of $\subset $ -maximal elements in . So $\kappa $ is to be adjusted accross the two models to be matched in the upgrading argument of Figure 4; it will always be finite in the context of finite inquisitive models for the finite model theoretic reading of our results, but could necessarily be infinite in the general case of infinite models that might even locally realise infinitely many distinct bisimulation types. Its granularity levels m will be dependent on the distance of the local structures from the distinguished worlds or states in the upgrading scenario of Figure 4. It will always be uniformly bounded by the initial level of n-bisimilarity $\sim ^n$ between the two pointed models under consideration. So there is a fixed finite bound on the number of ${\sim ^m}$ -colours that may occur. Such an upper bound can uniformly be chosen as a bound on the number of distinct $\sim $ -types realised by information states in the inquisitive assignments under consideration.

Towards normalised patterns for we think of decomposing $[w]_a$ into disjoint subsets $B_i \subset [w]_a$ , which we call blocks, such that every nonempty information state is contained in one of these, and such that each block $B_i$ is a disjoint union of $\subset $ -maximal information states in , one for each $\rho _m(s)$ , . In particular will be the union of its restrictions to the $\kappa $ many blocks, as illustrated in Figure 5.

Figure 5 Subdivison of $[w]_a= \sigma _a(w)$ in the local a-structure ${\mathbb {M}}\!\restriction \![w]_a$ for an inquisitive assignment that is $\kappa $ -regular at granularity m, where , $\kappa = \{ 1,2, \ldots \}$ and each one of the contributions $s(\alpha _j,i)$ in block $B_i$ is one $\subset $ -maximal element in , so that there are precisley $\kappa $ many such for each available ${\sim ^m}$ -type of nonempty information states in .

Definition 3.13. The inquisitive assignment in the local structure ${\mathbb {M}} \!\restriction \! [w]_a$ is $\kappa $ -regular at granularity m if $[w]_a = \dot {\bigcup }_{i < \kappa } B_i$ is a disjoint union of precisely $\kappa $ many blocks $B_i \subset [w]_a$ such that and

• – each of the restrictions realises every $\rho _m$ -colour combination $\alpha = \rho _m(s)$ for in precisely one $\subset $ -maximal element ;

• – these maximal elements are disjoint for distinct $\alpha $ and form a partition of $B_i$ .

It then follows that itself is generated by the combination of the downward closures of the family of disjoint maximal elements $s(\alpha ,i)$ across all $\alpha $ and i, which partition $[w]_a = \dot {\bigcup }_{\alpha ,i} s(\alpha ,i)$ .

Lemma 3.14. Let ${\mathbb {M}} = (W,(\Sigma _a),V)$ be an inquisitive epistemic model that is sufficiently rich in relation to given parameters $\kappa , K$ and the cardinality of $W/{\sim }$ ; let $m \colon W \rightarrow {\mathbb {N}}$ be any uniformly bounded function prescribing finite levels of granularity for the $\sim ^m$ -local structures ${\mathbb {M}}\!\restriction \! [w]_a$ at $w \in W$ . Then there is a globally bisimilar companion $\hat {{\mathbb {M}}} = (W,(\hat {\Sigma }_a),V)$ such that $\hat {{\mathbb {M}}},w \sim {\mathbb {M}},w$ for all $w \in W$ (so that the $\sim $ -colouring $\rho $ on W is unaffected) that is K-rich and in which every local structure $\hat {{\mathbb {M}}}\!\restriction \! [w]_a$ is $\kappa $ -regular at granularity $m(w)$ .

Proof. It suffices to restructure every individually into a that is $\kappa $ -regular w.r.t. $\rho _m$ for $m = m(w)$ and remains K-rich. Provided that $[w]_a$ has sufficiently many realisations of every ${\sim ^m}$ -type (as guaranteed by a sufficiently high level of richness in ${\mathbb {M}}$ ), $[w]_a$ can be split into $\kappa $ many disjoint blocks each of which is split into disjoint $\subset $ -maximal new information states, precisely one for every ${\sim ^m}$ -type $\alpha = \rho (s)$ for $s \in \Sigma _a(w)$ , realising every ${\sim ^m}$ -type of its worlds at least K times.

Observation 3.15. Every inquisitive epistemic model ${\mathbb {M}}$ admits, for $K \in {\mathbb {N}}$ , finite bisimilar coverings $\hat {{\mathbb {M}}}$ that are K-rich. As a consequence there are, for given $K,M \in {\mathbb {N}}$ , globally bisimilar inquisitive epistemic models $\hat {{\mathbb {M}}}$ sharing the same induced Kripke model ${\mathfrak {K}}(\hat {{\mathbb {M}}})$ with variations of just the inquisitive assignments, for every given M-bounded granularity assignment $m \colon \hat {W} \rightarrow {\mathbb {N}}$ , that make them both K-rich and $\kappa $ -regular w.r.t. that granularity assignment m. Such $\hat {{\mathbb {M}}}$ can be chosen to be finite for finite ${\mathbb {M}}$ and $\kappa $ .

3.3.2 Global pre-processing.

The desired pre-processing needs to unclutter and smooth out the local overlap patterns among local structures ${\mathfrak {M}}\!\restriction \![w]_a$ in $\mathsf {I}({\mathfrak {M}})$ in such a manner that the $\ell $ -bisimulation type determines the first-order behaviour of $\ell $ -neighbourhoods up to quantifier rank r (cf. Proposition 3.8). This requires a local unfolding of the connectivity in the underlying Kripke structures and uses ideas developed in [Reference Otto21] to eliminate incidental cycles and overlaps in finite bisimilar coverings — ideas which are applied to plain $S5$ Kripke structures in [Reference Dawar and Otto10]. Such overlaps, which up to bisimulation equivalence are incidental (i.e. cannot be prescribed by the bisimulation type), occur for instance whenever an a-class and an $a'$ -class for $a \not = a'$ share more than one world. These worlds would be linked by both an $R_a$ -edge and an $R_{a'}$ -edge. A bisimilar companion obtained from a classical tree unfolding (by the appropriate closure operations that turn it into an $S5$ frame) would separate these two edges. Similarly any cycle formed by a finite sequence of overlapping $a_i$ -classes that returns to its starting point would not be stable under appropriate bisimilar unfoldings.

For a given epistemic model ${\mathbb {M}}$ consider the induced Kripke structure ${\mathfrak {K}} = {\mathfrak {K}} ({\mathbb {M}}) = (W,(R_a)_{a \in \mathcal {A}},V)$ , which is a single-sorted, relational multi-modal $S5$ structure with equivalence relations $R_a$ derived from the inquisitive epistemic frame ${\mathbb {M}}$ , with equivalence classes $[w]_a= \sigma _a(w)$ . Generic constructions from [Reference Otto21], based on products with suitable Cayley groups, yield finite bisimilar coverings by $S5$ structures $\hat {{\mathfrak {K}}}$ that are N-acyclic in the following sense.

Figure 6 Example of particularly simple unfoldings in bisimilar coverings of $S5$ Kripke frames for agents with wavy, straight, dotted accessibility edges, respectively, and different shades for corresponding equivalence classes; top row: unfolding of a $2$ -cycle (overlap of two equivalence classes in two worlds) into a $4$ - or $6$ -cycle; below: unfolding of a $3$ -cycle into a $6$ -cycle (just non-trivial equivalence classes indicated and worlds in overlaps and links in induced cycles marked).

This acyclicity condition implies in particular that $a_i$ -classes and $a_j$ -classes for agents $a_i \not = a_j$ overlap in at most a single world: if $[w]_{a_1} \cap [w]_{a_2} \not = \{ w \}$ the two classes would form a non-trivial $2$ -cycle. For $N \geq 2 \ell $ it moreover implies that the overlap pattern between a-local structures is simply tree-like within Gaifman radius $\ell $ : any two distinct short sequences of such overlaps emanating from the same world cannot meet elsewhere (cf. Figure 6 for the basic intuition).

By [Reference Otto21], this form of N-acyclicity can be achieved, for any given N, in finite bisimilar coverings in which every a-class is bijectively related to an a-class in the original structure by the projection map of the covering, which induces the bisimulation. We briefly outline the extension of such bisimilar coverings of ${\mathfrak {K}}({\mathbb {M}})$ to bisimilar coverings of the inquisitive epistemic model ${\mathbb {M}}$ . Let be such an N-acyclic finite bisimilar covering, which in particular means that the graph of the covering projection is a bisimulation relation. Since a-classes in $\hat {{\mathfrak {K}}}$ are -related isomorphic copies of corresponding a-classes in ${\mathfrak {K}}$ , we may consistently endow them with an inquisitive $\Sigma _a$ -assignment as pulled back from ${\mathbb {M}}$ , to obtain a natural derived finite inquisitive bisimilar covering

in the sense of Definition 3.9. The inquisitive epistemic model $\hat {{\mathbb {M}}} = (\hat {W},(\hat {\Sigma }_a), \hat {V})$ is built on the basis of the covering $S5$ Kripke structure $\hat {{\mathfrak {K}}}$ so that ${\mathfrak {K}}(\hat {{\mathbb {M}}}) =\hat {{\mathfrak {K}}}$ . More specifically, for $\hat {w} \in \hat {W}$ consider its $\hat {R}_a$ -equivalence class $[\hat {w}]_a\subset \hat {W}$ , which is bijectively related by to the $R_a$ -equivalence class of in ${\mathfrak {K}}$ , $[w]_a \subset W$ . In restriction to $[\hat {w}]_a$ we put

where refers to the inverse of the local bijection between $[\hat {w}]_a $ and $[w]_a$ induced by . In other words, we make the following diagram commute and note that the relevant restriction of in the right-hand part of the diagram is bijective and part of a bisimulation at the level of the underlying $S5$ Kripke structures, which means in particular that it is compatible with the given propositional assignments:

We merely need to check that the resulting model $\hat {{\mathbb {M}}}$ is again an inquisitive epistemic model, and that induces an inquisitive bisimulation, not just a bisimulation at the level of the underlying single-sorted, multi-modal $S5$ -structures $\hat {{\mathfrak {K}}} = {\mathfrak {K}}(\hat {{\mathbb {M}}})$ and ${\mathfrak {K}} = {\mathfrak {K}}({\mathbb {M}})$ . That $\hat {{\mathbb {M}}}$ is an inquisitive epistemic model is straightforward from its construction: $\hat {\Sigma }_a$ -values are constant on the a-classes induced by $\hat {R}_a$ just as $\Sigma _a$ -values are constant across a-classes induced by $R_a$ ; and $\hat {w} \in \hat {\sigma }_a(\hat {w})$ follows from the fact that $w \in \sigma _a(w) = [w]_a$ .

A non-deterministic winning strategy in the unbounded inquisitive bisimulation on $\hat {{\mathbb {M}}},\hat {w}$ and is given by the following bisimulation relation, to be viewed as a set of winning positions for player II in the bisimulation game:

which is the natural lifting of to information states. It is easily verified that player II can stay in Z in response to any challenges by player I (Z satisfies the usual back&forth conditions). We summarise these findings as follows.

Lemma 3.17. Any inquisitive epistemic model ${\mathbb {M}} = (W, (\Sigma _a),V)$ admits, for every $N \in {\mathbb {N}}$ , a finite bisimilar covering of the form

by an inquisitive epistemic model $\hat {{\mathbb {M}}}= (\hat {W}, (\hat {\Sigma }_a),\hat {V})$ such that

• (i) $\hat {{\mathbb {M}}}$ is N-acyclic in the sense of Definition 3.16;

• (ii) the global bisimulation induced by is an isomorphism in restriction to each local structure $\hat {{\mathbb {M}}}\!\restriction \! [\hat {w}]_a$ of $\hat {{\mathbb {M}}}$ , which is isomorphically mapped by onto the local a-structure of ${\mathbb {M}}$ .

It is noteworthy that condition (ii) guarantees that degrees of regularity and richness are preserved in the covering, simply because they are properties of the local structures ${\mathbb {M}}\!\restriction \![w]_a$ , which up to isomorphism are the same in ${\mathbb {M}}$ and in $\hat {{\mathbb {M}}}$ . So, in combination with Observation 3.15, we obtain the following.

The non-trivially state-pointed case may deserve further comment. The desired $\hat {{\mathbb {M}}}$ in this case is based on the augmentation ${\mathbb {M}}_s$ with the extra agent s. The local pre-processing produces in particular a rich and $\kappa $ -regular s-local structure over a set of worlds $\hat {s}$ ; N-acyclicity for $N> 2\ell $ in the global pre-processing then serves to scatter the worlds in $\hat {s}$ within ${\mathfrak {K}}(\hat {{\mathbb {M}}})$ w.r.t. $\mathcal {A}$ in the sense that no two $(E_a)_{a \in \mathcal {A}}$ -paths of length up to $\ell $ from distinct worlds in $\hat {s}$ can meet: they are directly $E_s$ -linked and N-cyclic patterns are ruled out.

3.4.1 MSO-equivalence over local structures.

Recall Definition 3.10 of local structures ${\mathbb {M}}\!\restriction \![w]_a$ with colouring $\rho _m$ that marks out ${\sim ^m}$ -types in the surrounding ${\mathbb {M}}$ or ${\mathbb {M}}'$ . In the locally full relational encoding ${\mathfrak {M}} = {\mathfrak {M}}^{\mathsf {lf}}({\mathbb {M}})$ , we correspondingly consider ${\mathfrak {M}}\!\restriction \![w]_a,\rho _m$ as a mono-modal relational model. We apply Ehrenfeucht–Fraïssé techniques for $\mathsf {MSO}$ in order to obtain guarantees for levels of first-order equivalence $\equiv _k$ over these two-sorted local ${\sim ^m}$ -structures, assuming a suitable degree of richness and regularity w.r.t. $\rho _m$ . Richness matters since $\mathsf {FO}$ can assess cardinality distinctions between information states in the second sort, but just up to certain finite thresholds. These thresholds are inherited from $\mathsf {MSO}$ -definability over plain coloured sets over the first sort.

To compare the sizes of sets $P,P'$ up to some threshold $d \in {\mathbb {N}}$ , we introduce this cardinality equality with cut-off:

$$\begin{align*}|P| =_d |P'| \quad \colon\!\!\Leftrightarrow \quad |P|= |P'| \text{ or } |P|,|P'| \geq d. \end{align*}$$

For the analysis of a set W with any C-colouring $\rho \colon W \rightarrow C$ , we also use its representation as a plain relational structure $(W,(W_c)_{c \in C})$ with colour classes $W_c$ viewed as the interpretations of unary relations (monadic predicates). So we interchangeably think of representations of $W,\rho $ as a set with a colouring $\rho \colon W \rightarrow C$ or as a relational structure partitioned into these colour classes. In our applications, W will always be the first sort $[w]_a$ of some local ${\sim ^m}$ -structure, coloured by $\rho _m$ with the finite colour set for ${\sim ^m}$ -types of worlds.

With any subset $P \subset W$ we correspondingly associate the family

$$\begin{align*}(P_c)_{c \in C} \;\text{ where }\; P_c := \{ w \in P \colon \rho(w) = c \} = P \cap W_c. \end{align*}$$

For the comparison of $P \subset W$ with $P' \subset W'$ from two C-coloured sets $W,\rho $ and $W',\rho '$ we define the equivalence relation $\approx ^C_d$ according to

$$\begin{align*}P \approx^C_d P' \quad\text{ iff }\quad |P_c| =_d |P_c'| \text{ for all } c \in C; \end{align*}$$

and generalise this to k-tuples of subsets $\mathbf {P} \in (\wp (W))^k$ and $\mathbf {P}' \in (\wp (W'))^k$ by putting

$$\begin{align*}\mathbf{P} \approx^C_d \mathbf{P}' \quad\text{ iff }\quad \zeta(\mathbf{P}) \approx^C_d \zeta(\mathbf{P}') \text{ for all boolean terms }\zeta(\mathbf{X}). \end{align*}$$

TheFootnote ¹⁵ following is folklore, but we indicate the straightforward proof below.

Lemma 3.19. For C-coloured sets $W,W'$ with k-tuples $\mathbf {P} \in \wp (W)^k$ and $\mathbf {P}' \in \wp (W')^k$ of subsets, and for $d= 2^q$ :

$$\begin{align*}\mathbf{P} \approx^C_d \mathbf{P}' \quad \Rightarrow \quad (W,(W_c)_{c \in C},\mathbf{P}) \equiv^{\mathsf{MSO}}_q (W',(W_c')_{c \in C},\mathbf{P}'). \end{align*}$$

Note that assignments to first-order element variables x are implicit in the form of singleton sets for $\{ x\}$ (which induces but a small constant shift in quantifier rank levels).

We next transfer this $\mathsf {MSO}$ -equivalence between $\rho _m$ -coloured first sorts of suitable pre-processed local component structures to $\mathsf {FO}$ -equivalence between the two-sorted relational encodings of these local ${\sim ^m}$ -structures ${\mathfrak {M}}\!\restriction \![w]_a,\rho _m$ and ${\mathfrak {M}}'\!\restriction \![w]_a,\rho _m$ that locally realise the same ${\sim ^m}$ -types of information states and are $\kappa $ -regular at this granularity m for the same value of $\kappa $ .

Towards an interpretation of the $2$ -sorted full relational encodings of local ${\sim ^m}$ -structures like ${\mathfrak {M}}\!\restriction \![w]_a,\rho _m$ in terms of $\mathsf {MSO}$ -definability over $[w]_a$ , it is necessary to make available the information states in . Due to $\kappa $ -regularity at granularity m, this reduces to marking out the $\subset $ -maximal informatiobn states $s(\alpha ,i)$ in each block $B_i$ , for every one of the finitely many colour combinations for non-trivial information states s realised in ${\mathfrak {M}}\!\restriction \![w]_a,\rho _m$ . To this end we look at $\mathsf {MSO}$ -interpretability over derived single-sorted structures over $[w]_a$ . These encode the block decomposition (by an equivalence relation B) and the $\subset $ -maximal constituents across the blocks (by finitely many unary predicates $P_\alpha $ ):

$$\begin{align*}{\mathfrak{b}}_m([w]_a) \;:=\; \begin{array}[t]{@{}l@{}} ([w]_a,\rho_m, B, (P_\alpha) ) \\ \rule{0em}{3ex} \text{ for } \begin{array}[t]{@{}l@{\;:=\;}l@{}} \; B & \bigcup_{i < \kappa} B_i^2 = \{ (u,v) \in [w]_a^2 \colon u,v \text{ in the same block}\}, \\ \rule{0em}{3ex} P_\alpha & \bigcup_{i < \kappa} s(\alpha,i). \end{array} \end{array} \end{align*}$$

The full relational encoding of a ${\sim ^m}$ -local structure ${\mathfrak {M}}\!\restriction \! [w]_a,\rho _m$ becomes $\mathsf {MSO}$ -interpretable over these ${\mathfrak {b}}_m([w]_a)$ . In particular, for $s \in \wp ([w]_a)$ we have $s \in \Sigma _a(w)$ if, and only if

$$\begin{align*}\textstyle {\mathfrak{b}}_m([w]_a),s \models \exists X \Bigl( s \subset X \wedge \forall x \forall y \bigl( (Xx \wedge Xy) \rightarrow Bxy \bigr) \wedge \bigvee_\alpha X \subset P_\alpha\Bigr). \end{align*}$$

It follows that, for some fixed set-off c stemming from the underlying interpretation, and tuples $\mathbf {s},\mathbf {s}'$ of set parameters over $[w]_a$ and $[w']_a$ ,

(7) $$ \begin{align} {\mathfrak{b}}_m([w]_a), \mathbf{s} \equiv^{\mathsf{MSO}}_{r+c}{\mathfrak{b}}_m([w']_a), \mathbf{s}' \;\; \Rightarrow \;\; {\mathfrak{M}}\!\restriction\! [w]_a,\rho_m, \mathbf{s} \equiv^{\mathsf{FO}}_{r} {\mathfrak{M}}'\!\restriction\! [w']_a,\rho_m,\mathbf{s}' \end{align} $$

In the analysis of $\mathsf {FO}$ -equivalences between local ${\sim ^m}$ -structures (as part of the Ehrenfeucht–Fraïssé argument over exploded views as in the upgrading as in Figure 4) we shall encounter choices of elements inside these $2$ -sorted structures as parameters. These may be worlds $v \in [w]_a$ (first sort) or subsets $s \subset [w]_a$ (second sort). Looking at these in the $\mathsf {MSO}$ -perspective of the above interpretation, we can treat both kinds as monadic second-order parameters by associating $v \in [w]_a$ with $\{ v \} \subset [w]_a$ . In particular, a source world $w \in [w]_a$ for the local ${\sim ^m}$ -structure associated with $[w]_a$ can be fed as a distinguished world in ${\mathfrak {M}}\!\restriction \! [w]_a,\rho _m$ and as a singleton set parameter $\{ w\} \subset [w]_a$ in the $\mathsf {MSO}$ -analysis of ${\mathfrak {b}}_m([w]_a)$ .

Lemma 3.20. Any pair of m-bisimilar pointed ${\sim ^m}$ -local structures ${\mathbb {M}}\!\restriction \! [w]_a,w$ and ${\mathbb {M}}'\!\restriction \! [w']_a,w'$ for $m \geq 1$ that are both $\kappa $ -regular for the same (finite or infinite) value of $\kappa $ , realise the same colour combinations $\alpha \subset \rho _m([w]_a) = \rho _m([w']_a$ as nonempty contributions to the partitions of $[w]_a = \dot {\bigcup }_\alpha P_\alpha $ and $[w']_a = \dot {\bigcup }_\alpha P_\alpha '$ , respectively. Moreover

$$\begin{align*}{\mathfrak{b}}_m([w]_a), \{w\} \equiv^{\mathsf{MSO}}_q {\mathfrak{b}}_m([w']_a), \{w'\}, \end{align*}$$

provided both are sufficiently rich in relation to q.

It then follows from equation 7 that in this situation also

$$\begin{align*}{\mathfrak{M}}\!\restriction\! [w]_a,\rho_m,w \equiv^{\mathsf{FO}}_k {\mathfrak{M}}'\!\restriction\! [w']_a,\rho_m,w', \end{align*}$$

given the appropriate level of richness for $q = k+c$ (cf. Corollary 3.21 below).

In the comparisons between $\kappa $ -regular local ${\sim ^m}$ -structures ${\mathbb {M}} \!\restriction \! [w]_a, \rho _m$ and ${\mathbb {M}}' \!\restriction \! [w']_a, \rho _m$ it is essential that $m \geq 1$ . As remarked in the lemma, $\sim ^1$ between any two distinguished worlds, ${\mathbb {M}} \!\restriction \! [w]_a, \rho _m, w \sim ^1 {\mathbb {M}}' \!\restriction \! [w']_a, \rho _m,w'$ , implies that these two local structures are globally bisimilar and in particular realise the same ${\sim ^m}$ -types both of worlds $v \in [w]_a$ and $v' \in [w']_a$ and of information states and . The encodings of the block structure and $\subset $ -maximal information states in the $\kappa $ -regular inquisitive assignments and were essential for the background $\mathsf {MSO}$ -analysis over the first sorts, but we use these results towards the $\mathsf {FO}$ -analysis over their $2$ -sorted full relational encodings. In these terms we have established the following.

Corollary 3.21. If ${\mathbb {M}}$ and ${\mathbb {M}}'$ are both $\kappa $ -regular (for the same $\kappa $ ) at granularity m and sufficiently rich (in relation to $k \in {\mathbb {N}}$ ), then the following holds for any two worlds $v \in [w]_a$ and $v' \in [w']_a$ :

$$\begin{align*}\begin{array}{r@{\;\;\Rightarrow\;\;}l} {\mathbb {M}}\!\restriction\![w]_a, \rho_m, v \sim^1 {\mathbb {M}}'\!\restriction\![w']_a,\rho_m,v' & \\ \rule{0em}{3ex} {\mathbb {M}}\!\restriction\![w]_a, \rho_m, v \sim {\mathbb {M}}'\!\restriction\![w']_a,\rho_m,v' & {\mathfrak{M}}\!\restriction\! [w]_a, \rho_m, v \equiv_k {\mathfrak{M}}\!\restriction\! [w']_a, \rho_m ,v'. \end{array} \end{align*}$$

So Observation 3.15 and Proposition 3.18, any two inquisitive epistemic models ${\mathbb {M}}$ and ${\mathbb {M}}'$ admit, for any target value $N, k \in {\mathbb {N}}$ , globally bisimilar N-acyclic companions $\hat {{\mathbb {M}}} \sim {\mathbb {M}}$ and $\hat {{\mathbb {M}}}' \sim {\mathbb {M}}'$ , finite if ${\mathbb {M}}$ and ${\mathbb {M}}'$ are finite, whose locally full relational encodings satisfy the above transfer within every one of their local ${\sim ^m}$ -structures. This conditional guarantee of $\mathsf {FO}$ -indistinguishability is good for any allocation of the granularities $m \geq 1$ , which moreover may take different values for different pairs of local structures that are to be matched. It is important that the local analysis reflected in the corollary obviously imports – through $\rho _m$ – global information about ${\sim ^m}$ -types in $\hat {{\mathbb {M}}}$ and $\hat {{\mathbb {M}}}'$ into the local structures at hand, but that it does not rely on a uniform allocation of granularity across $\hat {{\mathbb {M}}}$ or $\hat {{\mathbb {M}}}'$ .

3.4.2 Local FO-equivalence of exploded views.

Returning to the global view of the underlying models ${\mathbb {M}} = (W,(\Sigma _a)_{a \in \mathcal {A}},V)$ and ${\mathbb {M}}' = (W',(\Sigma _a')_{a \in \mathcal {A}},V')$ and their exploded views, and assuming ${\mathbb {M}},w \;{\sim ^n}\; {\mathbb {M}}',w'$ , we recall equation (6) and its rôle on the lefthand side of Figure 4 for the world-pointed case. We first cover this basic, world-pointed version. The adaptation to the non-trivially state-pointed variant, involving the dummy agent s, will then be straightforward. For the world-pointed version, we need to lift the $[\,\cdot \,]_a$ -local equivalences (at suitable granularities $1 \leq m\leq n$ ) in matching local ${\sim ^m}$ -structures to the $\ell $ -local equivalence

$$\begin{align*}\mathsf{I}(\hat{{\mathfrak{M}}},\hat{w}) \;\equiv_{r}^{\scriptscriptstyle (\ell)}\; \mathsf{I}(\hat{{\mathfrak{M}}}',\hat{w}') \end{align*}$$

around the distinguished worlds $\hat {w}$ and $\hat {w}'$ . We aim to employ the criterion of N-acyclicity from Definition 3.16, more specifically its consequences for connectivity patterns in the exploded views. In order to reduce the notational overhead in the following we assume w.l.o.g. that $\hat {{\mathfrak {M}}} = {\mathfrak {M}}$ and $\hat {{\mathfrak {M}}}' = {\mathfrak {M}}'$ , or that ${\mathbb {M}}$ and ${\mathbb {M}}'$ themselves have been pre-processed in the sense of Proposition 3.18. In the exploded view of such N-acyclic ${\mathbb {M}}$ , any two local structures ${\mathfrak {M}}\!\restriction \![w_1]_{a_1} \not = {\mathfrak {M}}\!\restriction \![w_2]_{a_2}$ can be linked through at most one element v shared by $[w_1]_{a_1}$ and $[w_2]_{a_2}$ . This follows from Definition 3.16 for any $N \geq 2$ . Such a link, if it exists, relates the copies of v in the two component structures of $\mathsf {I}({\mathfrak {M}})$ by a path of length $2$ , which is formed by two $R_I$ -edges emanating from the node $v \in W$ in the core part. So this core part $(W,(E_a)_{a \in \mathcal {A}})$ , which is the underlying $S5$ frame, provides the only links between individual local constituents ${\mathfrak {M}}\!\restriction \![w_i]_{a_i}$ in the exploded view $\mathsf {I}({\mathbb {M}})$ . For N-acyclic ${\mathbb {M}}$ , this core part is N-acyclic, so that there cannot be any non-trivial overlaps between any two distinct threads of lengths up to $\ell $ of local constituents ${\mathfrak {M}}\!\restriction \![w_i]_{a_i}$ in the exploded view $\mathsf {I}({\mathbb {M}})$ emanating from the same $v \in W$ , provided $N> 2\ell $ .