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
Astronauta, banhado pela luz solar, no meio de uma floresta

Candidaturas até 30 de julho - um evento único, que reunirá estudantes de mestrado e doutoramento com investigadores e líderes da indústria de toda a Europa para uma experiência inesquecível.

Lupa e caneta sobre página com texto e gráfico

O curso visa dar formação inicial a estudantes de pós-graduação sobre o processo de escrita, submissão e publicação de trabalhos científicos, focando principalmente a publicação de artigos científicos em revistas internacionais com revisão por pares.

Iconografia relacionada com a temática do curso

O curso fornece uma exploração aprofundada de isótopos estáveis como uma ferramenta valiosa em Ecologia, usando assinaturas isotópicas para rastrear processos ecológicos e revelando insights sobre o ciclo de nutrientes e água, interações de espécies e condições ambientais em diversos ecossistemas e comunidades.

Composição de três imagens relativas à área da deteção remota

2.ª edição do curso, com candidaturas até 18 de outubro.

O evento pretende reunir investigadores que trabalhem sobre temas ligados à indústria e sobre património técnico e industrial, para uma reflexão prospetiva sobre o património industrial e atuais vias de colaboração no seu estudo, salvaguarda e preservação.

Computador portátil a projetar imagem de sequência biológica

O curso visa a aquisição de conhecimentos sobre as ferramentas bioinformáticas disponíveis para efetuar análises de sequências de DNA e proteínas, bem como a autonomia e espírito crítico na utilização dessas ferramentas. Procura igualmente desenvolver competências na utilização de software de bioinformática disponível gratuitamente na Internet e na interpretação do significado biológico dos resultados.

Bola de cristal colocada no solo

O curso tem como objetivo apresentar aos participantes um estado da arte atualizado sobre a diversidade da biota do solo e os papéis funcionais desempenhados pelos organismos do solo nos principais processos ecológicos.

A conferência visa reunir os principais especialistas no domínio da Imagiologia Médica por Micro-ondas (MMWI) e incluirá palestras, apresentações e pósteres de resumos revistos por pares e artigos de conferências, bem como workshops em áreas satélite de investigação com interesse para a investigação em MMWI.

Páginas