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

TL;DR

This paper develops a proof-theoretic method to establish the uniform interpolation property in multi-agent modal logics, providing a syntactic algorithm and avoiding second-order quantifiers.

Contribution

It extends proof-theoretic techniques to multi-agent modal logics, offering a new syntactic algorithm for uniform interpolants and modeling quantification.

Findings

Established UIP in multi-agent modal logics $ extbf{K_n}$, $ extbf{KD_n}$, $ extbf{KT_n}$

Presented a purely syntactic algorithm for uniform interpolants

Showed quantification over propositional variables via UIP

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\'ilkov\'a (2007) develops the method in Pitts (1992) to show UIP in classical modal logic $\mathbf{K}$ and $\mathbf{KT}$. This paper further extends B\'ilkov\'a (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.