Cut elimination for propositional cyclic proof systems with fixed-point operators
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917819410546688 |
|---|---|
| author | Hori, Hiromasa Nakazawa, Koji Tatsuta, Makoto |
| author_facet | Hori, Hiromasa Nakazawa, Koji Tatsuta, Makoto |
| contents | Infinitary and cyclic proof systems are proof systems for logical formulas with fixed-point operators or inductive definitions. A cyclic proof system is a restriction of the corresponding infinitary proof system. Hence, these proof systems are generally not the same, as in the cyclic system may be weaker than the infinitary system. For several logics, the infinitary proof systems are shown to be cut-free complete. However, cyclic proof systems are characterized with many unknown problems on the (cut-free) completeness or the cut-elimination property. In this study, we show that the provability of infinitary and cyclic proof systems are the same for some propositional logics with fixed-point operators or inductive definitions and that the cyclic proof systems are cut-free complete. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2312_12792 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Cut elimination for propositional cyclic proof systems with fixed-point operators Hori, Hiromasa Nakazawa, Koji Tatsuta, Makoto Logic in Computer Science Logic 03F05, 03F52 F.4.1 Infinitary and cyclic proof systems are proof systems for logical formulas with fixed-point operators or inductive definitions. A cyclic proof system is a restriction of the corresponding infinitary proof system. Hence, these proof systems are generally not the same, as in the cyclic system may be weaker than the infinitary system. For several logics, the infinitary proof systems are shown to be cut-free complete. However, cyclic proof systems are characterized with many unknown problems on the (cut-free) completeness or the cut-elimination property. In this study, we show that the provability of infinitary and cyclic proof systems are the same for some propositional logics with fixed-point operators or inductive definitions and that the cyclic proof systems are cut-free complete. |
| title | Cut elimination for propositional cyclic proof systems with fixed-point operators |
| topic | Logic in Computer Science Logic 03F05, 03F52 F.4.1 |
| url | https://arxiv.org/abs/2312.12792 |