In the Shadow of Incompleteness: Hilbert and Gentzen

Godel’s incompleteness theorems had a dramatic impact on Hilbert’s foundational program. That is common lore. For some, e.g. von Neumann and Herbrand, they undermined the finitist consistency program; for others, e.g. Godel and Bernays, they left room for a fruitful development of proof theory. This paper aims for a nuanced and deepened understanding of how Godel’s results effected a transformation of proof theory between 1930 and 1934. The starting-point of this transformative period is Godel’s announcement of a restricted unprovability result in September of 1930; its end-point is the completion of Gentzen’s first consistency proof for elementary number theory in late 1934. Hilbert, surprisingly, is the initial link between starting-point and end-point. He addressed Godelian issues in two strikingly different papers, (1931a) and (1931b), without mentioning Godel. In (1931a) he takes on the challenge of the restricted unprovability result; in (1931b) he responds to the second incompleteness theorem concerning the unprovability of consistency for a system S in S. He does so by bringing in semantic considerations and by pursuing novel, but also highly problematic directions: he argues for the contentual correctness of a constructive (for him, finitist) theory that includes intuitionist number theory. Gentzen followed the new directions in late 1931, addressed methodological issues and metamathematical problems in ingenious ways, while building on ideas and techniques that had been introduced in proof theory. Most distinctive is Gentzen’s struggle with contentual correctness and its relation to consistency. That is reflected in a sequence of notes Gentzen wrote between late-1931 and late-1934, but it is also central in his classical paper (1936). The immediate lessons seem to be: (i) there is real continuity between Hilbert’s proof theory and Gentzen’s work, and (ii) there is deepened concern for interpreting intuitionist arithmetic (and thus understanding classical arithmetic) from a more strictly constructive perspective. Ironically, the latter concern deeply influenced Godel’s functional interpretation of intuitionist arithmetic.