Por Paulo Firmino (Faculdade de Ciências da Universidade de Lisboa).
Abstract: Functional interpretations date back to 1958 with Gödel’s seminal paper [5] and the introduction of what is now known as the Dialectica interpretation. This presentation does not aim to be a review of functional interpretations. Rather, we intend it to be an introduction to our recent work on a new approach to functional interpretations in the context of pure logic, namely semi-intuitionistic logic and intuitionistic logic [4], as well as a herbrandized version of modified realizability [3], with the introduction of star types. Functional interpretations are the main tool of the research program of proof mining [6], which aims to extract computational information from mathematical proofs. We make reference to Kohlenbach’s monotone functional interpretation and the bounded functional interpretation by F. Ferreira and Oliva [2]. We highlight the application of proof mining in the domain of iterative arguments in nonlinear analysis, with the extraction of effective uniform rates of asymptotic regularity and rates of metastability for various iterative methods.
References:
- [1] F. Ferreira, G. Ferreira. A herbrandized functional interpretation of classical first-order logic. Archive for Mathematical Logic (2017) 56:523–539
- [2] F. Ferreira, P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135(1–3), 73–112, 2005
- [3] G. Ferreira, P. Firmino. Herbrandized modified realizability. Archive for Mathematical Logic (2024) 63:703–721
- [4] P. Firmino. Functional interpretations over finite types with star types. (in preparation)
- [5] K. Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12(3–4), 280–287, 1958
- [6] U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. 2008, Springer
