论文标题
直觉单调逻辑的统一林登插值
Uniform Lyndon interpolation for intuitionistic monotone modal logic
论文作者
论文摘要
在本文中，我们表明直觉单调模态逻辑$ \ mathsf {im} $具有统一的Lyndon插值属性（ULIP）。逻辑$ \ mathsf {im} $是直觉上的非正态模态逻辑，并且属性ULIP是加强插值的增强，其中插值仅依赖于前提或结论的含义，尊重命题变量的极性。我们证明ULIP的方法可产生显式统一的插值，并利用我们为此目的开发的$ \ Mathsf {imsf {im} $的终止序列微积分。据我们所知，$ \ Mathsf {im} $具有ulip的结果，终止顺序的微积分是直觉非正态模态逻辑的第一个结果。但是，我们的目的不是证明这些特定的结果，而是展示我们用于证明ULIP的建设性证明理论方法的灵活性。它是在过去几年中开发的，已应用于子结构，中间，经典（非）正常模态和直觉正常模态逻辑。鉴于这些结果，直觉的非正态模态逻辑似乎是一个自然的下一阶级，可以将方法应用于，我们在本文中朝着该方向迈出了第一步。
In this paper we show that the intuitionistic monotone modal logic $\mathsf{iM}$ has the uniform Lyndon interpolation property (ULIP). The logic $\mathsf{iM}$ is a non-normal modal logic on an intuitionistic basis, and the property ULIP is a strengthening of interpolation in which the interpolant depends only on the premise or the conclusion of an implication, respecting the polarities of the propositional variables. Our method to prove ULIP yields explicit uniform interpolants and makes use of a terminating sequent calculus for $\mathsf{iM}$ that we have developed for this purpose. As far as we know, the results that $\mathsf{iM}$ has ULIP and a terminating sequent calculus are the first of their kind for an intuitionistic non-normal modal logic. However, rather than proving these particular results, our aim is to show the flexibility of the constructive proof-theoretic method that we use for proving ULIP. It has been developed over the last few years and has been applied to substructural, intermediate, classical (non-)normal modal and intuitionistic normal modal logics. In light of these results, intuitionistic non-normal modal logics seem a natural next class to try to apply the method to, and we take the first step in that direction in this paper.
