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的开创性工作基于一种朴素后向证明搜索可终止的矢列演算，为直觉主义命题逻辑建立了这一性质。这一构造性方法已被广泛应用于包括直觉主义模态逻辑在内的多种逻辑系统。令人惊讶的是，迄今尚未有任何具有独立盒算子与钻石算子的直觉主义模态逻辑被证明满足均匀插值性质。我们通过证明构造性K系统（CK）与Wijesekera的K系统（WK）满足均匀插值性质，填补了这一空白。我们基于Pitts的技术，利用CK与WK已有的可终止演算系统（我们证明了这些系统可消除切割规则），并将所有结果在证明辅助工具Rocq中形式化。综合而言，我们的成果构成了对带有钻石算子的直觉主义模态逻辑的首个正向均匀插值结果。