Seminário de Lógica Matemática

# Some arguments in proof mining

Sala 6.2.33, FCUL, 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

Um programa de formação avançada em Cibersegurança para a administração pública e o setor privado desenvolvido pelo Centro Nacional de Cibersegurança, no âmbito do Plano de Recuperação e Resiliência.

Um programa de formação avançada em Cibersegurança para a administração pública e o setor privado desenvolvido pelo Centro Nacional de Cibersegurança, no âmbito do Plano de Recuperação e Resiliência.

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.

Extended enrolement date until July 12th.

Programa brevemente disponível.

A participação na 3.ª edição do Workshop é gratuita, mediante inscrição prévia.

Are you ready for this year's edition?

Investigação Ecológica ao Serviço da Conservação

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.