On the logical complexity of cyclic arithmetic

Anupam Das. Preprint. PDF

We study the logical complexity of proofs in cyclic arithmetic, as introduced by Simpson, in terms of quanti´Čüer alternations of formulae occurring. Writing \(\mathrm C\Sigma_n\) for (the logical consequences of) cyclic proofs containing only \(\Sigma_n\) formulae, we show for \(n\geq 0\):

  1. \(\mathrm I \Sigma_{n+1} \subseteq \mathrm C \Sigma_n\) over \(\Sigma_n\) sequents. This is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of Peano Arithmetic proofs. It improves upon the natural result that \(\mathrm I \Sigma_n \subseteq \mathrm C \Sigma_n\), although induces a non-elementary blowup in the size of proofs.
  2. \( \mathrm C \Sigma_n \subseteq \mathrm I \Sigma_{n+2}\), and moreover \(\mathrm{CA}\) and \(\mathrm{PA}\) proofs differ only elementarily in size. This 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. It improves upon the apparent proof complexity and logical complexity of previous work, including an approach by Berardi and Tatsuta.