Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement

TL;DR

This paper develops nested sequent calculi for intuitionistic grammar logics using structural refinement, enabling cut-free proofs, and analyzes their properties including conservativity, undecidability, and a decidable subclass.

Contribution

It introduces a novel proof-theoretic approach to intuitionistic grammar logics via structural refinement, producing sound, complete, and cut-free nested sequent systems.

Findings

Proved conservativity over modal logics

Established general undecidability of the logics

Identified a decidable subclass called 'simple' intuitionistic grammar logics

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.