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 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.

Martini, S., Masini, A., Zorzi, M. (2023). Cut Elimination for Extended Sequent Calculi. BULLETIN OF THE SECTION OF LOGIC, 52(4), 459-495 [10.18778/0138-0680.2023.22].

Cut Elimination for Extended Sequent Calculi

Martini, Simone
;
2023

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 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.
2023
Martini, S., Masini, A., Zorzi, M. (2023). Cut Elimination for Extended Sequent Calculi. BULLETIN OF THE SECTION OF LOGIC, 52(4), 459-495 [10.18778/0138-0680.2023.22].
Martini, Simone; Masini, Andrea; Zorzi, Margherita
File in questo prodotto:
File Dimensione Formato  
2023-BSL.pdf

accesso aperto

Descrizione: Full text
Tipo: Versione (PDF) editoriale
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione - Non commerciale - Non opere derivate (CCBYNCND)
Dimensione 1.94 MB
Formato Adobe PDF
1.94 MB Adobe PDF Visualizza/Apri

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/11585/950555
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact