Uniform Interpolation in Distributed Knowledge Modal Logics

TL;DR

This paper establishes the uniform interpolation property for various distributed knowledge modal logics, enhancing understanding of collective reasoning and information hiding in multi-agent systems.

Contribution

It extends the canonical-formula and literal-elimination framework to distributed knowledge logics and proves uniform interpolation for multiple systems, including transitive and Euclidean variants.

Findings

Uniform interpolants for distributed knowledge logics are characterized as remainders of eliminating atoms.

Every formula of modal depth k+1 has a uniform interpolant of modal depth 2k+1.

Uniform interpolation holds for six key 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 $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.