Abstract:

This paper deals with the attempts to characterize the set of all proofs in a given mathematical domain such as geometry or number theory. The characterization usually takes the form of a finite list of axiom schemata and inference rules, which is thought to be complete. A related effort, which originated with descartes, is to replace proofs - that is, reasoning about concepts and relations - by the solution of algebraic equations which are shown to be equivalent to the proofs. These formalist tendencies have always been opposed by intuitionists. I trace the dispute from descartes and Leibnitz through Kant all the way to its climax in the fifty years between the demonstration of the relative consistency of hyperbolic geometry and the discovery of Godel's theorems. My purpose is both historical and philosophical. On the historical level, I argue that Hilbert's program was not only a foundationalist effort to secure the consistency of mathematics. It was, in addition, an internal mathematical program in the aforementioned cartesian tradition of replacing proofs by computations. The demise of Hilbert's philosophical pretensions brought considerable and unexpected success to the mathematical program: Godel's theorem, which shows how to replace proofs by computations in very extensive domains of mathematics, and, ultimately, the Davis-Robinson-Putnam-Matijacevic theorem, which demonstrates, roughly, that every proof in those domains is equivalent to a solution of an algebraic (i.e. polynomial) equation. The fact that the notion of proof in number theory is indefinitely extensible (by Godel's theorem) depends on a complete characterization of the concept of `computation' (the Church-Turing thesis). On the philosophical level, I argue that this dependence undermines some contemporary intuitionist claims (by Weyl and Dummett) which are based on Godel's results.