Speaker
Lukas Melgaard
University of Birmingham
Talks at this conference:
Friday, 17:20, J330 
Cyclic proofs for arithmetic with least and greatest fixed points 
Authors: Lukas Melgaard and Gianluca Curzi We investigate the cyclic proof theory of \(\mu \mathrm{PA}\), a theory that extends Peano Arithmetic with least and greatest fixed point operators. Our cyclic system \(\mathrm{C} \mu \mathrm{PA}\) subsumes Simpson’s cyclic arithmetic [3] and the stronger \(\mathrm{CID}_{< \omega}\) from [1]. Our main result is that the inductive system \(\mu \mathrm{PA}\) and the cyclic system \(\mathrm{C} \mu \mathrm{PA}\) prove the same arithmetical theorems. We conduct a metamathematical argument inspired by those in [3,1] for Cyclic Arithmetic to formalize the soundness of cyclic proofs within secondorder arithmetic by a form of induction on closure ordinals and then appealing to conservativity results. Since the closure ordinals of our inductive definitions far exceed the recursive ordinals we cannot rely on ordinal notations and must instead formalize a theory of ordinals within secondorder arithmetic. This is similar to what is done in [1] for \(\mathrm{CID}_{< \omega}\) except here we also need to use the reverse mathematics of a more powerful version of KnasterTarski as seen in [2]. Bibliography


Thursday, 14:40, J222 
Cyclic versions of arithmetic theories with inductive definitions 
We investigate the cyclic proof theory of extensions of Peano Arithmetic by (finitely iterated) inductive definitions. Such theories are essential to proof theoretic analyses of certain `impredicative’ theories; moreover, our cyclic systems naturally subsume Simpson’s Cyclic Arithmetic. Our main result is that cyclic and inductive systems for arithmetical inductive definitions are equally powerful. We conduct a metamathematical argument, formalising the soundness of cyclic proofs within secondorder arithmetic and appealing to conservativity. This approach is inspired by those of Simpson and Das for Cyclic Arithmetic, however we must further address a difficulty that the closure ordinals of our inductive definitions (around ChurchKleene) far exceed the proof theoretic ordinal of the appropriate metatheory (around BachmannHoward or Bucholz), and so explicit induction on their notations is not possible. For this reason, we rather rely on a formalisation of the theory of (recursive) ordinals within secondorder arithmetic. 