Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
This work extends uniform interpolation to a broader class of intuitionistic logics, providing a new method for logics that previously lacked such results.
The authors adapted Pitts' proof-theoretic technique for uniform interpolation to the intuitionistic multi-succedent setting by designing a terminating, cut-free sequent calculus for the modal logic KM, enabling uniform interpolation and proving coherence of KM-algebras, with all results mechanized in Rocq.
Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM, while highlighting the hurdles we overcame. Finally, by (re)proving the algebraisability of KM, we deduce the coherence of the class of KM-algebras. All our results are fully mechanised in the Rocq proof assistant, ensuring correctness and enabling effective computation of interpolants.