Proof theory
Chairs: Abhishek De, Katarzyna Kowalik
Talks in this session
14:00 
Valentin Blot, Variants of bar recursion and their uses 
Bar recursion was invented by Spector to provide a proof of consistency for analysis via an extension of Gödel’s Dialectica interpretation to the axiom scheme of comprehension. Since then, several variants of this operator have been defined in various contexts, to provide computational content to diverse logical principles. In this talk I will present various forms of bar recursion in the setting of the realizability and Dialectica interpretations. I will show how these operators give computational content to principles such as the doublenegation shift, the axiom of choice in a classical setting, and the comprehension axiom of arithmetic. 

14:40 
Lukas Melgaard, 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. 

15:20 
Takako Nemoto, Computability theory over intuitionistic logic 
It is known that basic part of recursion theory, such as recursion theory, smntheorem, recursion theorem and normal form theorem can be formalized in HA [2]. The aim of this talk is to do recursion theory itself more in constructive mathematics. One of the problem is the treatment of complements of sets of natural numbers over intuitionistic logic. In this talk, we adopt the notion of complemented sets by [1] and try to develop degree theory. Bibliography
