Fragments of arithmetic and cyclic proofs
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_ | 1866916606492278784 |
|---|---|
| author | Beklemishev, Lev D. Shamkanov, Daniyar S. Smirnov, Ivan N. |
| author_facet | Beklemishev, Lev D. Shamkanov, Daniyar S. Smirnov, Ivan N. |
| contents | We present an alternative cyclic proof system for Peano arithmetic that could be simpler than the existing ones and well-adapted both for proof analysis and for automatizing inductive proof search. In addition, we will show how various traditional subsystems of Peano arithmetic defined by restricted forms of induction can be represented as fragments of the proposed system. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_06639 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Fragments of arithmetic and cyclic proofs Beklemishev, Lev D. Shamkanov, Daniyar S. Smirnov, Ivan N. Logic 03F07, 03F30 We present an alternative cyclic proof system for Peano arithmetic that could be simpler than the existing ones and well-adapted both for proof analysis and for automatizing inductive proof search. In addition, we will show how various traditional subsystems of Peano arithmetic defined by restricted forms of induction can be represented as fragments of the proposed system. |
| title | Fragments of arithmetic and cyclic proofs |
| topic | Logic 03F07, 03F30 |
| url | https://arxiv.org/abs/2502.06639 |