On the logical complexity of cyclic arithmetic

Anupam Das*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

13 Citations (Scopus)
73 Downloads (Pure)


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 all n≥0. Furthermore, due to the 'uniformity' of our method, we also show that CA and Peano Arithmetic (PA) proofs of the same theorem differ only exponentially in size. The inclusion IΣn+1 ⊆CΣn is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of PA proofs. It improves upon the natural result that IΣn is contained in CΣn. The converse 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 in Ko{\l}odziejczyk, Michalewski, Pradic & Skrzypczak '16 (KMPS'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. The uniformity of our method also allows us to recover a metamathematical account of fragments of CA; in particular we show that, for n≥0, the consistency of CΣn is provable in IΣn+2 but not IΣn+1. As a result, we show that certain versions of McNaughton's theorem (the determinisation of ω-word automata) are not provable in RCA0 , partially resolving an open problem from KMPS '16.
Original languageEnglish
Article number1
Number of pages39
JournalLogical Methods in Computer Science
Issue number1
Publication statusPublished - 6 Jan 2020

Bibliographical note

Funding Information:
The author is supported by a Marie Sklodowska-Curie fellowship, ERC project 753431.

Publisher Copyright:
© 2020, Logical Methods in Computer Science.


  • Induction
  • Peano arithmetic
  • cyclic proofs
  • logical complexity
  • proof theory

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'On the logical complexity of cyclic arithmetic'. Together they form a unique fingerprint.

Cite this