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

Seminário do Centro de Estatística e Aplicações da Universidade de Lisboa e do Centro de Matemática Computacional e Estocástica, por Alejandra Andrea Tapia Silva (Pontificia Universidad Católica de Chile).

Iconografia diversa relacionada com a cidade de Lisboa

Um manual dirigido a docentes do 3.º Ciclo do Ensino Básico e do Ensino Secundário, que propõe atividades teórico-práticas interdisciplinares nas áreas do Desenvolvimento Sustentável, Biotecnologia e Bioeconomia Circular.

Seminários por estudantes do Mestrado em Matemática de CIÊNCIAS.

Logótipo, data e local do evento

Com o tema “Ciência, Inovação e Sociedade”, o encontro será um palco de promoção e discussão do impacto científico, social, cultural e económico da investigação em Portugal.

Título e local do evento

O evento visa promover o diálogo interdisciplinar sobre estruturas de proteínas, doenças conformacionais e tecnologias baseadas em proteínas.

Computabilidade na Europa (CiE) - uma série interdisciplinar de conferências internacionais organizada pela Associação Computabilidade na Europa (ACiE).

Título/data do evento e vários objetos museológicos

Este curso visa fornecer uma visão atualizada do potencial das coleções museológicas para a investigação da biodiversidade. Mais especificamente, pretende apresentar estudos de caso sobre o valor dos museus e a utilização de coleções e espécimes no século XXI, utilizando novas tecnologias e métodos analíticos.

Horta Solar

E se fosse possível experimentar um curso universitário antes de concorrer ao ensino superior? Agora já é!

Banner Meredith Ringel Morris HCI for AGI

15 de julho: É com enorme entusiasmo que CIÊNCIAS recebe a investigadora de renome internacional Meredith R. Morris, Diretora de Investigação em Interacção Humano-IA na Google DeepMind e Professora Afiliada na Universidade de Washington, para uma palestra imperdível sobre um dos temas mais debatidos e transformadores da atualidade: o caminho rumo à Inteligência Artificial Geral (AGI).

Águas subterrâneas

Curso acreditado para efeitos de progressão na carreira dos professores na dimensão cientifico-pedagógica dos grupos 420 e 520.

Título e datas do programa de estágios

Preparados para explorar a investigação de perto?

Um workshop com o objetivo de reunir académicos que abordam a história da ecologia - e a evolução da própria disciplina - a partir de uma variedade de perspetivas.

Orquestra

Concerto no âmbito do programa Música na Universidade de Lisboa,

A 10.ª edição do Ser Cientista realiza-se entre 21 e 25 de julho - vem investigar connosco!

Pormenor de lâmpada

Candidaturas a decorrer de 01 a 30 de setembro.

Microplásticos no ocerano

O curso procura dar formação sobre a problemática da contaminação por detritos de plástico dos nossos ecossistemas, bem como alertar para os potenciais efeitos deletérios nos organismos, utilizando uma abordagem de ensino científico, com um discurso adequado a formandos sem formação científica - candidaturas até 03 de agosto.

Logótipo do evento, sobre fotografia dos Açores

Um simpósio internacional que reúne investigadores especializados em várias disciplinas (taxonomia, ecologia da vegetação, biogeografia, filogeografia, paleoecologia ou conservação da biodiversidade), focados na flora e vegetação terrestre e marinha da região da Macaronésia (Açores, Madeira, Selvagens, Canárias e Cabo Verde).

Quatro investigadores num laboratório

O curso visa capacitar investigadores, docentes e técnicos para integrar os princípios da economia circular em ambientes laboratoriais académicos - candidaturas até 16 de setembro.

Três investigadores num laboratório

O curso visa capacitar profissionais para aplicar os princípios da economia circular em ambientes laboratoriais industriais, promovendo práticas sustentáveis e eficientes - candidaturas até 17 de setembro.

Composição de imagens relativas à área das ciências forenses

O curso visa dotar os formandos com os conhecimento necessários à integração de equipas profissionais multidisciplinares nas áreas Médico-Legais e Forenses, em Laboratórios ou Serviços Médico-Legais e Forenses - candidaturas até 27 de julho.

Logótipo do evento

Physics Day é um evento promovido pelo Departamento de Física da Faculdade de Ciências da ULisboa, com um duplo objetivo: valorizar a diversidade e excelência da formação dos doutorados e promover um espaço de diálogo direto entre empresas e estudantes.

Cientista a trabalhar com tubos de ensaio

Os participantes neste curso irão adquirir os conhecimentos essenciais à integração de equipas profissionais multidisciplinares na área das Análises Clínicas/Patologia Clínica, em laboratórios privados, públicos, hospitalares ou do Estado - candidaturas até 27 de julho.

Saída de campo (Geologia)

O curso, com candidaturas até 20 de julho, convida os professores do Ensino Básico e Secundário a explorar a Geologia a partir das rochas que afloram nas imediações da sua escola.

Gotas de água

O curso visa capacitar os formandos para a aplicação dos índices de qualidade ecológica utilizados na avaliação da qualidade ambiental em sistemas de transição, no âmbito da Diretiva Quadro da Água (DQA) - candidaturas até 31 de agosto.

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.

Páginas