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
Logótipo ERC - European Research Council

Ciclo de sessões de divulgação das oportunidades ERC - European Research Council para 2020.

 

ERC Days @ Porto, 25 e 26 de junho

Ações de Formação Pedagógica para Docentes

O objetivo deste curso é apoiar o desenvolvimento docente, incentivando a reflexão sobre estratégias de ensino que podem ser utilizadas no ES.

Por Byungnam Kahng (Department of Physics and Astronomy, Seoul National University).

Por Fabio Deelan Cunden (University College Dublin).

João de Sousa Alves defende a dissertação "CAN FD: a communication network for future avionic systems".

Almoços com Ciências

Especialistas de Ciências ULisboa conversam informalmente sobre temas atuais, durante o almoço.

Por Cristiana Palmela Pereira (Faculdade de Medicina Dentária da Universidade de Lisboa).

The main goal of this 2-days workshop is to gather  researchers, post-docs and students from all Europe, working on Planetary Science studies to discuss about several topics related with Planetary Atmospheres (including exoplanets), and promote collaborations on the basis

Ciclo de colóquios no âmbito da Exposição "E3 - Einstein, Eddington e o Eclipse"

Colóquio por Marta Macedo (Instituto de Ciências Sociais, Universidade de Lisboa).

O evento conta com a participação, na qualidade de keynote speaker, de Filipe Duarte Santos (Ciências ULisboa).

Conferências CIUHCT "Ricardo Carlos Smith, a forgotten pioneer of Portuguese horticulture"

As Conferências do CIUHCT são um ciclo de palestras organizado anualmente pelo CIUHCT acerca de assuntos de História das Ciências e da Tecnologia.

Logotipo Lisboa 2020

O Programa Lisboa 2020 abre concursos para Investimentos em Infraestruturas Tecnológicas.

Frontiers in E3: 5th cE3c Annual Meeting

The cE3c 5th Annual Meeting will take place on July 1-2 2019, at the National Museum of Natural History and Science.

Verão na ULisboa 2019

A edição de 2019 da iniciativa Verão na ULisboa decorre nas semanas de 01 a 05 de julho (alunos do 10.º,11.º e 12.º ano) e de 08 a 12 de julho (alunos do 7.º, 8.º e 9.º ano).

As provas, requeridas por José Manuel Lourenço Coutinho Afonso, decorrem nos dias 01 e 02 de julho de 2019.

Cursos Avançados cE3c 2018/2019

Under the general framework of Global Change Ecology, the goal of this course is to provide the participants with the most recent and practical knowledge on the use of Functional Diversity.

Ciclo de colóquios no âmbito da Exposição "E3 - Einstein, Eddington e o Eclipse"

Colóquio por Duarte Pape (Paralelo Zero).

Doutoramento em História e Filosofia das Ciências

Doutorando: Luís Miguel Campos Ribeiro.

Tema da tese e alvo de discussão oral: O candidato apresentará o Seminário Doutoral III.

Ciência 2019 - Encontro com a Ciência e Tecnologia em Portugal

O evento procura reunir a comunidade científica em torno de um programa multidisciplinar que aborda os desafios científicos e societais atuais, tendo por base os 17 Objetivos de

Cursos Avançados cE3c 2018/2019

Currently, climate changes or alterations are known to be reflected on the stable isotope ratios of Hydrogen, Nitrogen, Carbon, Oxygen and Sulphur present in atmospheric gas forms, fresh or ocean water, as well as in plants and animals and organic matter in the soil.

Izabella Campolina Silva e Hemprich apresenta o trabalho de projeto "Consortia optimization for European Space Agengy proposals based on cognitive computing".

Escola de Verão de Energia

Imagina que era possível experimentar um curso universitário antes de concorreres ao ensino superior.

Páginas