Cut-free double sequent calculus for S5
Andrzej Indrzejczak · Logic Journal of IGPL · 1998
We aim at an exposition of some nonstandard cut-free Gentzen formalization for S5, called DSC (double sequent calculus). DSC operates on two types of sequents instead of one, and shifting of wffs from one side of a sequent to the other is regulated by special rules and subject to some restrictions. Despite of this apparent inconvenience it seems to be simpler than other, known Gentzen-style systems for S5. The number of additional formal machinery is kept in reasonable bounds. Rules have subformula-property, hence constructing of proofs in DSC is quite simple. DSC is a case study of S5 in the wider perspective of MSC (multiple sequent calculus), where sequents of arbitrary number of modal types are considered (see Indrzejczak [4]). MSC proves especially useful for obtaining cut-free formalizations of symmetric logics (KB and its extensions). S5, due to its special properties, allows for many simplifications in the general apparatus of MSC, in particular we cut down on the number of types of sequents and on the number of special, structural rules. Keywords:modal logic S5, sequent calculi