ABSTRACT. We study the logical complexity of proofs in cyclic arithmetic (CA), as introduced in Simpson '17, in terms of quantifier alternations of formulae occurring. Writing CΣ_n for (the logical consequences of) cyclic proofs containing only Σ_n formulae, our main result is that IΣ_{n+1} and CΣ_n prove the same Π_{n+1} theorems, for n > 0. Furthermore, due to the 'uniformity' of our method, we also show that CA and PA proofs differ only elementarily in size.

The inclusion IΣ_{n+1} ⊆ CΣ_n is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of Peano arithmetic (PA) proofs. It improves upon the natural result that IΣ_n ⊆ CΣ_n.

The inclusion CΣ_n ⊆ IΣ_{n+1} is obtained by calibrating the approach of Simpson '17 with recent results on the reverse mathematics of Büchi’s theorem (Kolodziejczyk, Michalewski, Pradic & Skrzypczak '16), and specialising to the case of cyclic proofs.

These results improve upon the bounds on proof complexity and logical complexity implicit in Simpson '17 and Berardi & Tatsuta '17.

This talk will be based on the following work: http://www.anupamdas.com/wp/log-comp-cyc-arith/