Page 48 - Textos de Matemática Vol. 38

40 FERNANDO FERREIRA
C. Parsons. On n-quantifier induction. The Journal of Symbolic Logic, 37:466–482, 1972.
Horst Luckhardt’s technique of elimination of extensionality appeared in
H. Luckhardt. Extensional G¨odel Functional Interpretation: A Consistency Proof of Classical Analysis, Lecture Notes in Mathematics, vol. 306. Springer, Berlin, 1973.
In the nineties, Ulrich Kohlenbach began urging a shift of attention in Proof In- terpretations from the obtaining of precise witnesses to the obtaining of bounds for these witnesses. The relaxation of the goal permitted Kohlenbach to define monotone interpretations and be able to deal with non-constructive principles like weak K¨onig’s lemma. The monotone interpretations are still based on the traditional assignments of formulas, but differ from realizability and the Dialec- tica interpretation in that the conclusion of the soundness theorem is relaxed. The original papers, where Kohlenbach introduced monotone realizability and monotone functional interpretations are (respectively):
U. Kohlenbach. Relative constructivity. The Journal of Symbolic Logic, 63:1218– 1238, 1998.
U. Kohlenbach. Analysing proofs in analysis. In W. Hodges, M. Hyland, C. Stein- horn, and J. Truss (editors), Logic: from Foundations to Applications, pp. 225–260. European Logic Colloquium (Keele, 1993), Oxford University Press, 1996.
The principles of uniform boundedness were introduced and studied in the clas- sical setting in
U. Kohlenbach. The use of a logical principle of uniform boundedness in analysis. In Cantini, A. and Casari, E. and Minari, P. (editors), Logic and Foundations of Mathematics, pp. 93–106. Synthese Library, Kluwer Academic Publishers, Dordrecht, 1999.
Ulrich Kohlenbach and his students have been using the technique of monotone functional interpretation to analyze proofs mathematical theorems, in search of concrete new computational information (this program has been dubbed Proof Mining). A good introduction to proof mining is
U. Kohlenbach and P. Oliva. Proof mining: a systematic way of analysing proofs in mathematics. Proceedings of the Steklov Institute of Mathematics, 242:136–164, 2003.
Proof Mining was recently extended to new base types:
U. Kohlenbach. Some logical metatheorems with applications in functional analysis. Transactions of the American Mathematical Society, 357:89–128, 2005.
Kohlenbach is writing a book on interpretative proof theory where he addresses the traditional material, the monotone interpretations and proof mining. The draft of the book is available in the internet: