## Abstract

We study the logical complexity of proofs in cyclic arithmetic (

and Peano Arithmetic (

CΣn⊆IΣ

**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,*_{n}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Σ*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 | 4818 |

Pages (from-to) | 1:1 - 1:39 |

Number of pages | 39 |

Journal | Logical Methods in Computer Science |

Volume | 16 |

Issue number | 1 |

DOIs | |

Publication status | Published - 6 Jan 2020 |

## Keywords

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