Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability
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_ | 1866915980329877504 |
|---|---|
| author | Lyon, Tim S. |
| author_facet | Lyon, Tim S. |
| contents | We introduce and study single-conclusioned nested sequent calculi for a broad class of intuitionistic multi-modal logics known as "intuitionistic grammar logics (IGLs)." These logics serve as the intuitionistic counterparts of classical grammar logics, and subsume standard intuitionistic modal and tense logics, including IK and IKt extended with combinations of the T, B, 4, 5, and D axioms. We analyze fundamental invertibility and admissibility properties of our calculi and introduce a novel structural rule, called the "shift rule," which unifies standard structural rules arising from modal frame conditions into a single rule. This rule enables a purely syntactic proof of cut-admissibility that is uniform over all IGLs, and yields completeness of our nested calculi as a corollary. Finally, we define a negative translation that constitutes a faithful embedding of classical grammar logics (CGLs) into IGLs, witnessed by proof transformations between multi-conclusioned and single-conclusioned nested sequent proofs for CGLs and IGLs, respectively. This reduces the general validity problem for CGLs to that of IGLs. The general validity problem over a class C of logics asks: given a logic L in C and a formula A, is A valid in L? As this problem is known to be undecidable for CGLs, our reduction implies its undecidability for IGLs as well. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_22174 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability Lyon, Tim S. Logic in Computer Science Logic 03B44, 03B45, 03B55, 03B70, 03C40, 03F03, 03F05 We introduce and study single-conclusioned nested sequent calculi for a broad class of intuitionistic multi-modal logics known as "intuitionistic grammar logics (IGLs)." These logics serve as the intuitionistic counterparts of classical grammar logics, and subsume standard intuitionistic modal and tense logics, including IK and IKt extended with combinations of the T, B, 4, 5, and D axioms. We analyze fundamental invertibility and admissibility properties of our calculi and introduce a novel structural rule, called the "shift rule," which unifies standard structural rules arising from modal frame conditions into a single rule. This rule enables a purely syntactic proof of cut-admissibility that is uniform over all IGLs, and yields completeness of our nested calculi as a corollary. Finally, we define a negative translation that constitutes a faithful embedding of classical grammar logics (CGLs) into IGLs, witnessed by proof transformations between multi-conclusioned and single-conclusioned nested sequent proofs for CGLs and IGLs, respectively. This reduces the general validity problem for CGLs to that of IGLs. The general validity problem over a class C of logics asks: given a logic L in C and a formula A, is A valid in L? As this problem is known to be undecidable for CGLs, our reduction implies its undecidability for IGLs as well. |
| title | Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability |
| topic | Logic in Computer Science Logic 03B44, 03B45, 03B55, 03B70, 03C40, 03F03, 03F05 |
| url | https://arxiv.org/abs/2511.22174 |