We study the logical complexity of proofs in cyclic arithmetic \(\left(\mathsf{CA}\right)\), as introduced by Simpson, in terms of quantifier alternations of formulae occurring. Writing \(\mathrm C\Sigma_n\) for (the logical consequences of) cyclic proofs containing only \(\Sigma_n\) formulae, our main result is that \(\mathrm I\Sigma_{n+1}\) and \(\mathrm C\Sigma_n\) prove the same \(\Pi_{n+1}\) theorems, for \(n \geq 0\). Furthermore, due to the ‘uniformity’ of our method, we also show that \(\mathsf{CA}\) and Peano Arithmetic \(\left(\mathsf{PA}\right)\) proofs of the same theorem differ only elementarily in size.
The inclusion \(\mathrm I\Sigma_{n+1} \subseteq \mathrm C\Sigma_n\) is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of \(\mathsf{PA}\) proofs. It improves upon the natural result that \(\mathrm I\Sigma_n \subseteq \mathrm C\Sigma_n\).
The converse inclusion, \(\mathrm C\Sigma_n \subseteq \mathrm I \Sigma_{n+1}\), is obtained by calibrating Simpson’s approach with recent results on the reverse mathematics of Büchi’s theorem, and specialising to the case of cyclic proofs.
These results improve upon the bounds on proof complexity and logical complexity implicit in Simpson’s work, and also an approach by Berardi and Tatsuta.