Seminário de Lógica Matemática

Some arguments in proof mining

Sala 6.2.33, FCUL, Lisboa

Por Pedro Pinto (Faculdade de Ciências, CMAFcIO, Universidade de Lisboa).

Abstract: Proof mining is the search of quantitative information from non-effective mathematical proofs [1]. It is known that, in general, it is not possible to extract such information directly for \Pi^0_3 statements. Instead one must translate those statements into what is called their metastable version [2]. A good understanding of these metastability properties is of great importance when carrying out a quantitative analysis, as \Pi^0_3 statements do frequently appear in ordinary mathematics (e.g. in convergence or Cauchy properties).

The purpose of this talk is to give a small insight of the inner works of proof mining and a theoretical explanation of how common mathematical arguments are analysed. Although these results are in essence true despite the technique used in proof mining, we will be focusing on the application of the bounded functional interpretation [3]. This work follows from recent developments in the application of this technique to the proof mining program [4][5][6][7]. We will look in some detail at the metastability property and explain how to give a quantitative meaning to two metastability properties taken simultaneously. Additionally, we will explain how to carry out an analysis of a mathematical proof that follows a discussion by cases. This helps in better understanding the difference between postulates (axioms added to an appropriate formal theory that serves as a background to the application of the proof-theoretical techniques) and implicative assumptions (antecedents of implications).

References:

[1] Kohlenbach, U. (2008). Applied proof theory: proof interpretations and their use in mathematics. Springer Science & Business Media.
[2] Tao, T., Soft analysis, hard analysis, and the finite convergence principle. Essay posted May 23, 2007. Available at: http://terrytao.wordpress.com/2007/05/23/soft-analysishard-analysis-and-the-finite-convergence-principle/ (32, 37, 464).
[3] Ferreira, F. (2009). Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157(2-3), 122-129.
[4] Ferreira, F., Leustean, L., & Pinto, P. (2018). On the removal of weak compactness arguments in proof mining. arXiv preprint arXiv:1810.01508.
[5] Leustean, L., & Pinto, P. (2019). Quantitative results on Halpern type proximal point algorithms (in preparation).
[6] Pinto, P. (2019). Metastability bounds on the Halpern type proximal point algorithm (in preparation).
[7] Dinis, B., & Pinto, P. (2019). Metastability of the proximal point algorithm with multi-parameters (in preparation).

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional

Uma vez por mês, aos domingos de manhã, junte-se à equipa de investigadores da Lista Vermelha de Invertebrados. Participe e contribua para a amostragem da diversidade de insetos em Sítios de Importância Comunitária da Rede Natura 2000.

Curso de 4 módulos, com os seguintes temas:

Field Trip "Tectono-stratigraphic evolution of the SW Iberian Margin and its hydrocarbon potential"

A AAPG-SC UL anuncia a 1.ª Field Trip do presente ano letivo, em parceria com a SEG Técnico Student Chapter Lisbon, intitulada “Tectono-stratigraphic evolution of the SW Iberian Margin and its hydrocarbon potential” e orientada pelo PhD Ricardo Pereira (Partex) e pelo Pr

O congresso conta com a participação de Jorge Relvas (Ciências ULisboa).

Noites no Observatório "Coincidências Cósmicas"

Vivemos num Universo que parece ter sido ajustado de forma muito precisa para permitir a nossa existência.

Seminário Permanente de Astronomia Antiga | CIUHCT/UL - DHFC/FCUL "O movimento da oitava esfera"

Este seminário é um curso livre, aberto à comunidade académica e a todos os interessados, com entrada gratuita.

Por Alessandro Zilio (LJLL - Paris Diderot / University of Paris).

Petra Alexandra Morbey Ferro Gaspar Pacheco defende a dissertação "Técnicas de Álgebra Multilinear na Resolução de Problemas de Teoria Aditiva".

A sessão, no âmbito da iniciativa VEHITS 2019 - 5th International Conference on Vehicle Technology and Intelligent Transport Systems a decorrer de 03 a 05 de maio de 2019, conta com a participação dos docentes de Ciências ULisboa Carla Silva (chair

A iniciativa conta com a participação de Luís Saraiva (Ciências ULisboa).

O Tagis - Centro de Conservação das Borboletas de Portugal e os coordenadores do Projeto Europeu ABLE, em parceria com o cE3c - Centro de Ecologia, Evolução e Alterações Ambientais, Butterfly Conservation Europe e o Município de Almada, convidam todos os interessados a particip

O ISIC é uma organização sem fins lucrativos e representa o ISIC, o Cartão Internacional de Estudante - patrocinado pela UNESCO, apoiado pelo Conselho da União Europeia para a Educação, Juventude, Cultura e Desporto e diversos ministérios da educação e organiza

O Dia Aberto de Ciências realiza-se no dia 08 de maio de 2019.

As provas, requeridas por Francisco André de Campos Pereira Dionísio, decorrem nos dias 13 e 14 de maio de 2019.

No dia 14 de maio, será apreciado o sumário do seminário/lição com o título "Pathogens and parasites as effective biological weapons".

Cursos Avançados cE3c 2018/2019

Nature-based approach to Design solutions for a more resilient future aims to support societies address a variety of environmental, social and economic challenges in sustainable ways. This approach relies on actions that are inspired by, supported by or copied from Nature.

Programa Doutoral em Filosofia da Ciência, Tecnologia, Arte e Sociedade

Candidaturas a Bolsas de Doutoramento de 30 de março a 15 de maio de 2019.

Gisela Vitória Cheoo defende a dissertação "Estimation of bowhead whale (Balaena mysticetus) population density using spatially explicit capture-recapture(SECR) methods".

Candidaturas ao Programa Almeida Garrett

Candidaturas até 17 de maio de 2019 (mobilidade no 1.º semestre) e até 18 de outubro de 2019 (mobilidade no 2.º semestre).

Uma vez por mês, aos domingos de manhã, junte-se à equipa de investigadores da Lista Vermelha de Invertebrados. Participe e contribua para a amostragem da diversidade de insetos em Sítios de Importância Comunitária da Rede Natura 2000.

Candidaturas a programa de apoio ao empreendedorismo na área do mar - MARE STARTUP

A Faculdade de Ciências da Universidade de Lisboa, a Universidade Católica Portuguesa, o Fórum Oceano e a Sociedade de Avaliação Estratégica e Risco lançaram em 2015 o consórcio MARE STARTUP destinado a promover o empreendedorismo e inovação empresarial no Mar, como forma

Páginas