Page 47 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 39
The above book includes the contribution of William Howard where he intro- duced the majorizability relations and discussed the axioms of extensionality. Marc Bezem’s modification of Howard’s majorizability relations appears in
M. Bezem. Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. The Journal of Symbolic Logic, 50:652–660, 1985.
The structure of the countable/continuous functionals is independently due to Kleene and Kreisel:
S. Kleene. Countable functionals. In A. Heyting (editor), Constructivity in Mathe- matics, pp. 81–100, North-Holland, 1959.
G. Kreisel. Interpretation of analysis by means of constructive functionals of finite type. Ibidem, pp. 101–128.
The latter paper is also famous for advancing a constructive interpretation of analysis (ultimately doomed) in terms of continuous and recursively continu- ous functionals (i.e., continuous functionals which have at least one recursive associate). A nice and informative book on countable functionals appeared in 1980:
D. Normann. Recursion on the Countable Functionals. Lecture Notes in Mathematics. Springer, Berlim, 1980.
More recently, Dag Normann wrote a survey article where the reader can find new developments and more recent bibliography:
D. Normann. The continuous functionals. In E. R. Griffor (ed.), Handbook of Com- putability Theory, Studies in Logic and the Foundations of Mathematics, vol. 140, pp. 251–275. North Holland, Amsterdam, 1999.
The original result of Kreisel, Lacombe and Shoenfield appeared in
G. Kreisel, D. Lacombe and J.R. Shoenfield. Partial recursive functionals and effective operations. In A. Heyting (editor), Constructivity in Mathematics, Appendix, pp. 290–297, North-Holland, 1959.
A generalization of this result is due to Ulrich Berger in
U. Berger. Total sets and objects in domain theory. Annals of Pure and Applied Logic, 60: 91–117. 1993.
The α-normalization calculus is due to William Tait in
W. Tait. Intensional interpretations of functionals of finite type I. The Journal of
Symbolic Logic, 32: 198–212. 1967.
The study of fragments of arithmetic in the setting of the Dialectica interpreta- tion is the work of Charles Parsons: