Unravelling Cyclic First-Order Arithmetic

TL;DR

This paper introduces a straightforward embedding of cyclic proof systems for arithmetic into finitary proofs, simplifying the proof equivalence and extending existing results using a novel labelled sequent calculus representation.

Contribution

It provides a simple, direct translation of cyclic proofs into inductive proofs for arithmetic, extending prior results and introducing a new labelled sequent calculus approach.

Findings

Embedding of cyclic proofs into finitary proofs for arithmetic.

Extension of Das' result on proof systems for Peano arithmetic.

Introduction of a labelled sequent calculus for cyclic proofs.

Abstract

Cyclic proof systems for Heyting and Peano arithmetic eschew induction axioms by accepting proofs which are finite graphs rather than trees. Proving that such a cyclic proof system coincides with its more conventional variants is often difficult: Previous proofs in the literature rely on intricate arithmetisations of the metamathematics of the cyclic proof systems. In this article, we present a simple and direct embedding of cyclic proofs for Heyting and Peano arithmetic into purely inductive, i.e. 'finitary', proofs by adapting a translation introduced by Sprenger and Dam for a cyclic proof system of $\mu\text{FOL}$ with explicit ordinal approximations. We extend their method to recover Das' result of $\text{C}\Pi_n \subseteq \text{I}\Pi_{n + 1}$ for Peano arithmetic. As part of the embedding we present a novel representation of cyclic proofs as a labelled sequent calculus.