Cyclic Proofs for iGL via Corecursion
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917058290122752 |
|---|---|
| author | Miranda, Borja Sierra |
| author_facet | Miranda, Borja Sierra |
| contents | Cyclic proof theory studies proofs where cycles are allowed. This is useful for developing proof theory for logics with fixpoint operators: cycles can be used to represent the unfolding of a fixpoint. However, this cyclic character is not unique to such explicit fixpoints. For example, modal logics whose frames have a Noetherian (conversely wellfounded) condition, such as GL (Goedel-Loeb logic), S4Grz (Grzegorczyk logic) and K4Grz also have cyclic proof systems.
Particularly, Shamkanov introduces a non-wellfounded and a cyclic sequent system GL. He proves the equivalence of these two systems with an acyclic finite system via proof translations. In order to go from the finite system to the non-wellfounded system he defines the translation by corecursion.
Iemhoff generalized the work of Shamkanov studying when, for a given modal logic proof system, there exists another modal logic proof system such that proofs in the first are equivalent to cyclic proofs in the second. There, she shows that iGL, an intuitionistic version of GL, also has a natural cyclic proof system.
We provide an alternative proof of the equivalence of a standard calculus for iGL and a cyclic one. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_10785 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Cyclic Proofs for iGL via Corecursion Miranda, Borja Sierra Logic Logic in Computer Science Cyclic proof theory studies proofs where cycles are allowed. This is useful for developing proof theory for logics with fixpoint operators: cycles can be used to represent the unfolding of a fixpoint. However, this cyclic character is not unique to such explicit fixpoints. For example, modal logics whose frames have a Noetherian (conversely wellfounded) condition, such as GL (Goedel-Loeb logic), S4Grz (Grzegorczyk logic) and K4Grz also have cyclic proof systems. Particularly, Shamkanov introduces a non-wellfounded and a cyclic sequent system GL. He proves the equivalence of these two systems with an acyclic finite system via proof translations. In order to go from the finite system to the non-wellfounded system he defines the translation by corecursion. Iemhoff generalized the work of Shamkanov studying when, for a given modal logic proof system, there exists another modal logic proof system such that proofs in the first are equivalent to cyclic proofs in the second. There, she shows that iGL, an intuitionistic version of GL, also has a natural cyclic proof system. We provide an alternative proof of the equivalence of a standard calculus for iGL and a cyclic one. |
| title | Cyclic Proofs for iGL via Corecursion |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2310.10785 |