Universal proof theory: Semi-analytic rules and uniform interpolation

In Craig, we introduced a syntactically defined and highly general class of calculi known as semi-analytic. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including FLₑ, FL₄ₖ, CFLₑ, CFL₄ₖ, and their K, D, and T-type modal extensions, as well as CPC, K, and KD. However, its more striking consequence lies in the negative direction. It extends the negative results of Craig to logics with CIP but without UIP. In particular, it shows that the modal logics K4 and S4 do not have a terminating semi-analytic calculus. keywords: Uniform interpolation, Sequent calculi, Substructural logics, Modal logics, Subexponential modalities