Gödel and the metamathematical tradition

Summary

Abstract. The metamathematical tradition that developed from Hilbert's program is based on syntactic characterizations of mathematics and the use of explicit, finitary methods in the metatheory. Although Gödel's work in logic fits squarely in that tradition, one often finds him curiously at odds with the associated methodological orientation. This essay explores that tension and what lies behind it.

§1. Introduction. While I am honored to have been asked to deliver a lecture in honor of the Kurt Gödel centennial, I agreed to do so with some hesitations. For one thing, I am not a historian, so if you are expecting latebreaking revelations from the Gödel Nachlass you will be disappointed. A more pressing concern is that I am a poor representative of Gödel's views. As a proof theorist by training and disposition, I take myself to be working in the metamathematical tradition that emerged from Hilbert's program; while I will point out, in this essay, that Gödel's work in logic falls squarely in this tradition, one often senses in Gödel a dissatisfaction with that methodological orientation that makes me uneasy. This is by no means to deny Gödel's significance; von Neumann once characterized him as the most important logician since Aristotle, and I will not dispute that characterization here. But admiration does not always translate to a sense of affinity, and I sometimes have a hard time identifying with Gödel's outlook.