João Enes
Faculdade de Ciências, ULisboa

Abstract: In this talk we present the work by Jeremy Avigad and Henry Towsner [1] where they provide a functional interpretation of classical theories of positive arithmetic inductive definitions, along the lines of Gödel's "Dialectica" interpretation of first-order arithmetic, which reduces them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

[1] J. Avigad and H. Towsner. Functional interpretation and inductive definitions. J. Symbolic Logic, 74(4):1100–1120, 2009

This seminar is supported by National Funding from FCT - Fundação para a Ciência e a Tecnologia, under the project: UID/MAT/04561/2013.