Conceptual
Browse Instruct Curate

Twist Sequent Calculi for the Modal Logic S4

Two Gentzen-style sequent calculi for the normal modal logic S4 that replace the standard negation inference rules with 'twist' rules acting directly on negated connectives and modal operators. The twist rules generate short, abbreviated proofs of provable negated modal formulas carrying many negations; the calculi satisfy cut-elimination and the subformula property, and the construction extends via (hyper)sequents to S5 and neighboring normal modal logics.