Uniform Lyndon interpolation for intuitionistic monotone modal logic

zbMATH Open1531.03029arXiv2208.04607MaRDI QIDQ6407380FDOQ6407380

Authors: Amirhossein Akbar Tabatabai, Rosalie Iemhoff, Raheleh Jalali 

Publication date: 9 August 2022

Abstract: In this paper we show that the intuitionistic monotone modal logic $mathsfiM$ has the uniform Lyndon interpolation property (ULIP). The logic $mathsfiM$ 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 $mathsfiM$ that we have developed for this purpose. As far as we know, the results that $mathsfiM$ 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.

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Subsystems of classical logic (including intuitionistic logic) (03B20) Interpolation, preservation, definability (03C40)

This page was built for publication: Uniform Lyndon interpolation for intuitionistic monotone modal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6407380)