Seminário de Lógica Matemática

Collection in Proof Mining: a general principle

Sala 6.2.33, FCUL, Lisboa

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.

15h00
CMAF-CIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Título do prémio

As candidaturas decorrem até ao dia 31 de maio.

Logótipo do Verão na ULisboa, sobre um fundo amarelo

Uma oportunidade única de conheceres e experimentares o ritmo e o espírito da vida académica!

Título/data do evento, logótipos das entidades organizadoras e fotografia de Lisboa (Castelo de S. Jorge e respetiva colina)

Inscrição (taxa reduzida) até 20 de abril.

Título/data/local do evento, logótipos das entidades organizadoras e várias fotografias da orla costeira e de pessoas

Escola de verão com um programa muito diversificado, com especialistas em vários tópicos, que vão falar sobre formas de olhar para o nosso planeta de uma forma integrada, juntando conhecimentos de várias disciplinas.

Vem investigar connosco!

Logótipo do evento, sobre um fundo branco

Um evento de reunião da comunidade nacional nas diversas vertentes da informática, com a ambição de ser o fórum de eleição para a divulgação, discussão e reconhecimento de trabalhos científicos.

Páginas