Modal Logic for Simulation, Refinement, and Mutual Ignorance

TL;DR

The paper develops a family of logics to formalize information change in multi-agent epistemic settings via refinement (information growth) and simulation (information loss) modalities, anchored by the mutual factual ignorance baseline M^∘. It introduces an origin modality [∘] to capture truth prior to any factual updates and provides modular, reduction-based axiomatizations culminating in ROSML, which combines refinement, simulation, and origin semantics. The authors establish soundness and completeness results for RML, SML, OML, and ROSML through systematic reductions to standard Modal Logic ML, and discuss dualities, semantics, and potential extensions to S5 epistemic frameworks. The work lays groundwork for deeper analysis of dynamic epistemic phenomena and invites future exploration of complexity, alternative model classes, and richer update mechanisms.

Abstract

Simulation and refinement are variations of the bisimulation relation, where in the former we keep only atoms and forth, and in the latter only atoms and back. Quantifying over simulations and refinements captures the effects of information change in a multi-agent system. In the case of quantification over refinements, we are looking at all the ways the agents in a system can become more informed. Similarly, in the case of quantification over simulations, we are dealing with all the ways the agents can become less informed, or in other words, could have been less informed, as we are at liberty how to interpret time in dynamic epistemic logic. While quantification over refinements has been well explored in the literature, quantification over simulations has received considerably less attention. In this paper, we explore the relationship between refinements and simulations. To this end, we also employ the notion of mutual factual ignorance that allows us to capture the state of a model before agents have learnt any factual information. In particular, we consider the extensions of multi-modal logic with the simulation and refinement modalities, as well as modalities for mutual factual ignorance. We provide reduction-based axiomatizations for several of the resulting logics that are built extending one another in a modular fashion.

Figures (2)

• Figure 1: Schematic drawing of an example of $M'$ as in the proof of Proposition \ref{['prop:RMLsoundness']}. In this example, $A=\{a,b\}$, $\Phi_a=\{\varphi_1,\varphi_2\}$ and $\Phi_b=\{\varphi_3,\varphi_4\}$. Dotted lines represent the relation $Z$. The state $s_0'$ has exactly the successors $s_{\varphi_1}', \cdots, s_{\varphi_4}'$, the state $s_0$ has at least the successors $s_{\varphi_1},\cdots, s_{\varphi_4}$ but may have more. Hence $Z$ is a refinement but not, in general, a bisimulation.
• Figure 2: Schematic drawing of an example of $M'$ as in the proof of Proposition \ref{['prop:SMLsoundness']}. Here, we take $A=\{a,b\}$, $\Phi_a=\{\varphi_1,\varphi_2\}$ and $\Phi_b=\{\varphi_3,\varphi_4\}$. For both $s_0$ and $s_0'$, all successors are drawn. In each successor of $s_0$, $\langle \text{\footnotesize{$\rightrightarrows$}} \rangle\varphi_i$ holds for some $i$. Note that the same $\langle \text{\footnotesize{$\rightrightarrows$}} \rangle\varphi_i$ may hold in multiple successors, such as $\langle \text{\footnotesize{$\rightrightarrows$}} \rangle\varphi_1$ in $t_1$ and $t_2$. Each successor of $s_0'$ corresponds either to a successor of $s_0$ or to some $\varphi_i\in \Phi_a^-\cup \Phi_b^-$. Dotted lines represent the relation $Z$. Note that every successor of $s_0$ is $Z$-related to some successor of $s_0'$ but not vice versa, so $Z$ is a simulation but not a bisimulation.

Theorems & Definitions (23)

• Proposition 0
• proof
• Proposition 1
• proof
• Proposition 2
• proof
• Proposition 3
• Proposition 3
• proof
• Proposition 3