By Pedro Pinto (Technische Universitat Darmstadt).

Abstract: The classical bounded functional interpretation [1] was recently shown to be a valid technique to employ in the proof mining practice [2][3]. In this talk, I will discuss some subtle features of recent "minings" guided by this functional interpretation. I will talk about the quantitative version of the metric projection argument. Next, we will look at the quantitative treatment of a nontrivial discussion by cases and how it guided the recent analysis in [4]. We finish with some brief considerations about metastability results.

[1] F. Ferreira, Injecting uniformities into Peano Arithmetic, Annals of Pure and Applied Logic, 157 (2009), pp. 122–129.
[2] F. Ferreira, L. Leustean, and P. Pinto, On the removal of weak compactness arguments in proof mining, Advances in Mathematics, 354 (2019).
[3] P. Pinto, Proof mining with the bounded functional interpretation, PhD thesis, Universidade de Lisboa, 2019.
[4] B. Dinis and P. Pinto, Quantitative results on the multi-parameters proximal point algorithm, arXiv preprint 1912.10175, (2019).