Unravelling Cyclic First-Order Arithmetic
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913962451271680 |
|---|---|
| author | Leigh, Graham E. Wehr, Dominik |
| author_facet | Leigh, Graham E. Wehr, Dominik |
| contents | Cyclic proof systems for Heyting and Peano arithmetic eschew induction axioms by accepting proofs which are finite graphs rather than trees. Proving that such a cyclic proof system coincides with its more conventional variants is often difficult: Previous proofs in the literature rely on intricate arithmetisations of the metamathematics of the cyclic proof systems.
In this article, we present a simple and direct embedding of cyclic proofs for Heyting and Peano arithmetic into purely inductive, i.e. 'finitary', proofs by adapting a translation introduced by Sprenger and Dam for a cyclic proof system of $μ\text{FOL}$ with explicit ordinal approximations. We extend their method to recover Das' result of $\text{C}Π_n \subseteq \text{I}Π_{n + 1}$ for Peano arithmetic. As part of the embedding we present a novel representation of cyclic proofs as a labelled sequent calculus. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_20865 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Unravelling Cyclic First-Order Arithmetic Leigh, Graham E. Wehr, Dominik Logic Logic in Computer Science Cyclic proof systems for Heyting and Peano arithmetic eschew induction axioms by accepting proofs which are finite graphs rather than trees. Proving that such a cyclic proof system coincides with its more conventional variants is often difficult: Previous proofs in the literature rely on intricate arithmetisations of the metamathematics of the cyclic proof systems. In this article, we present a simple and direct embedding of cyclic proofs for Heyting and Peano arithmetic into purely inductive, i.e. 'finitary', proofs by adapting a translation introduced by Sprenger and Dam for a cyclic proof system of $μ\text{FOL}$ with explicit ordinal approximations. We extend their method to recover Das' result of $\text{C}Π_n \subseteq \text{I}Π_{n + 1}$ for Peano arithmetic. As part of the embedding we present a novel representation of cyclic proofs as a labelled sequent calculus. |
| title | Unravelling Cyclic First-Order Arithmetic |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2507.20865 |