Uniform interpolation via nested sequents and hypersequents

TL;DR

This paper introduces a constructive proof-theoretic method for establishing uniform interpolation in modal logics using nested sequents and hypersequents, providing new proofs for several modal systems including S5.

Contribution

It develops a novel, constructive approach to uniform interpolation via nested sequents and hypersequents, extending proof-theoretic techniques to new modal logics.

Findings

Reproved uniform interpolation for K, D, T logics

First direct proof of uniform interpolation for S5

Method combines proof-theoretic and semantic notions

Abstract

A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents and apply it to reprove the uniform interpolation property for normal modal logics $\mathsf{K}$, $\mathsf{D}$, and $\mathsf{T}$. We then use the know-how developed for nested sequents to apply the same method to hypersequents and obtain the first direct proof of uniform interpolation for $\mathsf{S5}$ via a cut-free sequent-like calculus. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents and hypersequents also uses semantic notions, including bisimulation modulo an atomic proposition.