On the logical complexity of cyclic arithmetic

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. 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/

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