Cut Elimination for Extended Sequent Calculi
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Lodz University Press
2023-09-01
|
| Series: | Bulletin of the Section of Logic |
| Subjects: | |
| Online Access: | https://czasopisma.uni.lodz.pl/bulletin/article/view/13263 |
| _version_ | 1797366224142729216 |
|---|---|
| author | Simone Martini Andrea Masini Margherita Zorzi |
| author_facet | Simone Martini Andrea Masini Margherita Zorzi |
| author_sort | Simone Martini |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-03-08T17:01:14Z |
| format | Article |
| id | doaj.art-b1e1dee47c9c4f58b207a9f0b231cab9 |
| institution | Directory Open Access Journal |
| issn | 0138-0680 2449-836X |
| language | English |
| last_indexed | 2024-03-08T17:01:14Z |
| publishDate | 2023-09-01 |
| publisher | Lodz University Press |
| record_format | Article |
| series | Bulletin of the Section of Logic |
| spelling | doaj.art-b1e1dee47c9c4f58b207a9f0b231cab92024-01-04T12:28:22ZengLodz University PressBulletin of the Section of Logic0138-06802449-836X2023-09-0152445949510.18778/0138-0680.2023.2213163Cut Elimination for Extended Sequent CalculiSimone Martini0https://orcid.org/0000-0002-9834-1940Andrea Masini1Margherita Zorzi2Universit`a di Bologna, Dipartimento di Informatica – Scienza e IngegneriaUniversit`a di Verona, Dipartimento di Informatica Universit`a di Verona, Dipartimento di Informatica 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.https://czasopisma.uni.lodz.pl/bulletin/article/view/13263proof theorysequent calculuscut eliminationmodal logic2-sequents |
| spellingShingle | Simone Martini Andrea Masini Margherita Zorzi Cut Elimination for Extended Sequent Calculi Bulletin of the Section of Logic proof theory sequent calculus cut elimination modal logic 2-sequents |
| title | Cut Elimination for Extended Sequent Calculi |
| title_full | Cut Elimination for Extended Sequent Calculi |
| title_fullStr | Cut Elimination for Extended Sequent Calculi |
| title_full_unstemmed | Cut Elimination for Extended Sequent Calculi |
| title_short | Cut Elimination for Extended Sequent Calculi |
| title_sort | cut elimination for extended sequent calculi |
| topic | proof theory sequent calculus cut elimination modal logic 2-sequents |
| url | https://czasopisma.uni.lodz.pl/bulletin/article/view/13263 |
| work_keys_str_mv | AT simonemartini cuteliminationforextendedsequentcalculi AT andreamasini cuteliminationforextendedsequentcalculi AT margheritazorzi cuteliminationforextendedsequentcalculi |