Cyclic Arithmetic Is Equivalent to Peano Arithmetic.

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 coinduction. So cyclic proof systems are at least as powerful as the corresponding proof systems with explicit coinduction rules. Whether or not the converse inclusion holds is a non-trivial 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.