## Author: Anupam Das

## Paper Information

Title: | On the logical complexity of cyclic arithmetic |

Authors: | Anupam Das |

Proceedings: | PARIS Contributed papers |

Editors: | Alexis Saurin, David Baelde and Radu Calinescu |

Keywords: | Cyclic proofs, Peano arithmetic, Proof theory, Logical complexity, Reverse mathematics, Proof complexity |

Abstract: | 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Σ_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 n > 0. Furthermore, due to the 'uniformity' of our method, we also show that CA and PA proofs differ only elementarily in size. The inclusion IΣ_{n+1} ⊆ CΣ_n is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of Peano arithmetic (PA) proofs. It improves upon the natural result that IΣ_n ⊆ CΣ_n. The 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 (Kolodziejczyk, Michalewski, Pradic & Skrzypczak '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. This talk will be based on the following work: http://www.anupamdas.com/wp/log-comp-cyc-arith/ |

Pages: | 5 |

Talk: | Jul 08 16:45 (Session 42M: Contributed talks) |

Paper: |