Fragments of arithmetic and cyclic proofs

TL;DR

This paper introduces a new cyclic proof system for Peano arithmetic that simplifies proof analysis and automation, and can represent various subsystems with restricted induction.

Contribution

The paper proposes an alternative cyclic proof system for Peano arithmetic that is simpler and adaptable for proof analysis and automation, also representing subsystems as fragments.

Findings

The new system is simpler than existing cyclic proof systems.

It effectively models various subsystems of Peano arithmetic.

The system facilitates proof analysis and inductive proof automation.

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.