Fragments of arithmetic and cyclic proofs
Lev D. Beklemishev, Daniyar S. Shamkanov, Ivan N. Smirnov
TL;DR
The paper develops a simplified cyclic proof framework for first-order arithmetic that replaces induction axioms with structured cyclic proofs and annotations. It shows that the hierarchy of PA fragments defined by restricted induction, such as $I\Sigma_n$ and $I\Pi^R_{n+1}$, can be captured by corresponding cyclic systems $\mathsf{S}_n$, $\mathsf{S}^{\Pi}_n$, and $\mathsf{S}^{\Sigma}_n$, with precise equivalences to the traditional theories: $\mathsf{S}_n$ ≡ $I\Sigma_{n+1}$, $\mathsf{S}^{\Pi}_n$ ≡ $I\Pi^R_{n+1}$, and $\mathsf{S}^{\Sigma}_n$ ≡ $I\Sigma_n^R$. The approach leverages non-well-founded proofs, back-links, and annotation discipline to enable proof-search-oriented analysis and a clearer metatheory for induction in arithmetic. This yields a framework that is simpler to analyze and potentially more amenable to automation, while preserving alignment with core arithmetical fragments and their induction schemas. Practical impact includes foundations for automated inductive proof search and deeper proof-theoretic understanding of arithmetic fragments without reliance on automata-theoretic devices.
Abstract
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.