Uniform Agent-interpolation of Distributed Knowledge

TL;DR

This paper proves the uniform interpolation property for certain epistemic logics with distributed knowledge, providing a syntactic algorithm for constructing interpolants that include agent symbols.

Contribution

It extends sequent calculi for epistemic logic to establish uniform interpolation for logics K, KD, and KT with distributed knowledge, including a syntactic construction method.

Findings

Proves uniform interpolation for epistemic logics K, KD, and KT with distributed knowledge.

Develops a syntactic algorithm for constructing interpolants including agent symbols.

Extends existing sequent calculi to support uniform interpolation in these logics.

Abstract

Uniform interpolation property (UIP) is a strengthening of Craig interpolation property. It can be understood as the definability of propositional quantifiers. This paper develops the sequent calculi provided in Murai and Sano (2020), combining with the methods studied by B{\'\i}lkov{\'a} (2007) to show the uniform interpolation for epistemic logic $\mathbf{K}$, $\mathbf{KD}$ and $\mathbf{KT}$ with distributed knowledge. A purely syntactic algorithm is presented to determine a uniform interpolant formula. In the definition of an interpolant formula, not only propositional variables but also agent symbols are taken into consideration.