Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM

TL;DR

This paper extends Pitts' uniform interpolation technique to the intuitionistic modal logic KM using a new multi-succedent sequent calculus, proving key properties and mechanising the results in Rocq.

Contribution

It introduces a novel terminating multi-succedent calculus for KM and adapts Pitts' technique to construct uniform interpolants, with mechanised correctness proofs.

Findings

Successfully constructed uniform interpolants for KM

Proved the calculus terminates and is cut-free

Mechanised proofs in Rocq ensure correctness

Abstract

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.