Unravelling Cyclic First-Order Arithmetic

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.