Twist Sequent Calculi for S4 and its Neighbors
Norihiro Kamide
TL;DR
The paper develops cut-free, analytic Gentzen-style twist sequent calculi for $S4$, introducing $lTS4$ (local negation handling) and $gTS4$ (global negation handling) that use twist rules to integrate negation with standard connectives and modal operators. These twist systems yield shorter proofs for provable negated modal formulas with many negations and are shown to be equivalent to Kripke's $GS4$ via formal derivations, while offering proof-length advantages over $GS4$ in relevant cases. The authors establish cut-elimination and the subformula property for $lTS4$ and $gTS4$, and extend the twist approach to $K$, $KT$, and $S5$ with global calculi $gTK$, $gTKT$, $gTS5$ and the hypersequent calculus $HTS5$, clarifying where cut-elimination holds. The work has implications for logic programming and automated reasoning with negation and modalities, suggesting avenues for uniform-proof frameworks and future exploration of additional twist calculi for broader modal-logical systems.
Abstract
Two Gentzen-style twist sequent calculi for the normal modal logic S4 are introduced and investigated. The proposed calculi, which do not employ the standard logical inference rules for the negation connective, are characterized by several twist logical inference rules for negated logical connectives. Using these calculi, short proofs can be generated for provable negated modal formulas that contain numerous negation connectives. The cut-elimination theorems for the calculi are proved, and the subformula properties for the calculi are also obtained. Additionally, Gentzen-style twist (hyper)sequent calculi for other normal modal logics including S5 are considered.