Uniform Lyndon interpolation for the pure logic of necessitation with a modal reduction principle
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912540349431808 |
|---|---|
| author | Sato, Yuta |
| author_facet | Sato, Yuta |
| contents | 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 φ\to \Box^m φ$, $\Diamond$-free modal reduction principle, together with a rule $\frac{\neg \Box φ}{\neg \Box \Box φ}$, 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 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{Cl}$, proving ULIP as a corollary. We also prove ULIP of $\mathbf{NA}_{m,n} = \mathbf{N} + \Box^n φ\to \Box^m φ$ and $\mathbf{NRA}_{m,n} = \mathbf{N} + \Box^n φ\to \Box^m φ+ \frac{\neg φ}{\neg \Box φ}$ in the same manner. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_10176 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Uniform Lyndon interpolation for the pure logic of necessitation with a modal reduction principle Sato, Yuta Logic 03B45, 03C40, 03F05 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 φ\to \Box^m φ$, $\Diamond$-free modal reduction principle, together with a rule $\frac{\neg \Box φ}{\neg \Box \Box φ}$, 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 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{Cl}$, proving ULIP as a corollary. We also prove ULIP of $\mathbf{NA}_{m,n} = \mathbf{N} + \Box^n φ\to \Box^m φ$ and $\mathbf{NRA}_{m,n} = \mathbf{N} + \Box^n φ\to \Box^m φ+ \frac{\neg φ}{\neg \Box φ}$ in the same manner. |
| title | Uniform Lyndon interpolation for the pure logic of necessitation with a modal reduction principle |
| topic | Logic 03B45, 03C40, 03F05 |
| url | https://arxiv.org/abs/2503.10176 |