BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:On the logical complexity of cyclic arithmetic - A
nupam Das\, University of Birmingham
DTSTART:20191011T100000Z
DTEND:20191011T110000Z
UID:TALK3904AT
URL:/talk/index/3904
DESCRIPTION:We study the logical complexity of proofs in cycli
c arithmetic (CA)\, as introduced in Simpson '17\,
in terms of quantifier alternations of formulae o
ccurring. Writing CΣn for (the logical consequence
s of) cyclic proofs containing only Σn formulae\,
our main result is that IΣn+1 and CΣn prove the sa
me Πn+1 theorems\, for all n≥0. Furthermore\, due
to the 'uniformity' of our method\, we also show t
hat CA and Peano Arithmetic (PA) proofs of the sam
e theorem differ only exponentially in size.\n\nTh
e inclusion IΣn+1⊆CΣn is obtained by proof theoret
ic techniques\, relying on normal forms and struct
ural manipulations of PA proofs. It improves upon
the natural result that IΣn is contained in CΣn. T
he converse inclusion\, CΣn⊆IΣn+1\, is obtained by
calibrating the approach of Simpson '17 with rece
nt results on the reverse mathematics of Büchi's t
heorem in Kołodziejczyk\, Michalewski\, Pradic & S
krzypczak '16 [KMPS ‘16]\, and specialising to the
case of cyclic proofs. These results improve upon
the bounds on proof complexity and logical comple
xity implicit in Simpson '17 and also an alternati
ve approach due to Berardi & Tatsuta '17.\n\nThe u
niformity of our method also allows us to recover
a metamathematical account of fragments of CA\; in
particular we show that\, for n≥0\, the consisten
cy 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 formulati
on of McNaughton’s theorem\, the determinisation o
f omega-word automata\, is not provable in RCA0.\n
\nThis talk will be based on the following preprin
t\, that has recently been accepted to Logical Met
hods in Computer Science:\n\nhttps://arxiv.org/abs
/1807.10248
LOCATION:Computer Science\, The Sloman Lounge (UG)
CONTACT:Jamie Vicary
END:VEVENT
END:VCALENDAR