What is Godels Dialectica Interpretation?
In 1958 Godel published an interesting note in the philosophical journal Dialectica, giving a consistency proof for arithmetic that he had first developed in the early 1940’s. This short, deceptively simple, paper has greatly influenced modern constructive mathematics, proof theory, and lambda calculus, and indeed categorical logic. In particular, some of the “classic” papers by Tait, Spector, and Girard, as well as works by Prawitz, Troelstra, and Bishop, come directly from contemplating Godel’s Dialectica paper. More recently, it has been used by S. Cook and A. Urquhart for analyzing bounded arithmetical theories. The many footnotes added by Godel have a decidely “modern” flavour, and suggest Godel even had a “game-theoretic” intuition of his work. In my own case, it was explicitly to understand the underlying principles of the Dialectica Interpretation that Lambek and I wrote our 1986 book on categorical logic. I’ll give a brief historical tour of Godel’s paper. • 22 February Peter
