Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation

TL;DR

The paper develops single-conclusion nested sequent calculi for intuitionistic grammar logics (IGLs), introducing a unifying shift rule to encapsulate IPA frame conditions and delivering a purely syntactic cut-elimination argument applicable across IGLs. It also provides a novel interpolation framework based on single-conclusion nested proofs, establishing Lyndon interpolation and Beth definability for IGLs and their intuitionistic modal/tense fragments. These results connect proof theory with definability and interpolation in a broad intuitionistic multi-modal setting, and yield constructive methods for generating interpolants and explicit definitions. The work advances analytic proof theory for IGLs and lays groundwork for further exploration of decidability, invertibility, and potential lattice of extensions via labeled systems or translations.

Abstract

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 an interpolation algorithm that operates over single-conclusioned nested sequent proofs. This gives constructive proofs of both the Lyndon interpolation property (LIP) and Beth definability property (BDP) for all IGLs and for all intuitionistic modal and tense logics they subsume. To the best of the author's knowledge, this style of interpolation algorithm (that acts on single-conclusioned nested sequent proofs) and the resulting LIP and BDP results are new.

Figures (5)

• Figure 1: Depictions of the (F1) and (F2) conditions imposed on models. Dotted arrows indicate the relations implied by the presence of the solid arrows.
• Figure 2: The nested sequent system $\mathsf{NIK_{m}}(\mathcal{A})$ defined relative to the set $\mathcal{A}$ of axioms. Note that $\mathsf{d}_{x} \in \mathsf{NIK_{m}}(\mathcal{A})$iff$\mathrm{D}_{x} \in \mathcal{A}$.
• Figure 3: A diagram depicting which hp-admissibility (and hp-invertibility) results are sufficient to prove others. An arrow from one rule name to another indicates that the hp-admissibility of the source rule is sufficient to prove the hp-admissibility of the target rule. Note that 'Lem. \ref{['lem:hp-inver']}' indicates the hp-invertibility of certain rules in $\mathsf{NIK_{m}}(\mathcal{A})$.
• Figure 4: Height-preserving admissible rules in $\mathsf{NIK_{m}}(\mathcal{A})$.
• Figure 5: Some interpolation rules.

Theorems & Definitions (58)

• Definition 2.1: Frame
• Definition 2.2: Model
• Remark 2.3
• Definition 2.4: Semantic Clauses
• Lemma 2.5: General Monotonicity
• proof
• Definition 2.6: Axiom System $\mathsf{H}\mathsf{IK_{m}}$
• Remark 2.7
• Definition 2.8: $\mathsf{H}\mathsf{IK_{m}}(\mathcal{A})$
• Remark 2.9