Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Uniform Interpolation in Distributed Knowledge Modal Logics

Kexu Wang, Liangda Fang

Abstract

Uniform interpolation is the property that, for any formula and set of atoms, there exists the strongest consequence omitting those atoms. It plays a central role in knowledge representation and reasoning tasks such as knowledge update and information hiding. This paper studies the uniform interpolation property in epistemic modal logics with distributed knowledge, which captures agents' collective reasoning abilities. Building on the bisimulation-quantifier perspective, we extend the canonical-formula and literal-elimination framework of Fang, Liu, and van Ditmarsch to distributed knowledge settings and introduce the concept of collective $p$-bisimulation. We show that, for distributed knowledge modal logics $\mathsf{K}_n\mathbf{D}$, $\mathsf{D}_n\mathbf{D}$, and $\mathsf{T}_n\mathbf{D}$, every satisfiable canonical formula's uniform interpolant omitting an atom $p$ is exactly its remainder of eliminating $p$. Then, we provide a finer analysis for the transitive and Euclidean systems $\mathsf{K45}_n\mathbf{D}$, $\mathsf{KD45}_n\mathbf{D}$, and $\mathsf{S5}_n\mathbf{D}$, and prove that every formula of modal depth $k + 1$ has a uniform interpolant of modal depth $2 k + 1$. Thus, we prove the uniform interpolation property in all the six distributed knowledge modal logics. Finally, we generalize the results to some variants with propositional common knowledge and discuss the method's limitations.

Uniform Interpolation in Distributed Knowledge Modal Logics

Abstract

Uniform interpolation is the property that, for any formula and set of atoms, there exists the strongest consequence omitting those atoms. It plays a central role in knowledge representation and reasoning tasks such as knowledge update and information hiding. This paper studies the uniform interpolation property in epistemic modal logics with distributed knowledge, which captures agents' collective reasoning abilities. Building on the bisimulation-quantifier perspective, we extend the canonical-formula and literal-elimination framework of Fang, Liu, and van Ditmarsch to distributed knowledge settings and introduce the concept of collective -bisimulation. We show that, for distributed knowledge modal logics , , and , every satisfiable canonical formula's uniform interpolant omitting an atom is exactly its remainder of eliminating . Then, we provide a finer analysis for the transitive and Euclidean systems , , and , and prove that every formula of modal depth has a uniform interpolant of modal depth . Thus, we prove the uniform interpolation property in all the six distributed knowledge modal logics. Finally, we generalize the results to some variants with propositional common knowledge and discuss the method's limitations.

Paper Structure

This paper contains 18 sections, 80 theorems, 57 equations, 16 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Uniform Interpolation and Syntactic Methods
  4. Uniform interpolation, bisimulation, and forgetting
  5. d-canonical formulas and pruning
  6. Forgetting as literal elimination
  7. Uniform Interpolation in $\textsf{K}_n \textbf{D}$, $\textsf{KD}_n \textbf{D}$, and $\textsf{T}_n \textbf{D}$
  8. Uniform Interpolation in $\textsf{K45}_n \textbf{D}$, $\textsf{KD45}_n \textbf{D}$, and $\textsf{S5}_n \textbf{D}$
  9. $\delta^p$ may not be the uniform interpolant
  10. Uniform interpolation in $\textsf{K45}_n \textbf{D}$, $\textsf{KD45}_n \textbf{D}$
  11. Uniform interpolation in $\textsf{S5}_n \textbf{D}$
  12. Special cases where $\delta^p$ is a uniform interpolant
  13. Uniform Interpolation in Propositional Common Knowledge
  14. Uniform interpolation in $\textsf{K}_n\textbf{DPC}$, $\textsf{D}_n\textbf{DPC}$, $\textsf{T}_n\textbf{DPC}$
  15. Uniform interpolation in $\textsf{S5}_n\textbf{DPC}$
  16. ...and 3 more sections

Key Result

Lemma 3.2

Let $(M, s)$ and $(M', s')$ be two models, $p \in \mathcal{P}$, and $\phi$ be any $\mathcal{L}^{\textbf{D}}_{\textbf{C}}$ formula without $p$ occurring. If $(M, s) \mathrel{\raisebox{0.2ex}{$\underline{\leftrightarrow}$}}^{col}_p (M', s')$, then $M, s \vDash \phi \Longleftrightarrow M', s' \vDash \p

Figures (16)

  • Figure 1: Pruning
  • Figure 2: Inductive step in Lemma \ref{['lem: KandD']}
  • Figure 4: Step 1 of Lemma \ref{['lem: ConstructionK45']}
  • Figure 5: Step 2 of the base case of Lemma \ref{['lem: ConstructionK45']}
  • Figure 6: Step 3 of Lemma \ref{['lem: ConstructionK45']}
  • ...and 11 more figures

Theorems & Definitions (153)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 3.1: Uniform Interpolation
  • Definition 3.2: Collective $p$-Bisimulation
  • Lemma 3.2: the Adequacy Lemma of Collective $p$-Bisimulation
  • Definition 3.3: Forgetting
  • Proposition 3.3
  • Definition 3.4
  • Proposition 3.4
  • ...and 143 more