Page 49 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 41
U. Kohlenbach. Proof Interpretations and the Computational Content of Proofs. Draft in progress available at: http://www.mathematik.tu-darmstadt.de/˜kohlenbach/.newcourse.ps.gz.
The bounded interpretations were introduced in
F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135:73–112, 2005.
F. Ferreira and A. Nunes. Bounded modified realizability. The Journal of Symbolic Logic, 71:29-346, 2006.
The bounded interpretations were originally motivated by applications of ma- jorizability considerations to the feasible setting. Already in the early nineties, Stephen Cook and Alasdair Urquhart extended G¨odel’s interpretation to the feasible setting:
S. Cook and A. Urquhart. Functional interpretations of feasibly constructive arith- metic. Annals of Pure and Applied Logic, 63:103–200, 1993.
There are indeed applications of the bounded functional interpretation to the feasible setting:
F. Ferreira and P. Oliva. Bounded functional interpretation and feasible analysis. To appear in Annals of Pure and Applied Logic.
Clifford Spector’s seminal work on bar recursion is the following:
C. Spector. Provably recursive functionals of analysis: a consistenct proof of analysis by an extension of principles formulated in current intuitionistic mathematics. Recur- sive Function Theory: Proc. Symposia in Pure Mathematics (ed. J. C. E. Dekker). American Mathematical Society, Rhode Island, pp. 1-27, 1962.
Modified bar recursion was introduced in
P. Oliva and U. Berger. Modified bar recursion and classical dependent choice. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic: Logic Colloquium 2001 (eds. M. Baaz, S. Friedman and J. Kraj´ıcek). Lecture Notes in Logic, vol. 20, pp. 89-107, 2005.
Acknowledgments
The text presented here is a somewhat longer and more detailed version of the actual presentations given in Coimbra during the meeting Days in Logic’ 06 at the end of January 2006. I want to thank the organizers of the meeting Reinhard Kahle, Isabel Oitavem and Gon¸calo Gutierres without whose invita- tion I would not have found the drive to write these lectures. I must also thank