We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the K, D, T, K4, D4 and 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 □ and ♢. 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.

Cut Elimination for Extended Sequent Calculi

Andrea Masini;Margherita Zorzi
2023-01-01

Abstract

We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the K, D, T, K4, D4 and 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 □ and ♢. 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.
2023
Proof theory, sequent calculus, cut elimination, modal logic, 2-sequents
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1094391
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact