Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement

TL;DR

This work develops a uniform framework to study intuitionistic grammar logics by defining their semantics and axiomatizations, then deriving analytic proof systems through structural refinement. By transforming semantics into labeled sequent calculi and refining them with propagation rules, the authors obtain nested sequent calculi that retain essential proof-theoretic properties, enabling conservativity results and undecidability proofs. They identify a decidable simple fragment and outline propagation-rule adaptations, linking the intuitionistic grammar logics to their modal and classical grammar counterparts. The approach provides a systematic method to obtain cut-free, terminating proof systems for a broad class of logics and clarifies their computational boundaries. Overall, the paper advances the proof-theoretic treatment of intuitionistic grammar logics and lays groundwork for further interpolation and decidability discoveries.

Abstract

Intuitionistic grammar logics fuse constructive and multi-modal reasoning while permitting the use of converse modalities, serving as a generalization of standard intuitionistic modal logics. In this paper, we provide definitions of these logics as well as establish a suitable proof theory thereof. In particular, we show how to apply the structural refinement methodology to extract cut-free nested sequent calculi for intuitionistic grammar logics from their semantics. This method proceeds by first transforming the semantics of these logics into sound and complete labeled sequent systems, which we prove have favorable proof-theoretic properties such as syntactic cut-elimination. We then transform these labeled systems into nested sequent systems via the introduction of propagation rules and the elimination of structural rules. Our derived proof systems are then put to use, whereby we prove the conservativity of intuitionistic grammar logics over their modal counterparts, establish the general undecidability of these logics, and recognize a decidable subclass, referred to as "simple" intuitionistic grammar logics.

Figures (9)

• Figure 1: Depictions of the (F1) and (F2) conditions imposed on bi-relational $\Upsigma$-models. Dotted arrows indicate the relations implied by the presence of the solid arrows.
• Figure 2: Axioms are displayed in the first row and their related frame conditions are displayed directly underneath them. We note that when $n=0$ in the $\mathrm{IPA}$, the related frame condition is taken to be $\forall w (w R_{x} w)$.
• Figure 3: The labeled calculi $\mathbf{L}_{\Upsigma}(\mathcal{A})$. We have $(d_{x})$ as a rule in the calculus, if $\mathrm{D}_{x} \in \mathcal{A}$, and an $(i^{s}_{x})$ rule in the calculus, for each $\mathrm{IPA}$ of the form $(\langle s \rangle A \supset \langle x \rangle A) \land ([ x ] A \supset [s] A) \in \mathcal{A}$. Furthermore, we have a $(\langle x \rangle_{l})$, $(\langle x \rangle_{r})$, $([x]_{l})$, $([x]_{r})$, and $(c_{x})$ rule for each $x \in \Upsigma$. The side condition $\dag$ states that the rule is applicable only if $u$ is fresh.
• Figure 4: Admissible rules.
• Figure 5: Propagation rules. Each rule is applicable only if the side condition $\dag$ holds.

Theorems & Definitions (100)

• Definition 1: Bi-relational $\Upsigma$-Model Lyo21b
• Remark 2
• Definition 3: Semantic Clauses Lyo21b
• Lemma 4: Persistence
• proof
• Definition 5: Axiomatization
• Definition 6: Syntactic Notions for Extensions
• Definition 7: Semantic Notions for Extensions
• Remark 8
• Theorem 9: Soundness and Completeness Lyo21b