Functional interpretations. From the Dialectica interpretation to interpretations of classical and constructive set theory (Q2836179)

This is a comprehensive monograph on functional interpretations, starting with Gödel's Dialectica interpretation and ending with functional interpretations of various intuitionistic set theories. It is divided into three chapters. NEWLINENEWLINEThe first one, 111 pages long, deals with arithmetic. It presents NEWLINE(i) the starting point of the entire enterprise, Gödel's Dialectica interpretation of Heyting arithmetic (HA), which translates nested quantification into higher-type operations, thereby reducing the consistency problem for arithmetic to the problem of computability of primitive recursive functionals of finite types, NEWLINE(ii) the \(\wedge\)-interpretation (or Diller-Nahm interpretation, as it was introduced in [\textit{J. Diller} and \textit{W. Nahm}, Arch. Math. Logik Grundlagenforsch. 16, 49--66 (1974; Zbl 0277.02006)] of Heyting arithmetic in finite types \(HA^{\omega}\), NEWLINE(iii) \textit{Kreisel}'s modified realizability, introduced in [in;Constructivity in mathematics. Proceedings of the colloquium, held at Amsterdam, 1957. Amsterdam: Elsevier. 101--128 (1959; Zbl 0134.01001) and extended by \textit{A. S. Troelstra} [in: Proceedings of the second Scandinavian logic symposium. Amsterdam-London: North-Holland Publishing Company. 369--405 (1971; Zbl 0227.02015); Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard. Berlin-Heidelberg-New York: Springer-Verlag (1973; Zbl 0275.02025)], and [\textit{S. R. Buss} (ed.), Handbook of proof theory. Amsterdam: Elsevier (1998; Zbl 0898.03001)], NEWLINE(iv) hybrids of the \(\wedge\)-interpretation, and NEWLINE(v) both Dialectica and \(\wedge\)-interpretation in the classical setting, with PA and various extensions replacing HA and its extensions. NEWLINENEWLINEThe second chapter, 24 pages long, is devoted to analysis and the extension of the \(\wedge\)-interpretation to analysis, in the manner inaugurated in \textit{J. Diller} and \textit{H. Vogel} [Lect. Notes Math. 500, 56--72 (1975; Zbl 0323.02047)], together with a proof, following \textit{H. Vogel} [Arch. Math. Logik Grundlagenforsch. 18, 81--84 (1976; Zbl 0352.02035)]. of the strong computability of bar recursion functionals. NEWLINENEWLINEChapter 3, 73 pages long, is devoted to set theory, in the versions of Kripke-Platek set theory in finite types (with Dialectica and \(\wedge\)-interpretations, the latter due to \textit{W. Burr} [Arch. Math. Logic 39, No. 8, 599-604 (2000; Zbl 0968.03066)]).and constructive Zermelo-Fraenkel set theory in all finite types [\textit{D. Schulte}, J. Appl. Log. 6, No. 3, 443-458 (2008; Zbl 1156.03052; \textit{J. Diller} [``Functional interpretations of constructive set theory in all finite types'', Dialectica 62, No. 2, 149--177 (2008; \url{doi:10.1111/j.1746-8361.2008.01133.x})].NEWLINENEWLINEThe author succeeds in presenting a significantly simplified, streamlined, and minimalist version of the theory of functional interpretations, presenting numerous simplifications of the papers cited above. There is no mention of the prerequisites the prospective reader should come with to the study of this book. The reviewer believes that [\textit{J. Avigad} and \textit{S. Feferman}, Stud. Logic Found. Math. 137, 337--405 (1998; Zbl 0913.03053); \textit{A. S. Troelstra} and \textit{D. van Dalen}, Constructivism in mathematics. An introduction. Volume I \& II. Amsterdam etc.: North-Holland (1988; 0653.03040 Zbl 0661.03047)] should prepare the reader for the very demanding task of navigating this monograph.