2025/02/10 by Lev D. Beklemishev, Beklemishev, Lev D., Daniyar Shamkanov +3
Mathematics · #03F07 #03F30 #FOS: Mathematics #History and Theory of Mathematics #Logic (math.LO)
paper · pdf · doi:10.48550/arxiv.2502.06639
openalex publication_date 2025/02/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.