Page 46 - Textos de Matemática Vol. 38

38 FERNANDO FERREIRA
Annotated bibliography
The notion of realizability was introduced by Stephen Kleene in
S. C. Kleene. On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10:109–124, 1945.
It was subsequently modified by Georg Kreisel for the setting of finite type functionals in
G. Kreisel. On weak completeness of intuitionistic predicate logic. The Journal of Symbolic Logic, 27:139–158, 1962.
Go¨del’s Dialectica interpretation (functional interpretation) together with the notion of computable functional of finite type appeared in
K. Go¨del. U¨ber eine bisher noch nicht benu¨tzte Erweiterung des finiten Standpunk- tes. Dialectica, 12:280–287, 1958. Engish translation in Kurt G¨odel Collected Works II, pp. 241–251, Oxford University Press, New York, 1990.
Both the realizability and functional interpretations were adapted and extended to stronger and weaker theories. There are two relatively recent surveys on these issues, with pertinent bibliography:
A. S. Troelstra. Realizability. In S. R. Buss (ed.), Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, pp. 408–473. North Holland, Amsterdam, 1998.
J. Avigad and S. Feferman. G¨odel’s functional (“Dialectica”) interpretation. Ibi- dem, pp. 337–405.
The program of Reverse Mathematics was created by Harvey Friedman and Stephen Simpson. If the reader wants to learn about the aims of the program and its accomplishments, he would do well in consulting
S. G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer, Berlim, 1999.
The following book is more than three decades old but it is still necessary reading for the traditional interpretations, including their models (the strong normalization theorem for G¨odel’s T seems to have been proved here for the first time):
A. S. Troelstra (editor). Metamathematical Investigation of Intuitionistic Arith- metic and Analysis Lecture Notes in Mathematics, vol. 344. Springer, Berlim, 1973.