Uniform Lyndon interpolation for the pure logic of necessitation with a modal reduction principle

Abstract We prove the uniform Lyndon interpolation property (ULIP) of some extensions of the pure logic of necessitation $\mathbf{N}$. For any $m, n \in \mathbb{N}$, $\mathbf{N}^{+}\mathbf{A}_{m,n}$ is the logic obtained from $\mathbf{N}$ by adding a single axiom $\Box ^{n} \varphi \to \Box ^{m} \varphi $, $\Diamond $-free modal reduction principle, together with a rule $\frac{\neg \Box \varphi }{\neg \Box \Box \varphi }$, required to make the logic complete with respect to its Kripke-like semantics. We first introduce a sequent calculus $\mathbf{GN}^{+}\mathbf{A}_{m,n}$ for $\mathbf{N}^{+}\mathbf{A}_{m,n}$ and show that it enjoys cut elimination, proving Craig and Lyndon interpolation properties as consequences. We then introduce a general method, called propositionalization, that allows one to prove ULIP of a logic by reducing it to that of some weaker logic. Lastly, we construct a propositionalization of $\mathbf{N}^{+}\mathbf{A}_{m,n}$ into classical propositional logic $\mathbf{Cl}$, proving ULIP as a corollary. We also prove ULIP of $\mathbf{NA}_{m,n} = \mathbf{N} + \Box ^{n} \varphi \to \Box ^{m} \varphi $ and $\mathbf{NRA}_{m,n} = \mathbf{N} + \Box ^{n} \varphi \to \Box ^{m} \varphi + \frac{\neg \varphi }{\neg \Box \varphi }$ in the same manner.