On the expressive power of inquisitive epistemic logic

TL;DR

The paper establishes a van Benthem–Rosen style expressiveness result for inquisitive epistemic logic (InqML) by showing that InqML is exactly the bisimulation-invariant fragment of first-order logic over natural two-sorted encodings of inquisitive epistemic models. The authors develop a non-classical, model-theoretic analysis that combines inquisitive bisimulation, relational encodings, Gaifman locality, and MSO/FO techniques to handle the non-elementary nature of the model classes. A central contribution is the upgrading mechanism: from ∼^n equivalence to ∼-invariance, via locally tree-like exploded views and suitable bisimilar companions that are rich, regular, and acyclic, enabling FO-definability to be captured by InqML. The results hold for both world- and state-pointed properties, and extend to finite models and locally full encodings, highlighting InqML as expressively complete for bisimulation-invariant FO properties in this setting. These findings bridge non-classical modal logics with classical model theory, offering a precise, algebraic understanding of the expressive reach of inquisitive epistemic logic.

Abstract

Inquisitive modal logic, InqML, in its epistemic incarnation, extends standard epistemic logic to capture not just the information that agents have, but also the questions that they are interested in. We use the natural notion of bisimulation equivalence in the setting of InqML, as introduced in [Ciardelli/Otto: JSL 2021], to characterise the expressiveness of InqML as the bisimulation invariant fragment of first-order logic over natural classes of two-sorted first-order structures that arise as relational encodings of inquisitive epistemic (S5-like) models. The non-elementary nature of these classes crucially requires non-classical model-theoretic methods for the analysis of first-order expressiveness, irrespective of whether we aim for characterisations in the sense of classical or of finite model theory.

Figures (6)

• Figure 1: Generic upgrading patterns.
• Figure 2: Upgrading patterns for relational epistemic models.
• 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 \subseteq \alpha$ (as part of the representation of the $a$-local structure ${\mathfrak{M}}\!\restriction\![w]_a$) and the full set $\alpha' \subseteq \alpha'$ (as part of the representation of the $a'$-local structure ${\mathfrak{M}}\!\restriction\![w]_{a'}$).
• Figure 4: Upgrading for relational epistemic models, refined by Proposition \ref{['Gaifmanprop']}.
• Figure 5: Subdivison of $[w]_a= \sigma_a(w)$ in the local $a$-structure ${\mathbb M}\!\restriction\![w]_a$ for an inquisitive assignment $\Pi = \Sigma_a(w)$ that is $\kappa$-regular at granularity $m$, where $\rho_m(\Pi \setminus \emptyset) = \{ \alpha_1,\alpha_2,\ldots, \alpha_n \}$, $\kappa = \{ 1,2, \ldots \}$ and each one of the contributions $s(\alpha_j,i)$ in block $B_i$ is one $\subseteq$-maximal element in $\Pi$, so that there are precisley $\kappa$ many such for each available ${\sim^m}$-type of nonempty information states in $\Pi$.

Theorems & Definitions (39)

• Theorem 1.1: CiardelliOttoJSL2021
• Theorem 1.2: main theorem
• Definition 2.1
• Definition 2.2
• Proposition 2.3
• Definition 2.4
• Definition 2.5
• Proposition 2.6
• Definition 2.7
• Definition 2.8