Uniform interpolation with constructive diamond

TL;DR

This paper proves uniform interpolation for certain intuitionistic modal logics with diamond, filling a gap in the understanding of their logical properties using constructive proof techniques.

Contribution

It establishes uniform interpolation for Constructive K and Wijesekera's K, the first such results for intuitionistic modal logics with diamond, using cut-elimination and formal proof in Rocq.

Findings

Proved uniform interpolation for CK and WK logics.

Built on existing terminating calculi and formalized results in Rocq.

First positive uniform interpolation results for intuitionistic modal logics with diamond.

Abstract

Uniform interpolation is a strong form of interpolation providing an interpretation of propositional quantifiers within a propositional logic. Pitts' seminal work establishes this property for intuitionistic propositional logic relying on a sequent calculus in which na\"ive backward proof-search terminates. This constructive approach has been adapted to a wide range of logics, including intuitionistic modal logics. Surprisingly, no intuitionistic modal logic with independent box and diamond has yet been shown to satisfy uniform interpolation. We fill in this gap by proving the uniform interpolation property for Constructive K (CK) and Wijesekera's K (WK). We build on Pitts' technique by exploiting existing terminating calculi for CK and WK, which we prove to eliminate cut, and formalise all our results in the proof assistant Rocq. Together, our results constitute the first positive uniform interpolation results for intuitionistic modal logics with diamond.