Fragments of arithmetic and cyclic proofs
Lev D. Beklemishev, Daniyar Salkarbekovich Shamkanov, Ivan Nikolaevich Smirnov · Sbornik Mathematics · 2025
We define a new cyclic proof system for Peano arithmetic that is simpler than the existing ones and can be adapted for analysis of formal inference and for automatizing inductive proof search. We show how various traditional subsystems of Peano arithmetic defined by restricted forms of induction can be represented as fragments of the proposed system. Bibliography: 45 titles.