## 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Σ*for (the logical consequences of) cyclic proofs containing only Σ*_{n}*formulae, our main result is that IΣ*_{n}_{n+1}and CΣ*prove the same Π*_{n}_{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Σ*is contained in CΣ*_{n}*. The converse inclusion, CΣn⊆IΣ*_{n}_{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Σ*is provable in IΣ*_{n}_{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**RCA**_{0}, partially resolving an open problem from KMPS '16.Original language | English |
---|---|

Article number | 1 |

Number of pages | 39 |

Journal | Logical Methods in Computer Science |

Volume | 16 |

Issue number | 1 |

DOIs | |

Publication status | Published - 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.

## Keywords

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

## ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)