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 ([1]), a variant of Gödel’s Dialectica, are of standard use. A newer functional interpretation was introduced by Ferreira and Oliva in 2005 ([2]), 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.

Referências:
[1] 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.
[2] Ferreira, Fernando, and Paulo Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic 135.1-3: 73-112, 2005.
[3] Kohlenbach, Ulrich. Applied proof theory: proof interpretations and their use in mathematics. Springer Science & Business Media, 2008.
[4] Kohlenbach, Ulrich. On quantitative versions of theorems due to FE Browder and R. Wittmann. Advances in Mathematics, 226(3):2764-2795, 2011.
[5] 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.