Abstract
The aim of this article is to give an introduction to functional interpretations of set theory given by the authorin Burr (2000a). The first part starts with some general remarks on Gödel’s functional interpretation with a focus on aspects related to problems that arise in the context of set theory. The second part gives an insight in the techniques needed to perform a functional interpretation of systems of set theory. However, the first part of this article is not intended to be a complete survey of functional interpretations and here we recommend, for example, Avigad and Feferman (1998),Troelstra (1990) and Troelstra (1973).
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
REFERENCES
Aczel, P.: 1978, ‘The Type Theoretic Interpretation of Constructive Set Theory’, in A. McIntyre, L. Pacholski and J. Paris (eds.), Logic Colloquium ‘77 [Studies in Logic and the Foundations of Mathematics], Amsterdam.
Aczel, P.: 1982, ‘The Type Theoretic Interpretation of Constructive Set Theory: Choice Principles’, in A. S. Troelstra and D. van Dalen (eds.), The L.E.J. Brouwer Centenary Symposium [Studies in Logic and the Foundations of Mathematics 110], Amsterdam.
Avigad, J.: ‘Predicative Functionals and an Interpretation of ID<ω’, Annals of Pure and Applied Logic 92, p. 1–34
Avigad, J. and Feferman, S.: 1998, ‘Gödel's Functional (“Dialectica”) Interpretation’, in S. Buss (ed.), Handbook of Proof Theory [Studies in Logic and the Foundations of Mathematics 137], p. 337–406.
Beeson, M.: 1985, Foundations of Constructive Mathematics, Berlin.
Burr, W. and Hartung, V.: 1998, ‘A Characterization of the Σ1-definable Functions of KPω+(uniform AC)’, Archive for Mathematical Logic 37, 199–214.
Burr, W.: 1998, Functionals in Set Theory and Arithmetic, (Doctoral Thesis), Münster.
Burr, W.: 2000a, ‘Functional Interpretation of Aczel's Constructive Set Theory CZF’, Annals of Pure and Applied Logic 104, 31–73.
Burr, W.: 2000b, A Diller-Nahm Style Functional Interpretation of KPω, Archive for Mathematical Logic 39, pp. 599–604.
Buss, S. (ed.): 1998, Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics 137, Amsterdam.
Diller, J.: 1979, ‘Functional Interpretation of Heyting's Arithmetic in all Finite Types’, Nieuw Archief voor Wiskunde, Derde Serie 27, 70–97.
Diller, J. and Müller, G. H. (eds.): 1974, ‘⊨ ISLIC Proof Theory Symposium, Dedicated to Kurt Schütte on the Occasion of his 65th Birthday’, Proceedings of the International Summer Institute and Logic Colloquium, Lecture Notes in Mathematics 500, Kiel.
Diller, J. and Nahm, W.: 1974, ‘Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen’, Archiv für mathematische Logik und Grundlagenforschung 16, 49–66.
Diller, J. and Vogel, H.: 1975, ‘Intensionale Funktionalinterpretation der Analysis’, in J. Diller and G. H. Müller (eds.), ⊨ ISLIC Proof Theory Symposium, Dedicated to Kurt Schütte on the Occasion of his 65th Birthday, pp. 56–72.
Feferman, S.: 1968, ‘Ordinals Associated with Theories for one Inductively Defined Set’, unpublished.
Feferman, S. et al. (eds.): 1990, Kurt Gödel, Collected Works, Volume 2, Oxford.
Feferman, S. et al. (eds.): 1994, Kurt Gödel, Collected Works, Volume 3, Oxford.
Gödel, K.: 1941, ‘In What Sense is Intuitionistic Logic Constructive?’, in: S. Feferman et al. (eds.), Kurt Gödel, Collected Works, Volume 3, pp. 189–200.
Gödel, K.: 1958, ‘Ñber eine bisher noch nicht benützte Erweiterung des finiten Stand-punktes’, Dialectica 12, 280–287.
Goodman, N. D. and Myhill, J.: 1978, ‘Choice Implies Excluded Middle’, Zeitschrift für mathematische Logik und Grundlagen der Mathematik 24, 461.
Griffor, E. and Rathjen, M.: 1994, ‘The Strength of Some Martin-Löf Type Theories’, Archive for Mathematical Logic 3, 347–385.
van Heijenoort, J.: 1967, From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879–1931, Cambridge MA.
Hilbert, D.: 1926, Ñber das Unendliche, Mathematische Annalen 95, p. 161–190, (English translation in: J. van Heijenoort (ed.), From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879–1931, pp. 367–392.
Howard, W. A.: 1973, ‘Hereditarily Majorizable Functionals of Finite Type’, in A. S. Troelstra (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis [Lecture Notes in Mathematics 344], Berlin, pp. 454–461.
Jensen, R. B. and Karp, C.: 1971, ‘Primitive Recursive Set Functions’, in D. S. Scott (ed.), Axiomatic Set Theory, Proceedings of the Symposium in Pure Mathematics of the American Mathematical Society, held at the University of California, Los Angeles, California, July 10—August 5, 1967, Providence 1971, Proceedings of Symposia in Pure Mathematics 13, pp. 143–176.
Myhill, J.: 1975, ‘Constructive Set Theory’, Journal of Symbolic Logic 40, 347–382.
Rathjen, M.: 1992, ‘A Proof-Theoretic Characterization of the Primitive Recursive Set Functions’, Journal of Symbolic Logic 57, 954–969.
Shoenfield, J. R.: 1967, Mathematical Logic, Reading MA.
Troelstra, A. S. and van Dalen, D.: 1988, Constructivism in Mathematics — Volumes I and II [Studies in Logic and the Foundations of Mathematics 123], Amsterdam.
Troelstra, A. S. (ed.): 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Berlin, Lecture Notes in Mathematics 344.
Troelstra, A. S.: 1990, ‘Introductory Note to 1958 and 1972’, in Kurt Gödel, Collected Works, Volume 2, pp. 217–241.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Burr, W. Concepts and aims of functional interpretations: towards a functional interpretation of constructive set theory. Synthese 133, 257–274 (2002). https://doi.org/10.1023/A:1020844128690
Issue Date:
DOI: https://doi.org/10.1023/A:1020844128690