Por Pedro Pinto (Universidade de Lisboa).
Abstract: Proof mining is the research program that aims to analyse proofs of mathematical theorems in order to extract hidden quantitative information – such as rates of convergence, rates of metastability and rates of asymptotic regularity. Proof theoretical tools like Kohlenbach’s monotone functional interpretation (), a variant of Gödel’s Dialectica, are of standard use. A newer functional interpretation was introduced by Ferreira and Oliva in 2005 (), dubbed the bounded functional interpretation (BFI). In recent work, a general principle was developed to analyse certain proofs that rely on a weak sequential compactness argument. By using a principle of bounded collection, we are able to consider an alternative simpler proof in a setting suited for an analysis with the BFI.
In this presentation I will explain how the BFI can be used in Proof Mining and present this general principle. We finish with some examples that illustrate the application of this general principle.
 Browder, Felix. Convergence of approximants to fixed points of nonexpansive nonlinear mappings in Banach spaces. Archive for Rational Mechanics and Analysis, 24(1):82-90, 1967.
 Ferreira, Fernando, and Paulo Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic 135.1-3: 73-112, 2005.
 Kohlenbach, Ulrich. Applied proof theory: proof interpretations and their use in mathematics. Springer Science & Business Media, 2008.
 Kohlenbach, Ulrich. On quantitative versions of theorems due to FE Browder and R. Wittmann. Advances in Mathematics, 226(3):2764-2795, 2011.
 Wittmann, Rainer. Approximation of fixed points of nonexpansive mappings, Arch. Math 58: 486-491, 1992.
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.