A proof-theoretic approach to uniform interpolation property of multi-agent modal logic

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}}_{\mathbf{n}}$, $\mathbf{K}{\mathbf{D}}_{\mathbf{n}}$ and $\mathbf{K}{\mathbf{T}}_{\mathbf{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{K}\mathbf{T}$. This paper further extends Bílková (2007)'s systems to establish the UIP in multi-agent modal logic ${\mathbf{K}}_{\mathbf{n}}$, $\mathbf{K}{\mathbf{D}}_{\mathbf{n}}$ and $\mathbf{K}{\mathbf{T}}_{\mathbf{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.