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ïve 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.

翻译：均匀插值是一种强形式的插值性质，它为命题逻辑中命题量词的解释提供了框架。Pitts的开创性工作基于一种朴素反向证明搜索终止的矢列演算，确立了直觉主义命题逻辑的这一性质。这种构造性方法已被推广到包括直觉主义模态逻辑在内的广泛逻辑体系。令人惊讶的是，目前尚未有包含独立box和diamond算子的直觉主义模态逻辑被证明满足均匀插值。我们通过证明构造性K逻辑（CK）和Wijesekera的K逻辑（WK）的均匀插值性质填补了这一空白。我们基于Pitts的技术方法，利用CK和WK已有的终止演算——我们证明了这些演算满足切消定理——并在证明助手Rocq中形式化了所有结果。综合而言，我们的成果构成了首个关于包含diamond算子的直觉主义模态逻辑的正面均匀插值结果。