- This event has passed.
Unwinding of proofs
March 4, 2021 @ 10:00 am - 12:00 pm
Title: Unwinding of proofs
Speaker: Pedro Pinto (TU Darmstadt)
Abstract:
The unwinding of proofs program dates back to Kreisel in the fifties and rests on the following broad question: “What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?”
This research program has since been dubbed proof mining and has been greatly developed during the last two decades and emerged as a new form of applied proof theory [1,2]. Through the use of proof-theoretical tools, the proof mining program is concerned with the unveil of hidden finitary and combinatorial content from proofs that use infinitary noneffective principles.
In this talk, we set out to give a brief introduction to the proof mining program, focusing on the following points:
- functional interpretations in an introductory way;
- the bounded functional interpretation [3,4];
- a concrete translation example: the metric projection argument.
We finish with a brief discussion of some recent results [5,6].
References:
[1] U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008.
[2] U. Kohlenbach. Proof-theoretic methods in nonlinear analysis. In M. Viana B. Sirakov, P. Ney de Souza, editor, Proceedings of the International Congress of Mathematicians – Rio de Janeiro 2018, Vol. II: Invited lectures, pages 61–82. World Sci. Publ., Hackensack, NJ, 2019.
[3] F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135:73-112, 2005.
[4] F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157:122-129, 2009.
[5] B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. arXiv:2101.12675 [math.FA], 2021.
[6] U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA], 2021.
[2] U. Kohlenbach. Proof-theoretic methods in nonlinear analysis. In M. Viana B. Sirakov, P. Ney de Souza, editor, Proceedings of the International Congress of Mathematicians – Rio de Janeiro 2018, Vol. II: Invited lectures, pages 61–82. World Sci. Publ., Hackensack, NJ, 2019.
[3] F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135:73-112, 2005.
[4] F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157:122-129, 2009.
[5] B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. arXiv:2101.12675 [math.FA], 2021.
[6] U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA], 2021.
References: