Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

TL;DR

This paper introduces a novel methodology called structural refinement to derive nested sequent systems for intuitionistic modal logics from labelled systems, enabling better proof-theoretic analysis and encoding frame conditions.

Contribution

It develops a systematic process to transform labelled sequent systems into nested systems using structural refinement, incorporating parameterized propagation rules for intuitionistic modal logics.

Findings

Nested systems are sound and cut-free complete.

Propagation rules encode frame conditions as first-order Horn formulae.

Structural rules are eliminated while preserving proof properties.

Abstract

We employ a recently developed methodology -- called "structural refinement" -- to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized with formal grammars, and which encode certain frame conditions expressible as first-order Horn formulae that correspond to a subclass of the Scott-Lemmon axioms. We show that our nested systems are sound, cut-free complete, and admit hp-admissibility of typical structural rules.