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

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 ${\mathrm{\square }}^n\phi \to {\mathrm{\square }}^m\phi$, $\mathrm{◊}$-free modal reduction principle, together with a rule $\frac{\mathrm{\neg }\mathrm{\square }\phi }{\mathrm{\neg }\mathrm{\square }\mathrm{\square }\phi }$, required to make the logic complete with respect to its Kripke-like semantics. We first introduce a sequent calculus ${\mathbf{G}\mathbf{N}}^{+}{\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 a consequence. We then introduce a general method, called propositionalization, that enables one to reduce ULIP of a logic to some weaker logic. Lastly, we construct a propositionalization of ${\mathbf{N}}^{+}{\mathbf{A}}_{m,n}$ into classical propositional logic $\mathbf{C}\mathbf{l}$, proving ULIP as a corollary. We also prove ULIP of ${\mathbf{N}\mathbf{A}}_{m,n}=\mathbf{N}+{\mathrm{\square }}^n\phi \to {\mathrm{\square }}^m\phi$ and ${\mathbf{N}\mathbf{R}\mathbf{A}}_{m,n}=\mathbf{N}+{\mathrm{\square }}^n\phi \to {\mathrm{\square }}^m\phi +\frac{\mathrm{\neg }\phi }{\mathrm{\neg }\mathrm{\square }\phi }$ in the same manner.