Cut Elimination for Extended Sequent Calculi
Cut Elimination for Extended Sequent Calculi
Author(s): Simone Martini, Andrea Masini, Margherita ZorziSubject(s): Philosophy, Logic
Published by: Wydawnictwo Uniwersytetu Łódzkiego
Keywords: proof theory; sequent calculus; cut elimination; modal logic; 2-sequents
Summary/Abstract: We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \(\Box\) and \(\Diamond\). Starting points for this research are 2-sequents and indexed-based calculi (sequents and tableaux). By extending and modifying existing proposals, we show how to achieve a syntactical proof of the cut-elimination theorem that is as close as possible to the one for first-order classical logic. In doing this, we implicitly show how small is the proof-theoretical distance between classical logic and the systems under consideration.
Journal: Bulletin of the Section of Logic
- Issue Year: 52/2023
- Issue No: 4
- Page Range: 459-495
- Page Count: 37
- Language: English