University of Birmingham > Talks@bham > Theoretical computer science seminar > On the logical complexity of cyclic arithmetic

## On the logical complexity of cyclic arithmeticAdd to your list(s) Download to your calendar using vCal - Anupam Das, University of Birmingham
- Friday 11 October 2019, 11:00-12:00
- Computer Science, The Sloman Lounge (UG).
If you have a question about this talk, please contact Jamie Vicary. 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 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Σn is contained in CΣn. The converse 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 in Koł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 also an alternative approach due to 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Σn is provable in IΣn+2 but not IΣn+1. As a corollary, we partially resolve an open problem from [KMPS ‘16], showing that a natural formulation of McNaughton’s theorem, the determinisation of omega-word automata, is not provable in RCA0 . This talk will be based on the following preprint, that has recently been accepted to Logical Methods in Computer Science: https://arxiv.org/abs/1807.10248 This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Computer Science, The Sloman Lounge (UG)
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsMolecular and Medical Physics Seminar Series Cold atoms Data Science and Computational Statistics Seminar## Other talksModule tensor categories and the Landau-Ginzburg/conformal field theory correspondence View fusion vis-à-vis a Bayesian interpretation of Black-Litterman for portfolio allocation Advancing biomedical photoacoustic imaging using structured light and optical microresonators Structured Decompositions: recursive data and recursive algorithms TBC |