The philosophical significance of Gödel's _Dialectica_ interpretation

Hilbert's Program in the 1920s aimed to give finitary consistency proofs for infinitary mathematics, thus putting infinitary mathematics on a more secure footing. There is a popular narrative that Hilbert's Program was decisively refuted by Gödel's incompleteness theorems in 1931. However, Gödel himself, in a remarkable paper of 1958, pursues a modified version of Hilbert's Program: he presents his Dialectica interpretation as a new, Hilbert‐style consistency proof for arithmetic based on “an extension of the finitary standpoint,” and he clearly regards this proof as epistemologically significant. In this essay, I explain and assess the epistemological project that Gödel sets out in his Dialectica paper. Ultimately, I argue that the Dialectica interpretation is best understood, not as a consistency proof, but as a way of assigning a constructive meaning to arithmetic.