A proof-theoretic approach to uniform interpolation property of multi-agent modal logic
Youan Su
TL;DR
This work delivers a purely proof-theoretic treatment of the uniform interpolation property in multi-agent modal logics $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$ by extending Bilkova’s method to the multi-modal setting. It defines sequent calculi $\mathsf{G}(\mathbf{K_n})$, $\mathsf{G}(\mathbf{KD_n})$, and a loop-checked $\mathsf{G}(\mathbf{KT_n^+})$ to establish UIP syntactically, and provides an algorithmic construction of uniform interpolants via the $\mathcal{A}_p(\cdot)$ formulas. The paper also shows how quantification over propositional variables can be modeled by UIP through a translation between second-order and first-order propositional calculi, yielding a direct method that avoids second-order quantifiers. These results advance forgetting and interpolation in multi-agent epistemic logics, with potential extensions to intuitionistic and distributed knowledge frameworks and agent-counting considerations.
Abstract
Uniform interpolation property (UIP) is a strengthening of Craig interpolation property. It was first established by Pitts(1992) based on a pure proof-theoretic method. UIP in multi-modal $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$ logic have been established by semantic approaches, however, a proof-theoretic approach is still lacking. Bílková (2007) develops the method in Pitts (1992) to show UIP in classical modal logic $\mathbf{K}$ and $\mathbf{KT}$. This paper further extends Bílková (2007)'s systems to establish the UIP in multi-agent modal logic $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$. A purely syntactic algorithm is presented to determine a uniform interpolant formula. It is also shown that quantification over propositional variables can be modeled by UIP in these systems. Furthermore, a direct argument to establish UIP without using second-order quantifiers is also presented.