Cyclic arithmetic is equivalent to Peano arithmetic

Abstract

Cyclic proof provides a style of proof for logics with inductive (and coinductive) definitions, in which proofs are cyclic graphs representing a form of argument by infinite descent. It is easily shown that cyclic proof subsumes proof by (co)induction. So cyclic proof systems are at least as powerful as the corresponding proof systems with explicit (co)induction rules. Whether or not the converse inclusion holds is a nontrivial question. In this paper, we resolve this question in one interesting case. We show that a cyclic formulation of first-order arithmetic is equivalent in power to Peano Arithmetic. The proof involves formalising the meta-theory of cyclic proof in a subsystem of second-order arithmetic.