Gödel’s paper containing his so-called Dialectica interpretation was published 50 years ago in, well, Dialectica. And so Dialectica has a special issue on Gödel’s Dialectica interpretation, edited by Thomas Strahm. It looks like all the articles are freely available. Here’s (most of) the introduction:
Gödel’s famous dialectica paper (1958), entitled ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’, was published in a special issue of this journal in 1958 in honour of Paul Bernays’ 70th birthday. In the past fifty years, the dialectica interpretation proposed by Gödel has become one of the most fundamental conceptual tools in logic and the foundations of mathematics. This special issue traces some of the fundamental issues and applications of Gödel’s interpretation. The ideas of Gödel’sdialectica interpretation date back at least as far as 1941, when Gödel presented them in a lecture to the mathematics and philosophy clubs at Yale University. The Yale lecture was entitled ‘In What Sense is Intuitionistic Logic Constructive?’ and can be found in Volume III of the Collected Works (1994). Prior to the Yale lecture, Gödel had delivered two addresses where he raised important thoughts towards the dialectica interpretation: an invited lecture given in 1933 in Cambridge, Massachusetts entitled ‘The Present Situation in the Foundations of Mathematics’ and an informal seminar in 1938 ‘Vortrag bei Zilsel’ delivered in Vienna. The full history of the dialectica paper is presented by Feferman (1993) and Troelstra (1990).
Let us briefly summarize the main rationale of Gödel’s dialectica interpretation. In its most elementary form, it provides an interpretation of intuitionistic number theory in a quantifier-free theory of functionals of finite type. Together with Gödel’s double-negation interpretation from classical arithmetic into its intuitionistic counterpart, the dialectica interpretation also provides a reduction of classical arithmetic. Gödel’s functional interpretation can be seen as a possible realization of the so-called modified Hilbert program in the sense that it enables a reduction of a classical system to a quantifier-free theory of functionals of finite type, thereby reducing the consistency problem for the classical theory to the consistency of a quantifier-free system of higher-type recursion, the latter being informally more finitistic and sufficiently well understood.
Gödel’s interpretation of arithmetic has been substantially extended in the past fifty years both to stronger and weaker theories. In particular, versions of the dialectica interpretation have been proposed for impredicative classical analysis, subsystems of classical arithmetic, theories of ordinals, predicative subsystems of second order arithmetic, analysis with game quantifiers, systems of feasible arithmetic and analysis, admissible and constructive set theories, as well as iterated arithmetical fixed point theories. A comprehensive survey of many of these results can be found in Avigad and Feferman (1995) as well as Troelstra (1973). In more recent years, work on functional interpretations has shifted from purely foundational purposes to applications to concrete proofs in mathematics in the sense of Kreisel’s unwinding program. In connection with this, Kohlenbach’s proof mining program provides very impressive results making use of variants of Gödel’s dialectica interpretation, see his article in this special issue.
Let us now give a brief survey of the articles contained in this special issue.
The paper by Justus Diller gives a broad survey of functional interpretations in the context of constructive set theories and elaborates in detail on the logical problems one has to solve in order to provide such interpretations of set theory. In addition, a new simplified interpretation, the so-called ∧-interpretation, is proposed and analyzed. It is rooted in the Diller-Nahm interpretation of 1974.
Solomon Feferman’s paper gives a vivid account of Gödel’s views on finitism, constructivity and Hilbert’s program, using unpublished articles and lectures as well as Gödel’s correspondence with Paul Bernays. Feferman’s article contains a full section on the dialectica interpretation and on Gödel’s influential Cambridge lecture mentioned above.
Fernando Ferreira’s article gives an informal analysis of Gödel’s dialectica interpretation and presents a balanced mixture between philosophical discussions and technical issues. The paper starts off by a discussion of Gödel’s use of higher types and the relationship to his set-theoretic realism. Further investigations of the paper include the validation of additional principles, higher order equality and monotone functional interpretations.
As already mentioned above, Ulrich Kohlenbach’s article is centred on recent topics in applied proof theory and, in particular, his recent program of proof mining. His paper focuses on the logical aspects of his program and, in particular, on the systematic design and study of variants of the dialectica interpretation, which have been used in applications to concrete proofs from various areas of mathematics.
Finally, Paulo Oliva’s article provides a detailed analysis of Gödel’s dialectica interpretation via linear logic. The latter comes naturally into the picture of Gödel’s interpretation, since contraction is the main source of its asymmetry. The paper analyses various properties of the dialectica interpretation, e.g. the characterization theorem, within the context of linear logic.