Uniform Lyndon interpolation for intuitionistic monotone modal logic

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