On the Logical Complexity of Cyclic Proofs in Arithmetic

‘Cyclic proofs’ are an approach to proof theory that replaces induction axioms by non-wellfoundedness in structure of a proof. Naturally, we would expect some sort of correctness condition to avoid fallacious reasoning, and this is typically in the form of a certain ‘liveness’ condition on the infinite branches. When the proof is expressed as a finite graph (possibly with cycles), this condition can be effectively checked via reduction to decidable problems over omega-word automata.

Simpson recently introduced ‘cyclic arithmetic’ (CA), as a cyclic variant of Peano arithmetic (PA). His main result was that CA coincides with PA in terms of provability. His proof requires the formalisation of much of omega-word automaton theory inside PA, although a later proof of this result by Berardi & Tatsuta avoids this and is more structural in its exposition.

In this talk I will present some results comparing the logical complexity of fragments of CA and PA, namely by restricting the number of quantifier alternations of formulae in a proof. We also show that the proof complexity of CA and PA differs only elementarily, improving upon the apparent non-elementary complexity in Simpson’s proof.