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

2025/03/13 by Y. Sato, Sato, Yuta
Computer Science · #Logic, Reasoning, and Knowledge #Advanced Algebra and Logic #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2503.10176

Abstract

We prove the uniform Lyndon interpolation property (ULIP) of some extensions of the pure logic of necessitation N. For any m, n ∈ ℕ, N⁺A_m,n is the logic obtained from N by adding a single axiom \Boxⁿ φ→ \Box^m φ, \Diamond-free modal reduction principle, together with a rule (¬ \Box φ)/(¬ \Box \Box φ), required to make the logic complete with respect to its Kripke-like semantics. We first introduce a sequent calculus GN⁺A_m,n for N⁺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 N⁺A_m,n into classical propositional logic Cl, proving ULIP as a corollary. We also prove ULIP of NA_m,n = N + \Boxⁿ φ→ \Box^m φ and NRA_m,n = N + \Boxⁿ φ→ \Box^m φ+ (¬ φ)/(¬ \Box φ) in the same manner.

Related

• Uniform Lyndon interpolation property in propositional modal logics
• Uniform Lyndon interpolation for intuitionistic monotone modal logic
• Lyndon interpolation property for extensions of S4 and intermediate propositional logics
• Uniform Lyndon Interpolation for Basic Non-normal Modal and Conditional Logics
• Interpolation via Generalized Splitting