2 Inquisitive modal logic

By $(p_i)_{i \in I}$ we denote a set of propositional variables. Following the terminology in [Reference Ciardelli2, Reference Ciardelli and Roelofsen6] we associate the following two kinds of states with a given non-empty set W of possible worlds.

Information states: any subset $s\subseteq W$ is called an information state; the set of information states over W is $\mathscr {P}(W)$ .

Inquisitive states: a non-empty set $\Pi $ of information states, $\Pi \subseteq \mathscr {P}(W)$ , is an inquisitive state if it is closed w.r.t. set inclusion: $s \in \Pi $ implies $t \in \Pi $ for all $t \subseteq s$ ; the set of inquisitive states over W is the set of those non-empty sets of information states in $\mathscr {P}(\mathscr {P}(W))$ that satisfy this characteristic downward closure condition.

A state-pointed (inquisitive modal) model is a pair $\mathbb {M}, s$ which consists of a model $\mathbb {M}$ together with a distinguished information state $s\subseteq W$ . If s is a singleton information state, i.e. $s=\{w\}$ for some $w\in W$ , we also speak of a world-pointed inquisitive model $\mathbb {M}, \{w\}$ for which we also write just $\mathbb {M}, w$ .

Note that the associated Kripke structure reduces the inquisitive assignment (of inquisitive states $\Sigma (w) \in \mathscr {P}(\mathscr {P}(W))$ ) to an assignment of single information states $\sigma (w) = \bigcup \Sigma (w) \in \mathscr {P}(W)$ that can be cast as sets of successors w.r.t. a modal accessibility relation. The natural relational encoding of $\sigma $ is in terms of the accessibility relation

$$ \begin{align*} R = \{ (w,w') \colon w' \in \sigma(w) \} \subseteq W\times W, \end{align*} $$

so that $\sigma (w)$ becomes the set of immediate successors of w w.r.t. R, i.e. the set $\sigma (w) = R[w] =\{ w' \colon (w,w') \in R \}$ . A corresponding, natural relational encoding of the inquisitive assignment will have to resort to a two-sorted encoding with a second sort of information states (from $\mathscr {P}(W)$ ) besides the first sort W of worlds (see Section 3.1 below). In this two-sorted scenario, however, the characteristic downward closure condition on the inquisitive states $\Sigma (w)$ would remain non-elementary. This motivates the following relaxation of the notion of models to what we call pseudo-models, which may also be cast in the model-theoretic tradition of approximate or weak models that reduce the complexity of higher-order features, similar to, e.g. the use of weak models in topological model theory [Reference Ziegler, Barwise and Feferman17]. As we shall see below, this concept can serve here as a useful tool for the analysis of the intended, proper models.

Compared to Definition 2.1, the following definition of pseudo-models just waives the downward closure requirement on inquisitive assignments.

Definition 2.2 (pseudo-models and inquisitive closure).

A pseudo-(inquisitive modal) model is a structure $\mathbb {M}=(W,\Sigma ,V)$ over the set of possible worlds W with propositional assignment $V: (p_i)_{i \in I}\rightarrow \mathscr {P}(W)$ and a function $\Sigma : W\rightarrow \mathscr {P}(\mathscr {P}(W)) \setminus \{ \emptyset \}$ , which assigns a non-empty subset $\Sigma (w)$ of $\mathscr {P}(W)$ but not necessarily an inquisitive state to every world $w \in W$ .

With any pseudo-model $\mathbb {M} = (W,\Sigma ,V)$ we associate its inquisitive closure $\mathbb {M}\!\downarrow := (W,\Sigma \!\downarrow ,V)$ , which is the proper model whose inquisitive assignment $\Sigma \!\downarrow $ is induced by $\Sigma $ according to

$$ \begin{align*} \begin{aligned}[t] \Sigma\!\downarrow: W&\longrightarrow\mathscr{P}(\mathscr{P}(W))\text{,}\\ w&\longmapsto\Sigma\!\downarrow\!(w):= \{t\in\mathscr{P}(W)\colon t\subseteq s\text{ for some }s\in\Sigma(w)\}. \end{aligned} \end{align*} $$

We note that the distinction between a pseudo-model and its inquisitive closure is immaterial at the level of the associated Kripke models with their modal assignment $\sigma (w) = \bigcup \Sigma (w) = \bigcup \Sigma \!\downarrow \!(w)$ .

Definition 2.3 ( $\mathrm{InqML}$ : syntax).

The basic syntax of $\mathrm{InqML}$ is given by the grammar

with negation, disjunction and diamond $\Diamond $ treated as abbreviations according to $\neg \varphi :=\varphi \rightarrow \bot $ , $\varphi \vee \psi :=\neg (\neg \varphi \wedge \neg \psi )$ , and $\Diamond \varphi :=\neg \Box \neg \varphi $ .

In [Reference Ciardelli2] the symbol is called intuitionistic disjunction, $\Box $ the universal modality and $\boxplus $ the inquisitive modality.

The following extends the standard definition of the semantics of $\mathrm{InqML}$ from [Reference Ciardelli2, Reference Ciardelli and Roelofsen6] to pseudo-models in a straightforward manner.

We note that the semantic clause for implication in Definition 2.4 refers to all subsets $t \subseteq s$ , over models or pseudo-models alike. Similarly, the downward closure condition known as persistency, as discussed in the following observation, speaks about all subsets $t \subseteq s$ of the given information state s, also when interpreted in the non-standard setting of pseudo-models.

Property (i) is called persistency in [Reference Ciardelli2, Reference Ciardelli and Roelofsen6] (and usually referred to as downward closure in team semantic terminology), while (ii) is called semantic ex-falso (reflecting the empty team property).

The following gives a further indication that extension of the semantics of $\mathrm{InqML}$ beyond the intended inquisitive models is very natural. The proof is by straightforward syntactic induction following the clauses of Definition 2.4; for the $\boxplus $ -case one uses persistency, and for the $\Box $ -case, which refers to the associated Kripke structure, one uses the fact that the associated modal assignment $\sigma $ is the same for the pseudo-model and its inquisitive closure.

Proposition 2.6. Let $\mathbb {M}$ be a pseudo-model, $\mathbb {M}\!\downarrow $ its inquisitive closure, and $s \subseteq W$ any information state over their common universe W of possible worlds. Then for $\varphi \in \mathrm{InqML}$ we have

$$ \begin{align*} \mathbb{M}\!\downarrow,s\models\varphi \;\;\Longleftrightarrow\;\; \mathbb{M},s\models\varphi. \end{align*} $$

This indicates that, as far as e.g. deductive reasoning is concerned, $\mathrm{InqML}$ might as well be cast in the extended setting of pseudo-models. The difference is important, though, e.g. in issues concerning what is the natural habitat for the key notion of model equivalence, viz. inquisitive bisimulation equivalence [Reference Ciardelli, Otto and Lang4] to be discussed in Section 5, or how $\mathrm{InqML}$ embeds into classical logics of reference like $\mathrm{FO}$ (cf. key results in [Reference Ciardelli, Otto and Lang4] vs. Corollary 5.8 here).

3 Standard translation

A standard translation serves as a semantically adequate (one could say, truthful) translation between logical frameworks.

Recall the well-known standard translation of modal logic $\mathrm{ML}$ into first-order logic $\mathrm{FO}$ . It is based on the straightforward transcription of the clauses for the Kripke semantics of $\mathrm{ML}$ into their natural first-order analogues over Kripke models viewed as ordinary relational first-order structures. The situation for $\mathrm{InqML}$ is different, because inquisitive (pseudo-)models are naturally rendered as two-sorted rather than ordinary single-sorted relational structures.Footnote ² Since an inquisitive assignment is a function from the set W of possible worlds to sets of sets of possible worlds, it is of inherently higher type than a modal assignment. Its natural relational encoding consists of a binary relation not over W itself, but between W (as a first sort) and a set S of information states (as a second sort) where $S \subseteq \mathscr {P}(W)$ . In the following we discuss a setting and format for a standard translation of $\mathrm{InqML}$ into $\mathrm{FO}$ in the natural two-sorted relational framework that is similar in spirit to that in [Reference Ciardelli, Otto and Lang4] but more liberal and more uniform (cf. Remark 3.5). The technical novelty underpinning this new approach is the application of a graded notion of flatness, graded flatness, to $\mathrm{InqML}$ , as independently developed by the first author in [Reference Meissner14].

We want to associate the semantics of inquisitive modal logic $\mathrm{InqML}$ over models (or even pseudo-models) with the semantics of first-order logic over associated two-sorted relational (pseudo-)models. As usual, this task involves two translation levels that need to go hand in hand: transformations linking the underlying (pseudo-)models $\mathbb {M}$ to relational representations $\mathscr {M}$ , from which the underlying (pseudo-)models $\mathbb {M}$ can be recovered as $\mathbb {M} = \mathbb {M}(\mathscr {M})$ ; and a translation of formulae $\varphi \in \mathrm{InqML}$ into formulae $\varphi ^{\ast } \in \mathrm{FO}$ such that

$$ \begin{align*} \mathbb{M}(\mathscr{M}),s \models \varphi \;\Longleftrightarrow\; \mathscr{M},s \models \varphi^{\ast}. \end{align*} $$

3.1 Relational representations of models

As relational counterparts of inquisitive (pseudo-)models we consider two-sorted relational structures of the form

$$ \begin{align*} \mathscr{M}=(W,S,\epsilon,E,(P_i)_{i \in I}) \end{align*} $$

with some non-empty sets W and S as first and second sorts, linked by two mixed-sorted binary relations $\epsilon ,E\subseteq W\times S$ , and with unary predicates $P_i\subseteq W$ over the first sort for all $p_i$ , $i \in I$ , that encode the propositional assignment as usual. The intended rôles of $\epsilon $ and E are as follows: the relation $\epsilon \subseteq W\times S$ encodes membership of possible worlds in information states, so that $s \in S$ can be associated with $\underline {s}:=\{w\in W\colon (w,s)\in \epsilon \} \in \mathscr {P}(W)$ ; and $E \subseteq W\times S$ encodes the inquisitive assignment as a relation that associates with each world $w \in W$ the set $E[w]:=\{s\in S\colon (w,s)\in E\} \in \mathscr {P}(S)$ .

Definition 3.1 (relational (pseudo-)models)

A structure $\mathscr {M}$ of the type above is a relational (inquisitive modal) model if the following conditions are satisfied for all $w \in W$ , $s,t \in S$ and $a \subseteq S$ :

1. (i) $\underline {s}=\underline {t} \;\Rightarrow \; s=t$ (extensionality);

2. (ii) $E[w]\not =\emptyset $ (non-emptiness);

3. (iii) if $a\subseteq \underline {s}$ for $s\in E[w]$ , then $a = \underline {t}$ for some $t\in E[w]$ (downward closure).

Correspondingly, a structure $\mathscr {M}=(W,S,\epsilon ,E,(P_i)_{i \in I})$ of the same format is a relational (inquisitive modal) pseudo-model if it satisfies (i) and (ii).

Relational (pseudo-)models with distinguished information states $s \in S$ are described as state-pointed or, in the case of singleton states $\underline {s} = \{ w \}$ as world-pointed, in analogy with the terminology for models. Due to extensionality (i), we shall identify information states $s \in S$ with sets of worlds $\underline {s} \subseteq W$ and regard the second sort S as a subset of the power set $\mathscr {P}(W)$ , with $\epsilon $ as the actual membership relation between W and $S \subseteq \mathscr {P}(W)$ .

Observation 3.2. The class $\mathscr {C}$ of all state-pointed (respectively world-pointed) relational pseudo-models is $\Delta $ -elementary, i.e. there exists a set of formulae $\Phi \subseteq \mathrm{FO}$ such that $\mathscr {C}=$ Mod $(\Phi )$ .Footnote ³

It is fairly easy to see that the class of all relational models cannot be $\Delta $ -elementary, as downward closure (condition (iii) in Definition 3.1) cannot be expressed without reference to arbitrary subsets of the first sort. Indeed, if it was $\Delta $ -elementary then so would be the class of all full relational models, defined by the additional condition that $S = \mathscr {P}(W)$ be the full power set. That, however, is ruled out by the observation that $\mathrm{FO}$ does not satisfy compactness over this class of all full relational models: over that class, $\mathrm{FO}$ captures the full power of monadic second-order logic $\mathrm{MSO}$ over the first sort; so it can, e.g., define the class corresponding to Kripke models that satisfy the well-foundedness condition of Löb frames (cf. [Reference Ciardelli, Otto and Lang4]).

Observation 3.3. The class of all relational models is not $\Delta $ -elementary.

From relational (pseudo-)models to (pseudo-)models

With any relational (pseudo-)model $\mathscr {M}=(W,S,\epsilon ,E,(P_i)_{i \in I})$ we associate the (pseudo-)model $\mathbb {M}(\mathscr {M}) = (W,\Sigma ,V)$ that decodes the relational information in $\mathscr {M}$ into functional assignments according to

$$ \begin{align*} \begin{array}{r@{}l} \Sigma \colon w&\ \longmapsto \{ s \in S \colon (w,s) \in E \},\\ \rule{0em}{3ex} V \colon p_i &\ \longmapsto \{ \displaystyle w \in W \colon w \in P_i \}. \end{array} \end{align*} $$

We observe that the actual extension of the second sort $S \subseteq \mathscr {P}(W)$ in $\mathscr {M}$ is immaterial in as far as it may go beyond the range of $\Sigma $ .

From (pseudo-)models to relational (pseudo-)models

With a (pseudo-)model $\mathbb {M} =(W,\Sigma ,V)$ and a distinguished information state $s \subseteq W$ , we associate as a relational representation any relational (pseudo-)model $\mathscr {M}=(W,S,\epsilon ,E,(P_i)_{i \in I})$ that encodes $\Sigma $ and V over sorts W and S, where $S \subseteq \mathscr {P}(W)$ is rich enough to represent the image $\Sigma (w) \subseteq \mathscr {P}(W)$ for all $w \in W$ as well as the distinguished information state s:

$$ \begin{align*} \begin{array}{r@{\;}c@{\;}l} S &\,\subseteq& \displaystyle \mathscr{P}(W) \mbox{ with } S \supseteq \{ s \} \;\cup \bigcup_{w \in W} \!\Sigma(w),\\ \rule{0em}{3ex} \epsilon &:=& \{ (w,s) \in W \times S \colon w \in s \} = \; \in\restriction\! (W\!\times\! S),\\ \rule{0em}{3ex} E &:=& \{(w,s)\in W\times S \colon s\in\Sigma(w) \},\\ \rule{0em}{3ex} P_i &:=& \{ w\in W\colon w\in V(p_i) \} \mbox{ for } i \in I. \end{array} \end{align*} $$

Note that $\mathscr {M}$ is fully determined by $\mathbb {M}$ once the actual extension of the second sort S is fixed; that however is naturally only subject to a richness condition. (We argued above that insistence on fullness, i.e. on the maximal extension $S = \mathscr {P}(W)$ , may not be advisable.)

Definition 3.4 (relational representations).

A relational (pseudo-)model $\mathscr {M}$ is a relational representation of a given (pseudo-)model $\mathbb {M}$ precisely for $\mathbb {M} = \mathbb {M}(\mathscr {M})$ .

A state-pointed relational (pseudo-)model $\mathscr {M},s$ is a relational representation of the state-pointed (pseudo-)model $\mathbb {M},s$ if in addition the distinguished information state s is represented as an element of its second sort S.Footnote ⁴

It is clear from the above that every state-pointed (pseudo-)model admits relational representations, and that every relational (pseudo-)model $\mathscr {M}$ represents a unique (pseudo-)model, viz. $\mathbb {M}(\mathscr {M})$ .

3.2 Graded flatness and the standard translation

Compared to the well-known standard translation for plain modal logic over Kripke models (for which $\mathbb {M}$ and $\mathscr {M}$ are practically identical), $\mathrm{InqML}$ involves challenges associated with the semantics of implication and $\Box $ . The corresponding clauses in Definition 2.4 involve reference to information states that might not necessarily be directly available in the second sort of $\mathscr {M}$ .

There are different suggestions to overcome this problem. An elimination of $\Box $ is possible via so-called resolutions [Reference Ciardelli2] or via the $\Box $ -free characteristic formulae for finitary bisimulation classes from [Reference Ciardelli, Otto and Lang4]; then a straightforward translation can be given. That standard translation, however, is based on stronger closure conditions on the universe of information states in the relational encodings of the inquisitive models, which give $\mathrm{FO}$ direct access to the relevant information states. Such stronger closure conditions may further interfere with compactness over the required classes of models, as mentioned in Section 3.1. A straightforward translation without elimination of $\Box $ is also possible but also requires stronger closure conditions on the class of relational models.

Remark 3.5. Compared to the previous translations, the present proposal is more general, more uniform and more direct: it works for the natural class of all pseudo-models and does not require any additional (elementary or non-elementary) closure conditions on the state universe of the intended relational models. Moreover, it is defined directly by induction on the unrestricted standard syntax of $\mathrm{InqML}$ , without appeal to specific syntactic normal forms.

Our standard translation relies on the following concept of graded flatness, which had also been investigated in the team-semantic context of dependence logic (cf. [Reference Kontinen13]) and in the context of inquisitive first-order logic (cf. [Reference Grilletti8]) under the name of coherence. For our context it was independently (re-)discovered and put to this new use in [Reference Meissner14]. Our preferred terminology of graded flatness derives from the notion of flatness in team semantics. If we think of information states (sets of worlds) as teams, then a formula $\varphi \in \mathrm{InqML}$ would be flat (in the team semantic sense) if its truth in s is equivalent to truth in $\{w\}$ for all $w \in s$ . Graded flatness generalises this idea to quantitative bounds on the size of subsets $s' \subseteq s$ that need to be investigated, rather than singleton subsets. Such a size bound can be obtained as a syntactic parameter as follows.

Definition 3.6 (flatness grade).

The flatness grade $\flat (\varphi )\in \mathbb {N}$ of $\varphi \in \mathrm{InqML}$ is defined by syntactic induction, for all $\psi ,\chi \in \mathrm{InqML}$ , according to

• – $\flat (\varphi ) := 0$ for atomic $\varphi $ and all $\varphi $ of the form $\Box \psi $ or $\boxplus \psi $ ;

• – $\flat (\psi \wedge \chi ) := \max \{\flat (\psi ), \flat (\chi )\}$ ;

• – $\flat (\psi \rightarrow \chi ) := \flat (\chi )$ ;

• – .

Proposition 3.7 (graded flatness).

Inquisitive modal logic $\mathrm{InqML}$ satisfies the following graded flatness property. For all $\varphi \in \mathrm{InqML}$ and state-pointed (pseudo-)models $\mathbb {M},s$ :

$$ \begin{align*} \mathbb{M},s\models\varphi \;\;\Longleftrightarrow\;\; \mathbb{M},t\models\varphi \mbox{ for all }\, t \subseteq s\; \mbox{ of size } \left|t\right|\leq\flat (\varphi)+1. \end{align*} $$

Proof. The direction from left to right follows immediately from persistency for $\mathrm{InqML}$ . The implication from right to left is shown by syntactic induction on $\varphi $ . We illustrate the -case, which is the most interesting.

For let $m:= \flat (\psi )$ and $n :=\flat (\chi )$ so that $\flat (\varphi )=m+n+1$ , and assume that for all $t \subseteq s$ of size $\left |t\right |\leq m+n+2$ . By Definition 2.4 and the induction hypothesis we get that for all $t \subseteq s$ with $\left |t\right |\leq m+n+2$ :

$$ \begin{align*} \begin{array}{rrl} & \forall a \subseteq t \text{ with }\left|a\right|\leq m+1: &\mathbb{M},a\models\psi \\ \mbox{ or } & \forall a \subseteq t \text{ with }\left|a\right|\leq n+1: &\mathbb{M},a\models\chi. \end{array} \end{align*} $$

It follows that

$$ \begin{align*} \begin{array}{rrl} & \forall t \subseteq s\text{ with }\left|t\right|\leq m+1: & \mathbb{M},t\models\psi \\ \mbox{ or } & \forall t \subseteq s\text{ with }\left|t\right|\leq n+1: & \mathbb{M},t\models\chi. \end{array} \end{align*} $$

Indeed, if this were false, there would exist states $t_{1}\subseteq s$ with $\left |t_{1}\right |\leq m+1$ and $t_{2}\subseteq s$ with $\left |t_{2}\right |\leq n+1$ such that $\mathbb {M},t_{1}\not \models \psi $ and $\mathbb {M},t_{2}\not \models \chi $ . But then, for $t_{0}:=t_{1}\cup t_{2}$ , the previous statement would be false: we have $\left |t_{0}\right |\leq m+n+2$ but $t_{1}\subseteq t_{0}$ violates the first disjunct and $t_{2}\subseteq t_{0}$ violates the second disjunct.

With the induction hypothesis we get .

We use the following notation. Generally, we take variable symbols $x,y, \ldots $ to be interpreted over the first sort (worlds), and variable symbols $\lambda ,\mu ,\ldots $ for the second sort (information states). A tuple of length n is denoted $\textbf {x}=(x_1,\ldots ,x_n)$ , the set of its components as $\{\textbf {x}\} = \{ x_1,\ldots ,x_n\}$ . If the length of a tuple is determined by some flatness grade $\flat (\varphi )$ , we write $\textbf {x}_{\varphi }$ for the tuple $(x_1,\ldots ,x_{\flat (\varphi )+1})$ and $\{\textbf {x}_{\varphi }\}$ for the associated set. For better readability we write $x\!\in \!\lambda $ instead of $\epsilon x\lambda $ in the following first-order formulae.

Our standard translation $\varphi \mapsto \varphi ^{\ast }(\lambda )$ is defined below, by syntactic induction on $\varphi \in \mathrm{InqML}$ . The interesting, somewhat non-standard feature involves the necessary passage between sorts: on one hand, $\varphi $ is translated into the first-order formula $\varphi ^{\ast }(\lambda )$ in a free variable $\lambda $ of the second sort, which is to be interpreted as the distinguished information state s; the core induction, on the other hand, deals with auxiliary formulae $\mathsf {ST}(\xi ,\textbf {x})$ in tuples $\textbf {x}$ of free variables of the first sort that capture the semantics of $\xi ^{\ast }(\mu )$ for $\mu = \{\textbf {x}\}$ .

Definition 3.8 (standard translation).

For $\varphi \in \mathrm{InqML}$ define its standard translation $\varphi ^*(\lambda )\in \mathrm{FO}$ in one free state variable $\lambda $ as

$$ \begin{align*} \varphi^*(\lambda):= \forall \textbf{x}_{\varphi} \left(\!\!\! \bigwedge_{\quad k \leq\flat(\varphi)+1} \!\!\!\!\!\!\!\!\! x_k \!\in\! \lambda \;\; \longrightarrow \; \mathsf{ST}(\varphi,\textbf{x}_{\varphi})\!\right), \end{align*} $$

where the auxiliary first-order formulae $\mathsf {ST}(\xi ,\textbf {x})$ , with free world variables among $\textbf {x}$ , are defined by syntactic induction according to:

• – $\displaystyle \mathsf {ST}(p,\textbf {x}):=\underset {k\leq n}{\bigwedge }Px_k$

• – $\displaystyle \mathsf {ST}(\bot ,\textbf {x}):= \bigwedge _{k\leq n} \neg x_k \!=\! x_k$

• – $\displaystyle \mathsf {ST}(\psi \wedge \chi ,\textbf {x}):=\mathsf {ST}(\psi ,\textbf {x})\wedge \mathsf {ST}(\chi ,\textbf {x})$

• – $\mathsf {ST}(\psi \rightarrow \chi ,\textbf {x}):=\forall \textbf {y} \left( \Bigl ( \bigwedge _{k\leq n} \bigvee _{l\leq n} y_k=x_l\Bigr ) \longrightarrow \bigl ( \mathsf {ST}(\psi ,\textbf {y})\rightarrow \mathsf {ST}(\chi ,\textbf {y})\bigr )\right)$

• –

• – $\displaystyle \mathsf {ST}(\Box \psi ,\textbf {x}):=\underset {k\leq n}{\bigwedge } \forall \textbf {y}_{\psi } \forall \boldsymbol {\mu }_{\psi } \left( \!\!\!\! \bigwedge _{\quad l \leq \flat (\psi )+1} \!\!\!\!\!\!\!\! \bigl ( Ex_k \mu _l\wedge y_l \!\in \! \mu _l \bigr ) \; \longrightarrow \; \mathsf {ST}(\psi ,\textbf {y}_{\psi }) \!\right) $

• – $\displaystyle \mathsf {ST}(\boxplus \psi ,\textbf {x}):=\underset {k\leq n}{\bigwedge }\forall \mu \left (Ex_k \mu \rightarrow \psi ^*(\mu )\right )$

The intuition for, e.g. the translation of $\Box $ in this definition is the following. We want to suitably mimic the semantics of $\Box $ in our context, hence we want to say that for all worlds $x_k\in \textbf {x}$ , $\psi ^*(\lambda )$ is satisfied by the information state $\sigma (x_k)$ . For this we need access to the states $\sigma (x_k)$ . Via the subformula $Ex_k \mu _l\wedge y_l \in \mu _l$ of our translation we can check whether a world $y_l$ is element of $\sigma (x_k)$ . Since $\sigma (x_k)$ is in general not necessarily represented as an element of the second sort of the relational pseudo-model that is supposed to satisfy the translation, we cannot access it directly via a state variable. Instead we can fix all its substates of size $\flat (\psi )+1$ in the shape of tuples of worlds via

$$ \begin{align*} \forall \textbf{y}_{\psi} \forall \boldsymbol{\mu}_{\psi} \left( \!\!\!\! \bigwedge_{\quad l \leq \flat(\psi)+1} \!\!\!\!\! \bigl( Ex_k \mu_l\wedge y_l \in \mu_l\bigr) \longrightarrow \; \mathsf{ST}(\psi,\textbf{y}_{\psi}) \!\right). \end{align*} $$

By Proposition 3.7 this correctly expresses that $\sigma (x_k)$ satisfies $\psi ^*(\lambda )$ .

Remark 3.9. We may analogously define a standard translation $\varphi ^{\ast }(x)$ in the single free world variable x of the first sort, which covers the world-pointed case just as the standard translation $\varphi ^{\ast }(\lambda )$ covers the state-pointed case. For this we may just use $\varphi ^{\ast }(x) := \mathsf {ST}(\varphi ,x)$ .Footnote ⁵

The following shows that the proposed standard translation is adequate – in preserving the semantics and turning $\mathrm{InqML}$ into a syntactic fragment of $\mathrm{FO}$ – over the rich class of relational encodings of (pseudo-)models.

Proposition 3.10 ( $\mathrm{InqML}$ as a fragment of $\mathrm{FO}$ ).

Let $\varphi \in \mathrm{InqML}$ and let $\varphi ^*(\lambda )\in \mathrm{FO}$ be its standard translation. Let $\mathbb {M},s$ be a (pseudo-)model and $\mathscr {M},s$ be a relational representation of $\mathbb {M},s$ . Then

$$ \begin{align*} \mathbb{M},s\models\varphi\;\Longleftrightarrow\;\mathscr{M},s\models\varphi^*(\lambda), \end{align*} $$

where the state variable $\lambda $ is interpreted as s.

Proof. We show below that, for $\varphi \in \mathrm{InqML}$ ,

$$ \begin{align*} \mathbb{M},\{\textbf{w}\}\models\varphi\;\Longleftrightarrow\;\mathscr{M},\textbf{w} \models \mathsf{ST}(\varphi,\textbf{x}) \qquad (\ast) \end{align*} $$

for all finite tuples of worlds $\textbf {w}$ from W and matching tuples $\textbf {x}$ of variables. From this we obtain the claim of the proposition, that $\mathbb {M},s\models \varphi \Leftrightarrow \mathscr {M},s\models \varphi ^*(\lambda )$ , as follows. By Proposition 3.7, $\mathbb {M},s\models \varphi $ is equivalent to

$$ \begin{align*} \forall t\subseteq s \text{ with } \left|t\right|\leq\flat(\varphi)+1:\mathbb{M},t\models\varphi, \end{align*} $$

which is further equivalent to

$$ \begin{align*} \forall \textbf{w}_{\varphi}\in s:\mathbb{M},\{\textbf{w}_{\varphi}\}\models\varphi\text{.} \end{align*} $$

(Note that for the direction from right to left we need $\mathbb {M},\emptyset \models \varphi $ on the right-hand side, but the set of all tuples $\textbf {w}_{\varphi }\in s$ of size $1\leq \left |\textbf {w}_{\varphi }\right |\leq \flat (\varphi )+1$ does not contain the empty tuple. This, however, is unproblematic for the equivalence since $\mathbb {M},\emptyset \models \varphi $ trivially holds by Observation 2.5.) With $(\ast )$ we find that $\mathbb {M},s\models \varphi $ is equivalent to

$$ \begin{align*} \forall\textbf{w}_{\varphi}\in s:\mathscr{M},\textbf{w}_{\varphi}\models \mathsf{ST}(\varphi,\textbf{x}_{\varphi}), \end{align*} $$

which translates equivalently into

$$ \begin{align*} \mathscr{M}, s \models\forall \textbf{x}_{\varphi} \left( \!\!\!\!\!\bigwedge_{\quad k \leq \flat(\varphi)+1} \!\!\!\!\!\!\! x_k \!\in\! \lambda \;\; \longrightarrow \; \mathsf{ST}(\varphi,\textbf{x}_{\varphi}) \!\right), \end{align*} $$

which is the same as $\mathscr {M},s\models \varphi ^*(\lambda )$ , by Definition 3.8.

It remains to show $(\ast )$ by syntactic induction. We explicitly treat the $\Box $ - and $\boxplus $ -steps, and show the implication from left to right in each case.

For the case of $\varphi =\Box \psi $ assume $\mathbb {M},\{\textbf {w}\}\models \Box \psi $ , which, by Definition 2.4 and Proposition 3.7, means that

$$ \begin{align*} \forall w\in \{\textbf{w}\}\;\forall t\subseteq\sigma(w)\text{ with }\left|t\right|\leq\flat(\psi)+1:\mathbb{M},t\models\psi. \end{align*} $$

This is further equivalent to

$$ \begin{align*} \forall w\in\{\textbf{w}\}\;\forall \textbf{u}_{\psi} \in\sigma(w):\mathbb{M},\{\textbf{u}_{\psi}\}\models\psi, \end{align*} $$

and by induction hypothesis to

$$ \begin{align*} \forall w\in\{\textbf{w}\}\;\forall \textbf{u}_{\psi}\in\sigma(w): \mathscr{M},\textbf{u}_{\psi}\models \mathsf{ST}(\psi,\textbf{y}_{\psi}). \end{align*} $$

This condition is correctly rendered in $\mathrm{FO}$ as

$$ \begin{align*} \displaystyle \mathscr{M},\textbf{w}\models \mathsf{ST}(\Box\psi,\textbf{x}) =\underset{k\leq n}{\bigwedge} \forall \textbf{y}_{\psi} \forall \boldsymbol{\mu}_{\psi} \left( \!\!\!\! \bigwedge_{\quad l \leq \flat(\psi)+1} \!\!\!\!\!\!\!\! \bigl( Ex_k \mu_l\wedge y_l \!\in\! \mu_l \bigr) \; \longrightarrow \; \mathsf{ST}(\psi,\textbf{y}_{\psi}) \!\right): \end{align*} $$

universal quantification over $w\in \{\textbf {w}\}$ is expressed by the conjunction over the $x_k\in \textbf {x}$ enumerating the $w_k\in \textbf {w}$ ; the quantification $\forall \textbf {u}_{\psi }\in \sigma (w)$ is represented by the quantification $\forall \textbf {y}_{\psi } \forall \boldsymbol {\mu }_{\psi } $ , relativised so that the $y_l$ are instantiated by worlds from $\sigma (w_k)$ .

For the case $\varphi =\boxplus \psi $ assume $\mathbb {M},\{\textbf {w}\}\models \boxplus \psi $ . With Definition 2.4 and Proposition 3.7 we get

$$ \begin{align*} \forall w\in \{\textbf{w}\}\;\forall t\in\Sigma(w)\;\forall a\subseteq t \text{ with }\left|a\right|\leq\flat(\psi)+1:\mathbb{M},a\models\psi, \end{align*} $$

hence

$$ \begin{align*} \forall w\in \{\textbf{w}\}\;\forall t\in\Sigma(w)\;\forall \textbf{u}_{\psi}\in t : \mathbb{M},\{\textbf{u}_{\psi}\}\models\psi. \end{align*} $$

By induction hypothesis we get

$$ \begin{align*} \forall w\in \{\textbf{w}\}\;\forall t\in\Sigma(w)\;\forall \textbf{u}_{\psi}\in t : \mathscr{M},\textbf{u}_{\psi}\models \mathsf{ST}(\psi,\textbf{y}_{\psi}). \end{align*} $$

Again we can express this in FO according to

$$ \begin{align*} \mathscr{M},\textbf{w}\models\underset{k\leq n}{\bigwedge}\forall \mu \left[ Ex_k \mu\longrightarrow \left(\forall \textbf{y}_{\psi}\left( \!\!\!\! \bigwedge_{\quad l \leq \flat(\psi)+1} \!\!\!\!\!\!\!\!\! y_l\in \mu \; \longrightarrow \; \mathsf{ST}(\psi,\textbf{y}_{\psi})\right)\right)\right], \end{align*} $$

which is $\mathscr {M},\textbf {w}\models \mathsf {ST}(\boxplus \psi ,\textbf {x})$ by Definition 3.8.

Remark 3.11. The analogue of Proposition 3.10 for world-pointed models and our world-version of the standard translation from Remark 3.9 is easily checked.

4 Compactness for $\mathrm{InqML}$

It is known that $\mathrm{InqML}$ has a sound and strongly complete proof calculus and therefore satisfies compactness (cf. [Reference Ciardelli2]). We use our standard translation to give a new, purely model-theoretic proof, essentially by reduction to first-order compactness. But while the corresponding reduction is totally straightforward for basic modal logic $\mathrm{ML}$ over Kripke structures, we here need to deal with the additional complication that the class of relational models is not $\Delta $ -elementary. Correspondingly, a detour through pseudo-models plays an essential rôle in our proof. Moreover, the proof also shows that compactness over the class of all pseudo-models works in a straightforward manner. We interpret this as an additional, natural indication that $\mathrm{InqML}$ could also be explored over the extended class of all pseudo-models.

We consider the satisfiability version of compactness. Of course, by semantic ex-falso (cf. Observation 2.5), any set $\Phi \subseteq \mathrm{InqML}$ is trivially satisfied by any model $\mathbb {M},\emptyset $ . For a non-trivial statement we need to exclude the empty state.

With persistency it is easy to see that compactness over the class of all state-pointed (pseudo-)models implies compactness over the class of all world-pointed (pseudo-)models.

5 A Hennessy-Milner class for $\mathrm{InqML}$

The notion of inquisitive bisimulation from [Reference Ciardelli, Otto and Lang4] plays an essential rôle for $\mathrm{InqML}$ as does ordinary bisimulation for plain modal logic $\mathrm{ML}$ (for background cf. [Reference Goranko, Otto, Blackburn, Wolter and van Benthem7]). In particular, inquisitive n-bisimulation equivalence $\sim _n$ between two inquisitive models represents a finite approximation to full inquisitive bisimulation equivalence; at level $n \in \mathbb {N}$ , $\sim _n$ is related to $\mathrm{InqML}$ -equivalence up to nesting depth n (of the modalities $\Box $ and $\boxplus $ ), in the familiar style of an Ehrenfeucht–Fraïssé correspondence for $\mathrm{InqML}$ [Reference Ciardelli, Otto and Lang4] (see Theorem 5.1 below). Full inquisitive bisimulation equivalence $\sim $ between world- or state-pointed inquisitive models is naturally defined in terms of back&forth systems, bisimulation relations, or winning strategies for the defender (player $\textbf{II}$ ) in the corresponding infinite back&forth game. The finite levels $\sim _n$ for $n \in \mathbb {N}$ are best understood as approximations to $\sim $ in terms of winning strategies for player $\textbf{II}$ in the n-round back&forth game; the common refinement $\sim _{\omega }$ of all the finite levels $\sim _n$ is defined in terms of winning strategies for any finite number of rounds, which in general is characteristically weaker than full $\sim $ . The crucial feature of the back&forth games for inquisitive bisimulation is that each round comprises two phases so that the probing of state-pointed positions is interleaved with a probing of intermediate world-pointed positions (for details of the game and a fuller discussion we refer to [Reference Ciardelli, Otto and Lang4]).

The following summarises the Ehrenfeucht–Fraïssé correspondence derived in [Reference Ciardelli, Otto and Lang4]. We write $\equiv _{\mathrm{InqML}}^n$ for $\mathrm{InqML}$ -equivalence between world- or state-pointed inquisitive models up to nesting depth n, and use the term $\sim _n$ -types for $\sim _n$ -equivalence classes (of world- or state-pointed) inquisitive modal models.

Theorem 5.1 (inquisitive Ehrenfeucht–Fraïssé [Reference Ciardelli, Otto and Lang4]).

For world- or state-pointed inquisitive modal models over a finite signature and $n \in \mathbb {N}$ :

$$ \begin{align*} \begin{array}{rcl} \mathbb{M},w \sim_n \mathbb{M}',w' &\Leftrightarrow & \mathbb{M},w \equiv_{\mathrm{InqML}}^n \mathbb{M}',w', \\ \rule{0em}{3ex} \mathbb{M},s \sim_n \mathbb{M}',s' &\Leftrightarrow & \mathbb{M},s \equiv_{\mathrm{InqML}}^n\mathbb{M}',s'. \end{array} \end{align*} $$

In particular, $\mathrm{InqML}$ is preserved under $\sim $ , and $\sim _{\omega }$ coincides with $\mathrm{InqML}$ -equivalence over finite signatures. Moreover, for world- or state-pointed inquisitive modal models $\mathbb {M},w$ or $\mathbb {M},s$ over a finite signature, there are characteristic formulae $\chi _{\mathbb {M},w}^n $ and $\chi _{\mathbb {M},s}^n$ of $\mathrm{InqML}$ that define $\sim _n$ -types (up to persistency, cf. Observation 2.5) in the sense that

$$ \begin{align*} \begin{array}{rcl} \mathbb{M}',w' \models \chi_{\mathbb{M},w}^n&\Leftrightarrow & \mathbb{M}',w' \sim_n \mathbb{M},w, \\ \rule{0em}{3ex} \mathbb{M}',s' \models \chi_{\mathbb{M},s}^n &\Leftrightarrow & \mathbb{M}',s' \sim_n \mathbb{M},s_0 \mbox{ for some } s_0 \subseteq s. \end{array} \end{align*} $$

We remark that the characteristic formulae $\chi _{\mathbb {M},w}^n$ , for $\sim _n$ -types of worlds, are truth-conditional (in the terminology of [Reference Ciardelli2, Reference Ciardelli, Otto and Lang4]) or flat (in the terminology of team semantics). This means that

$$ \begin{align*} \begin{array}{rcl} \mathbb{M}',s' \models \chi_{\mathbb{M},w}^n &\Leftrightarrow &\mathbb{M}',\{ w' \} \models \chi_{\mathbb{M},w}^n \mbox{ for all } w' \in s' \\ \rule{0em}{3ex} &\Leftrightarrow &\mathbb{M}',w' \models \chi_{\mathbb{M},w}^n \; \mbox{ for all } w' \in s'. \end{array} \end{align*} $$

For plain modal logic $\mathrm{ML}$ and many of its relatives, the significant gap between $\sim $ and $\sim _{\omega }$ , and between $\sim _{\omega }$ and $\equiv _{\mathrm{ML}}$ for infinite signatures, is bridged by modally saturated and in particular by $\omega $ -saturated models. This phenomenon, which for basic modal logic is (a generalisation of) the well-known Hennessy–Milner theorem, is a crucial tool in the model theory of modal logic [Reference Goranko, Otto, Blackburn, Wolter and van Benthem7]: $\omega $ -saturated Kripke structures are modally saturated and satisfy the Hennessy–Milner correspondence

$$ \begin{align*} \mathcal{K},w \sim \mathcal{K}',w' \; \Leftrightarrow \; \mathcal{K},w \sim_{\omega} \mathcal{K}',w' \; \Leftrightarrow \; \mathcal{K},w \equiv_{\mathrm{ML}} \mathcal{K}',w'. \end{align*} $$

We here establish an inquisitive version of this Hennessy-Milner phenomenon, which technically works with $\omega $ -saturated relational pseudo-models and our standard translation. It turns out that the passage through pseudo-models is absolutely crucial for the argument (cf. Observation 5.3).

In what follows we could consider signatures of arbitrary infinite cardinalities, i.e. with arbitrary index sets I for the family of basic propositions $(p_i)_{i \in I}$ ; but to simplify the formal account, and without any essential loss of generality, we stick to at most countably infinite I. Consider $\mathrm{InqML}$ -types of worlds of inquisitive (pseudo-)models: for a world $w \in W$ in the (pseudo-)model $\mathbb {M}$ , let $\rho _w:=\{\varphi \in \mathrm{InqML}\colon \mathbb {M},w\models \varphi \}$ be its $\mathrm{InqML}$ -type. Even if the overall signature is infinite, any individual $\mathrm{InqML}$ - or $\mathrm{FO}$ -formula can only refer to finitely many basic propositions (or their relational counterparts). In this sense we have $\mathrm{InqML} = \bigcup _k \mathrm{InqML}_k$ for its fragments $\mathrm{InqML}_k$ that use just the first k basic propositions from $I_k \subseteq I$ , for $k \in \mathbb {N}$ . The $\mathrm{InqML}$ -type of a world in a (relational) pseudo-model therefore always is the union of its restrictions to finite sub-signatures, which are types in corresponding reducts.

For bisimulation types, i.e. equivalence classes w.r.t. $\sim $ or $\sim _n$ , however, the situation is different. If we denote as $\sim _{n,k}$ the notion of n-bisimilarity of the $I_k$ -reducts of models, then even at the level of $n=1$ , all the $\sim _{1,k}$ -types do not determine the $\sim _1$ -type of a world w, as the former do e.g. not determine whether w has a Kripke-successor in which infinitely many basic propositions are satisfied simultaneously.

In the following we want to consider standard translations of $\mathrm{InqML}$ -formulae on world-pointed relational inquisitive models and therefore use the world-version of the standard translation from Remark 3.9 whenever this is appropriate. With a world w in some relational pseudo-model we associate its complete $\mathrm{InqML}$ -type $\rho _w$ with a partial first-order type $\rho ^{\ast }_w(x)$ consisting of the standard translations of all formulae in $\rho _w$ . So $\rho _w$ is determined by (the standard translations of) the characteristic formulae $\chi ^{n,k}_w\in \mathrm{InqML}_k$ for the $\sim _n$ -types of w in the $I_k$ -reducts, i.e. the $\sim _{n,k}$ -types, for all $n,k \in \mathbb {N}$ , by Theorem 5.1.

From now on, for reasons of simplicity, we identify $\mathrm{InqML}$ -formulae like $\chi ^{n,k}_v$ with their standard translation in $\mathrm{FO}$ , which is expressed as $\chi ^{n,k}_v(x)$ in a first-order variable of the first sort, or as $\chi ^{n,k}_v(\lambda )$ in a first-order variable of the second sort in case we consider state-pointed relational inquisitive models.

Recall from classical model theory (see e.g. [Reference Hodges11]) that a first-order structure is $\omega $ -saturated if it realises every first-order type with finitely many parameters. Generally, a (partial) first-order type of a $\sigma $ -structure $\mathcal {A}$ is a set of $\mathrm{FO}(\sigma )$ -formulae $\Phi $ in some tuple of free variables that is consistent with the complete $\mathrm{FO}(\sigma )$ -theory of $\mathcal {A}$ ; a tuple of elements of A realises $\Phi $ if all $\varphi \in \Phi $ are satisfied by this tuple. A (partial) type with parameters $\textbf{a}$ from A is a (partial) type of the expansion of $\mathcal {A}$ with new constant symbols for the $a \in \textbf{a}$ , so that $\Phi _{\textbf{a}}$ can specify first-order properties in relation to these parameters in $(\mathcal {A},\textbf{a})$ .Footnote ⁶

Classical chain constructions based on $\mathrm{FO}$ compactness establish that any first-order structure admits elementary extensions that are $\omega $ -saturated. Compactness is also at the heart of the straightforward argument for the following fact, to be used in the proof of our main result of this section.

In the following, we say that an element $s\in \mathscr {P}(W)$ is represented in the second sort of a relational pseudo-model if $s\in S\subseteq \mathscr {P}(W)$ .

Lemma 5.2. Let $s \in S$ be represented in the second sort of an $\omega $ -saturated relational pseudo-model $\mathscr {M}$ , $\rho _v(x)$ as above (not necessarily realised in $\mathscr {M}$ ). Then $\rho _v(x)$ is realised by a world in s in $\mathscr {M}$ iff

$$ \begin{align*} \mathscr{M},s \models \exists x \left( x\!\in\! s \wedge \chi^{n,k}_v(x) \right) \ \ \mbox{for all } k,n \in \mathbb{N}. \end{align*} $$

This lemma implies in particular that $\omega $ -saturation is at odds with full downward closure. This is the reason why our inquisitive version of the Hennessy–Milner correspondence must be based on $\omega $ -saturated relational pseudo-models rather than relational encodings of proper models.

Indeed, an information state whose worlds admit arbitrarily long but just finite Kripke-paths (Löb condition) cannot be represented in an $\omega $ -saturated pseudo-model, because any such state would also have to contain a world with an infinite Kripke-path. This follows as $\omega $ -saturation would inductively always provide a next Kripke-successor that still has Kripke-paths of unbounded finite lengths in front of it.

We define an auxiliary equivalence relation between state-pointed pseudo-models as follows: $\mathbb {M},s$ and $\mathbb {M}',s'$ are bulk-equivalent,

$$ \begin{align*} (\dagger) \quad \mathbb{M},s \equiv^{bulk}_{\mathrm{InqML}}\mathbb{M}',s', \end{align*} $$

if for every $w\in s$ there is some $w'\in s'$ such that $\mathbb {M},w \equiv _{\mathrm{InqML}} \mathbb {M}',w'$ , and vice versa. In general, $\equiv ^{bulk}_{\mathrm{InqML}}$ is a proper strengthening of $\equiv _{\mathrm{InqML}}$ ; the two do coincide, however, for $\omega $ -saturated pseudo-models and for information states that are represented in the second sort. In that situation, ordinary $\mathrm{InqML}$ -equivalence reflects the natural relationship between state- and world-based inquisitive bisimulation: state-equivalence $\mathbb {M},s \equiv _{\mathrm{InqML}} \mathbb {M}',s'$ as a flat lifting of world-equivalence, in the spirit of our bulk equivalence.

Lemma 5.5. For pairs of state-pointed pseudo-models $\mathbb {M},s$ and $\mathbb {M}',s'$ stemming from $\omega $ -saturated relational pseudo-models $\mathscr {M}$ and $\mathscr {M}'$ :

$$ \begin{align*} \mathbb{M} \!\downarrow,s \equiv^{bulk}_{\mathrm{InqML}} \mathbb{M}' \!\downarrow,s' \; \Rightarrow \; \mathbb{M} \!\downarrow,s \sim \mathbb{M}'\!\downarrow,s'. \end{align*} $$

Note that the information states $s \subseteq W$ and $s' \subseteq W'$ in the premise of the claim of the lemma are arbitrary information states and need not themselves be represented in the second sort of the underlying relational pseudo-models $\mathscr {M}$ and $\mathscr {M}'$ . However, by Remark 5.4, Lemma 5.5 implies the same conclusion for states s and $s'$ that are represented in the second sort of $\mathscr {M}$ and $\mathscr {M}'$ , respectively, under the weaker assumption that $\mathbb {M} \!\downarrow ,s \equiv _{\mathrm{InqML}} \mathbb {M}' \!\downarrow ,s' $ .

Proof. The idea is to represent or simulate the infinite bisimulation game from [Reference Ciardelli, Otto and Lang4] on $\mathbb {M}\!\downarrow ;\mathbb {M}'\!\downarrow $ in terms of the underlying relational pseudo-models $\mathscr {M};\mathscr {M}'$ . The challenge lies in dealing with those information states that may essentially occur in the bisimulation game without being represented in the second sort of the underlying relational pseudo-models.

For the claim of the lemma it suffices to show that player $\textbf{II}$ can maintain $\equiv ^{bulk}_{\mathrm{InqML}}$ through a single round in the following sense: starting from a state position $\bigl (\mathbb {M}\!\downarrow ,s; \mathbb {M}'\!\downarrow, s'\bigr )$ with $\mathbb {M}\!\downarrow ,s\equiv ^{bulk}_{\mathrm{InqML}}\mathbb {M}'\!\downarrow ,s'$ , player $\textbf{II}$ can respond to any world challenge from player $\textbf{I}$ to get to a world position $\bigl (\mathbb {M}\!\downarrow ,w;\mathbb {M}'\!\downarrow ,w'\bigr )$ such that $\mathbb {M}\!\downarrow ,w\equiv _{\mathrm{InqML}}\mathbb {M}'\!\downarrow ,w'$ , and from there respond to any state challenge from player $\textbf{I}$ to get again to a state position $\bigl (\mathbb {M}\!\downarrow ,t;\mathbb {M}'\!\downarrow ,t'\bigr )$ such that $\mathbb {M}\!\downarrow ,t\equiv ^{bulk}_{\mathrm{InqML}}\mathbb {M}'\!\downarrow ,t'$ .

Let $\mathbb {M}\!\downarrow ,s \equiv ^{bulk}_{\mathrm{InqML}} \mathbb {M}'\!\downarrow ,s'$ and assume w.l.o.g. that player $\textbf{I}$ picks an element $w \in s$ ; then by the definition of $\equiv ^{bulk}_{\mathrm{InqML}}$ at $(\dagger )$ , player $\textbf{II}$ can respond with some $w' \in s'$ with $\mathbb {M}\!\downarrow ,w\equiv _{\mathrm{InqML}}\mathbb {M}'\!\downarrow ,w'$ . If player $\textbf{I}$ now picks (again w.l.o.g.) an information state $t\in \Sigma \!\downarrow \!(w)$ in $\mathbb {M}\!\downarrow $ , we need player $\textbf{II}$ to respond with some $t' \in \Sigma '\!\downarrow \!(w')$ in $\mathbb {M}'\!\downarrow $ such that $\mathbb {M}\!\downarrow ,t \equiv ^{bulk}_{\mathrm{InqML}} \mathbb {M}'\!\downarrow ,t'$ .

For this consider the partial $\mathrm{FO}$ -type describing the essential properties of t (in variable $\lambda $ of the second sort) in $\mathscr {M}$ (with parameter w):Footnote ⁷

$$ \begin{align*} \Phi_w(\lambda) := \{ E w\lambda \} \cup \left\{ \exists x \left( x \in \lambda \wedge \chi_v^{n,k} (x) \right)\colon n,k \in \mathbb{N}, v \in t \;\right\}, \end{align*} $$

where $\chi _v^{n,k}(x)$ is (the standard translation of) the $\mathrm{InqML}$ -formula that characterises the $\sim _{n,k}$ -type of $\mathbb {M}\!\downarrow , v$ . We want to show that $\Phi _{w'}(\lambda )$ (with parameter $w'$ ) is finitely satisfiable in $\mathscr {M}'$ and hence a partial type of $\mathscr {M}'$ . It suffices to show that $\mathscr {M}',w'$ satisfies every formula of the form

$$ \begin{align*} \varphi(x)= \exists \lambda \left( E x \lambda \wedge \bigwedge_{i\leq m} \exists y \bigl( y\!\in\! \lambda \wedge \chi_{v_i}^{n,k}(y)\bigr)\right), \end{align*} $$

for $n,m,k \in \mathbb {N}$ and $v_1,\ldots ,v_m \in t$ . For this claim we can use the fact that $\mathbb {M},w \equiv _{\mathrm{InqML}} \mathbb {M}',w'$ , which implies that $\mathbb {M}\!\downarrow ,w \sim _{n+1,k}\mathbb {M}'\!\downarrow ,w'$ . So for the state $t\in \Sigma \!\downarrow \!(w)$ there is some $t^*\in \Sigma '\!\downarrow \!(w')$ in $\mathbb {M}'\!\downarrow $ with $\mathbb {M}\!\downarrow ,t \sim _{n,k} \mathbb {M}'\!\downarrow ,t^*$ . Let $\hat {t}'\in \Sigma '(w')$ be an information state in the pseudo-model $\mathbb {M}'$ that is represented in the second sort of $\mathscr {M}'$ , such that $t^*\subseteq \hat {t}'$ . Then for every $v\in t$ there is some $v'\in t^*\subseteq \hat {t}'$ with $\mathbb {M}\!\downarrow ,v \sim _{n,k} \mathbb {M}'\!\downarrow ,v'$ , hence with $\mathbb {M}'\!\downarrow ,v'\models \chi _{v}^{n,k}(y)$ . So $\mathscr {M}',w'\models \varphi (x)$ , with $\hat {t}'$ as an existential witness for $\lambda $ . Then $\Phi _{w'}(\lambda )$ is consistent with the $\mathrm{FO}$ -theory of $\mathscr {M}',w'$ (i.e. a partial type with parameter $w'$ in $\mathscr {M}'$ ).

By $\omega $ -saturation of $\mathscr {M}'$ there is a realisation $\tilde {t}'$ of $\Phi _{w'}(\lambda )$ . So (by Lemma 5.2 and using $\omega $ -saturation again) there is, for every world $v\in t$ , some world $v'\in \tilde {t}'$ that realises its $\mathrm{InqML}$ -type $\rho _v$ , i.e. such that $\mathbb {M}\!\downarrow ,v \equiv _{\mathrm{InqML}} \mathbb {M}'\!\downarrow ,v'$ . Now

$$ \begin{align*} t':=\{v'\in\tilde{t}'\colon\exists v\in t\text{ with }\mathbb{M}\!\downarrow,v \equiv_{\mathrm{InqML}} \mathbb{M}'\!\downarrow,v'\} \subseteq \tilde{t}' \end{align*} $$

is an information state in $\Sigma '\!\downarrow \!(w')$ , as $\tilde {t}'\in \Sigma '(w')$ in $\mathbb {M}'$ ( $\tilde {t}' \in E[w']$ in $\mathscr {M}'$ ). It follows that $t' \in \Sigma '\!\downarrow \!(w')$ is an appropriate response to match $t \in \Sigma \!\downarrow \!(w)$ . Indeed, for every world $v \in t$ there is a world $v' \in t'$ and vice versa, with $\mathbb {M}\!\downarrow ,v \equiv _{\mathrm{InqML}} \mathbb {M}'\!\downarrow ,v'$ . So we have $\mathbb {M}\!\downarrow ,t \equiv ^{bulk}_{\mathrm{InqML}} \mathbb {M}'\!\downarrow ,t'$ , and $t'$ is as desired.

Lemma 5.5 does give rise to a nice class of models with a Hennessy–Milner property for $\mathrm{InqML}$ .

Corollary 5.6 (a Hennessy–Milner class for $\mathrm{InqML}$ ).

If $\mathbb {M} = \mathbb {M}(\mathscr {M})$ and $\mathbb {M}'= \mathbb {M}(\mathscr {M}')$ arise as pseudo-models from $\omega $ -saturated relational pseudo-models $\mathscr {M}$ and $\mathscr {M}'$ , then their $\downarrow $ -closures, which are proper models, satisfy the following Hennessy–Milner property for bulk-equivalentFootnote ⁸ states:

$$ \begin{align*} \mathbb{M}\!\downarrow, s\equiv^{bulk}_{\mathrm{InqML}} \mathbb{M}'\!\downarrow, s' \;\; \Leftrightarrow \;\; \mathbb{M}\!\downarrow, s \;\sim\; \mathbb{M}'\!\downarrow, s'. \end{align*} $$

Similarly, for worlds:

$$ \begin{align*} \mathbb{M}\!\downarrow, w\equiv_{\mathrm{InqML}} \mathbb{M}'\!\downarrow, w' \;\; \Leftrightarrow \;\; \mathbb{M}\!\downarrow, w \;\sim\; \mathbb{M}'\!\downarrow, w'. \end{align*} $$

As further corollaries we obtain characterisation results for $\mathrm{InqML}$ as a fragment of $\mathrm{FO}$ , in the style of a van Benthem theorem. The relevant notions of inquisitive bisimulation equivalence can be naturally transferred from models to their relational encodings as in [Reference Ciardelli, Otto and Lang4].

The following corollary crucially differs from the characterisation obtained along very different routes in [Reference Ciardelli and Otto5]. On the one hand, the underlying elementary class of pseudo-models, which our new characterisation refers to, is considerably wider than the non-elementary class of relational encodings of proper models. On the other hand, it therefore significantly involves preservation assumptions that bridge the gap between pseudo-models and proper models. Involving the natural extension of the semantics of $\mathrm{InqML}$ to this wider class of pseudo-models, it also enriches the analysis of the relation between $\mathrm{InqML}$ and $\mathrm{FO}$ in another direction.

We first state and sketch the proof for the simpler version of this characterisation for world properties; the more general characterisation of state properties, with persistency as an additional semantic constraint, is then treated in Corollary 5.11.

Compare Definition 2.2 for the notion of inquisitive closure, which involves downward closure w.r.t. information states in inquisitive assignments, in the passage from $\Sigma $ to $\Sigma \!\downarrow $ or the analogous passage in the relational encoding of $\Sigma $ in terms of E.

For the following we adapt the notion of inquisitive closure (from Definition 2.2) to state-pointed relational pseudo-models so as to include all subsets of the distinguished information state in the second sort:Footnote ⁹ the inquisitive closure $(\mathscr {M},s)\!\downarrow $ augments the second sort of the relational encoding of $\mathbb {M}(\mathscr {M})\!\downarrow $ by representations of all subsets of s in the second sort in as far as they are not already covered as subsets of information states in inquisitive assignments.

In the following, we invoke the set of all boolean combinations of (standard translations) of $\mathrm{InqML}$ -formulae, meaning the closure of all standard translations of $\mathrm{InqML}$ -formulae under the classical $\mathrm{FO}$ -connectives $\neg $ , $\wedge $ and $\vee $ .

Proof. For first-order $\psi (\lambda )$ in a free variable $\lambda $ of the second sort, let

$$ \begin{align*} \psi^{\downarrow}(\lambda) := \forall\mu\bigl(\mu\subseteq\lambda\rightarrow\psi(\mu)\bigr), \end{align*} $$

where $\mu \subseteq \lambda $ stands for the natural rendering in our $2$ -sorted first-order framework, which is literally adequate in inquisitive closures of state-pointed relational pseudo-models. Then $\psi $ is persistent if, and only if, $\psi \equiv \psi ^{\downarrow }$ over this class. It is easy to check that $\downarrow $ commutes with conjunction in the sense that

$$ \begin{align*} (\psi_1 \wedge \psi_2)^{\downarrow}(\lambda) \equiv \psi_1^{\downarrow}(\lambda) \wedge \psi_2^{\downarrow}(\lambda). \end{align*} $$

Consider now a persistent formula $\psi (\lambda )$ that is a boolean combination of standard translations, w.l.o.g. in conjunctive normal form. As $\downarrow $ commutes with conjunction, it suffices to show that the $\downarrow $ -version of each conjunct of the conjunctive normal form satisfies the claim of the lemma. And as the standard translation commutes with conjunction and disjunction (i.e. in $\mathrm{InqML}$ vs. $\vee $ in $\mathrm{FO}$ ), it suffices to prove expressibility of $\psi ^{\downarrow }$ as a standard translation of an $\mathrm{InqML}$ -formula for a simple disjunction of the form

$$ \begin{align*} \psi(\lambda)= \neg \varphi_1^{\ast}(\lambda) \vee \varphi_2^{\ast}(\lambda) \end{align*} $$

for $\varphi _1,\varphi _2 \in \mathrm{InqML}$ with standard translations $\varphi _i^{\ast }(\lambda )$ . We here think of $\varphi _1$ as a (possibly empty) conjunction and of $\varphi _2$ as a (possibly empty) disjunction. The degenerate cases, in which $\psi $ has trivial positive or negative contributions, correspond to (classical) $\bot $ or $\top $ in the places of $\varphi _2^{\ast }$ or $\varphi _1^{\ast }$ , respectively. And as classical $\bot $ agrees with the standard translation of inquisitive $\bot $ only for non-empty states, it is important that we aim for equivalence w.r.t. non-empty states only. But in all those scenarios we find that $\psi ^{\downarrow }(\lambda )$ is equivalent to the standard translation of the inquisitive implication $\varphi _1 \rightarrow \varphi _2 \in \mathrm{InqML}$ :

$$ \begin{align*} \psi^{\downarrow}(\lambda)\equiv (\varphi_1 \rightarrow \varphi_2)^{\ast}(\lambda) \end{align*} $$

over the class of inquisitive closures of state-pointed relational pseudo-models with non-empty distinguished states.

Proof. As in the proof of Corollary 5.8, the implication (ii) $\Rightarrow $ (i) is obvious, and we argue indirectly for (i) $\Rightarrow $ (ii): we show that, if $\varphi $ is not equivalent, w.r.t. non-empty information states, to any boolean combination of $\mathrm{InqML}$ -formulae then it cannot satisfy the preservation and invariance conditions in (i). This then implies (ii) with Lemma 5.10. The crucial claim for that is the following. If $\varphi (\lambda )$ is not equivalent to any boolean combination of standard translations of $\mathrm{InqML}$ -formulae, then there is a set $\Psi = \Psi (\lambda )$ of first-order formulae in the single free variable $\lambda $ of the second sort, such that

1. (a) for all standard translations $\psi (\lambda )$ of $\mathrm{InqML}$ -formulae, either $\psi \in \Psi $ or ${\neg \psi \in \Psi }$ ,

2. (b) $\Psi \cup \{ \varphi \}$ and $\Psi \cup \{ \neg \varphi \}$ are both satisfiable by non-empty information states in relational pseudo-models.

Condition (a) says that $\Psi $ is “complete” w.r.t. the set of all standard translations of $\mathrm{InqML}$ -formulae; (b) guarantees that there are $\omega $ -saturated relational pseudo-models $\mathscr {M},s$ and $\mathscr {M}',s'$ (models of $\Psi $ with states $s,s'$ that are represented) such that $\mathscr {M},s \equiv _{\mathrm{InqML}} \mathscr {M}',s'$ , whence also $(\mathscr {M},s)\!\downarrow ,s \equiv _{\mathrm{InqML}} (\mathscr {M}',s')\!\downarrow ,s'$ , but $\mathscr {M},s \models \varphi $ while $\mathscr {M}',s' \models \neg \varphi $ . This contradicts the preservation and invariance as stated in (i): preservation of $\varphi $ and $\neg \varphi $ under passage to closures implies $(\mathscr {M},s)\!\downarrow ,s \models \varphi $ and $(\mathscr {M}',s')\!\downarrow ,s' \models \neg \varphi $ . Moreover, $\mathscr {M},s \equiv _{\mathrm{InqML}} \mathscr {M}',s'$ implies $(\mathscr {M},s)\!\downarrow ,s \sim (\mathscr {M}',s')\!\downarrow ,s'$ with Remark 5.4 and Corollary 5.6; but this contradicts preservation of $\varphi $ under inquisitive bisimulation.

The set $\Psi $ is obtained by a compactness argument, which is more involved than the analogue used in the world-pointed case of Corollary 5.8. The present argument crucially involves the additional persistency assumption in (i). Assuming w.l.o.g. a finite signature we may enumerate all standard translations of $\mathrm{InqML}$ -formulae as $(\psi _i(\lambda ))_{i \in \mathbb {N}}$ , and obtain the desired $\Psi $ as the union of a chain of finite sets $\Psi _i$ as follows. Starting from $\Psi _0 := \emptyset $ we inductively augment $\Psi _i$ by either $\psi _i$ or $\neg \psi _i$ to obtain $\Psi _{i+1}$ . In the inductive process we maintain, as an invariant, the condition that for all boolean combinations of standard translations $\psi (\lambda )$ of $\mathrm{InqML}$ -formulae, and over the elementary class of all state-pointed relational pseudo-models with a non-empty distinguished information state,Footnote ¹⁰

$$ \begin{align*} (\ast) \quad \Psi_i(\lambda) \not\models \varphi(\lambda) \leftrightarrow \psi(\lambda), \end{align*} $$

i.e. that $\varphi $ remains inequivalent to all boolean combinations of standard translations over the class of all state-pointed relational pseudo-models of $\Psi _i$ with non-empty distinguished state. Then $\Psi = \bigcup _i \Psi _i$ meets requirements (a) and (b); indeed, with compactness, (b) is covered by $(\ast )$ for (the standard translations of) $\bot $ or $\top $ in the rôle of $\psi $ . If $\Psi \cup \{ \varphi \}$ were not satisfiable in a non-empty information state, then $\Psi (\lambda ) \models \varphi (\lambda ) \leftrightarrow \bot $ over the class of relational pseudo-models with non-empty information states (and over this class, classical $\bot $ is equivalent to the standard translation of inquisitive $\bot $ ); similarly for $\Psi \cup \{ \neg \varphi \}$ and equivalence with $\top $ .

The initial set $\Psi _0 = \emptyset $ satisfies condition $(\ast )$ by assumption. It remains to argue that $(\ast )$ can be maintained in at least one of the augmentations $\Psi _i \cup \{ \psi _i \}$ or $\Psi _i \cup \{ \neg \psi _i \}$ . Assume this were not the case, i.e. that, for some boolean combinations $\xi _0,\xi _1$ of standard translations of $\mathrm{InqML}$ -formulae,

$$ \begin{align*} \Psi_i \cup \{ \psi_i \} \models \varphi \leftrightarrow \xi_0 \quad \mbox{ and } \quad \Psi_i \cup \{ \neg \psi_i \} \models \varphi \leftrightarrow \xi_1. \end{align*} $$

But then

$$ \begin{align*} \Psi_i \models \varphi \leftrightarrow \bigl((\psi_i \wedge \xi_0) \vee (\neg \psi_i \wedge \xi_1) \bigr) \end{align*} $$

contradicts the assumption that $(\ast )$ was satisfied in the previous step.