Pedro Pinto
Faculdade de Ciências da Universidade de Lisboa

Abstract: Bounded functional interpretation was introduced by F. Ferreira and P. Oliva in [1] as an interpretation of Heyting arithmetic that greatly differs from Gödel's Dialectica interpretation. By a composition with a negative translation is possible to obtain a bounded interpretation of Peano arithmetic. In this talk we start by presenting a direct bounded functional interpretation of Peano arithmetic, [2]. Next we show a result by Kohlenbach relating his monotone interpretation and the bounded interpretation, [3]. More precisely, we show that over the model of the strongly majorizable functionals a solution for the bounded interpretation is also a solution for the monotone interpretation, although the latter uses the existence of an underlying precise witness.

[1] F. Ferreira and P. Oliva, Bounded functional interpretation, Annals of Pure and Applied Logic 135, 73–112 (2005) [2] F. Ferreira, Injecting uniformities into Peano arithmetic, Annals of Pure and Applied Logic 157, 122–129 (2009) [3] U. Kohlenbach, A note on the monotone functional interpretation, Math. Log. Quart. 57, No.6, 611–614 (2011)

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.