Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915087282864128 |
|---|---|
| author | Maniwa, Akinori Kashima, Ryo |
| author_facet | Maniwa, Akinori Kashima, Ryo |
| contents | The cut-elimination procedure for the provability logic is known to be problematic: a Löb-like rule keeps cut-formulae intact on reduction, even in the principal case, thereby complicating the proof of termination. In this paper, we present a syntactic cut-elimination proof based on nested sequents, a generalization of sequents that allows a sequent to contain other sequents as single elements. A similar calculus was developed by Poggiolesi (2009), but there are certain ambiguities in the proof. Adopting the idea of Kushida (2020) into nested sequents, our proof does not require an extra measure on cuts or error-prone, intricate rewriting on derivations, but only straightforward inductions, thus leading to less ambiguity and confusion. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_00487 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents Maniwa, Akinori Kashima, Ryo Logic in Computer Science The cut-elimination procedure for the provability logic is known to be problematic: a Löb-like rule keeps cut-formulae intact on reduction, even in the principal case, thereby complicating the proof of termination. In this paper, we present a syntactic cut-elimination proof based on nested sequents, a generalization of sequents that allows a sequent to contain other sequents as single elements. A similar calculus was developed by Poggiolesi (2009), but there are certain ambiguities in the proof. Adopting the idea of Kushida (2020) into nested sequents, our proof does not require an extra measure on cuts or error-prone, intricate rewriting on derivations, but only straightforward inductions, thus leading to less ambiguity and confusion. |
| title | Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2501.00487 |