On the logical complexity of cyclic arithmetic

摘要

We study the logical complexity of proofs in cyclic arithmetic($mathsf{CA}$), as introduced in Simpson '17, in terms of quantifieralternations of formulae occurring. Writing $CSigma_n$ for (the logicalconsequences of) cyclic proofs containing only $Sigma_n$ formulae, our mainresult is that $ISigma_{n+1}$ and $CSigma_n$ prove the same $Pi_{n+1}$theorems, for all $ngeq 0$. Furthermore, due to the 'uniformity' of ourmethod, we also show that $mathsf{CA}$ and Peano Arithmetic ($mathsf{PA}$)proofs of the same theorem differ only exponentially in size. The inclusion $ISigma_{n+1} subseteq CSigma_n$ is obtained by prooftheoretic techniques, relying on normal forms and structural manipulations of$mathsf{PA}$ proofs. It improves upon the natural result that $ISigma_n$ iscontained in $CSigma_n$. The converse inclusion, $CSigma_n subseteqISigma_{n+1}$, is obtained by calibrating the approach of Simpson '17 withrecent results on the reverse mathematics of B"uchi's theorem inKo{l}odziejczyk, Michalewski, PradicandSkrzypczak '16 (KMPS'16), andspecialising to the case of cyclic proofs. These results improve upon thebounds on proof complexity and logical complexity implicit in Simpson '17 andalso an alternative approach due to BerardiandTatsuta '17. The uniformity of our method also allows us to recover a metamathematicalaccount of fragments of $mathsf{CA}$; in particular we show that, for $ngeq0$, the consistency of $CSigma_n$ is provable in $ISigma_{n+2}$ but not$ISigma_{n+1}$. As a result, we show that certain versions of McNaughton'stheorem (the determinisation of $omega$-word automata) are not provable in$mathsf{RCA}_0$, partially resolving an open problem from KMPS '16.