In the 1920s, David Hilbert proposed a research program with the aim of providing mathematics with a secure foundation. This was to be accomplished by first formalizing logic and mathematics in their entirety, and then showing---using only so-called finitistic principles---that these formalizations are free of contradictions. ;In the area of logic, the Hilbert school accomplished major advances both in introducing new systems of logic, and in developing central metalogical notions, such as completeness and decidability. The analysis of unpublished material presented (...) in Chapter 2 shows that a completeness proof for propositional logic was found by Hilbert and his assistant Paul Bernays already in 1917--18, and that Bernays's contribution was much greater than is commonly acknowledged. Aside from logic, the main technical contribution of Hilbert's Program are the development of formal mathematical theories and proof-theoretical investigations thereof, in particular, consistency proofs. In this respect Wilhelm Ackermann's 1924 dissertation is a milestone both in the development of the Program and in proof theory in general. Ackermann gives a consistency proof for a second-order version of primitive recursive arithmetic which, surprisingly, explicitly uses a finitistic version of transfinite induction up to www . He also gave a faulty consistency proof for a system of second-order arithmetic based on Hilbert's &egr;-substitution method. Detailed analyses of both proofs in Chapter 3 shed light on the development of finitism and proof theory in the 1920s as practiced in Hilbert's school. ;In a series of papers, Charles Parsons has attempted to map out a notion of mathematical intuition which he also brings to bear on Hilbert's finitism. According to him, mathematical intuition fails to be able to underwrite the kind of intuitive knowledge Hilbert thought was attainable by the finitist. It is argued in Chapter 4 that the extent of finitistic knowledge which intuition can provide is broader than Parsons supposes. According to another influential analysis of finitism due to W. W. Tait, finitist reasoning coincides with primitive recursive reasoning. The acceptance of non-primitive recursive methods in Ackermann's dissertation presented in Chapter 3, together with additional textual evidence presented in Chapter 4, shows that this identification is untenable as far as Hilbert's conception of finitism is concerned. Tait's conception, however, differs from Hilbert's in important respects, yet it is also open to criticisms leading to the conclusion that finitism encompasses more than just primitive recursive reasoning. (shrink)

W. Tait, The provenance of pure reason. Essays in the philosophy of mathematics and its history. New York: Oxford University Press, 2005. ix + 332 pp. £36.50. ISBN 0-19-514192-X. Reviewed by J. W....

In the early 1920s, the German mathematician David Hilbert (1862–1943) put forward a new proposal for the foundation of classical mathematics which has come to be known as Hilbert's Program. It calls for a formalization of all of mathematics in axiomatic form, together with a proof that this axiomatization of mathematics is consistent. The consistency proof itself was to be carried out using only what Hilbert called “finitary” methods. The special epistemological character of finitary reasoning then yields the required justification (...) of classical mathematics. Although Hilbert proposed his program in this form only in 1921, various facets of it are rooted in foundational work of his going back until around 1900, when he first pointed out the necessity of giving a direct consistency proof of analysis. Work on the program progressed significantly in the 1920s with contributions from logicians such as Paul Bernays, Wilhelm Ackermann, John von Neumann, and Jacques Herbrand. It was also a great influence on Kurt Gödel, whose work on the incompleteness theorems were motivated by Hilbert's Program. Gödel's work is generally taken to show that Hilbert's Program cannot be carried out. It has nevertheless continued to be an influential position in the philosophy of mathematics, and, starting with the work of Gerhard Gentzen in the 1930s, work on so-called Relativized Hilbert Programs have been central to the development of proof theory. (shrink)

There are some puzzles about G¨ odel’s published and unpublished remarks concerning finitism that have led some commentators to believe that his conception of it was unstable, that he oscillated back and forth between different accounts of it. I want to discuss these puzzles and argue that, on the contrary, G¨ odel’s writings represent a smooth evolution, with just one rather small double-reversal, of his view of finitism. He used the term “finit” (in German) or “finitary” or “finitistic” primarily to (...) refer to Hilbert’s conception of finitary mathematics. On two occasions (only, as far as I know), the lecture notes for his lecture at Zilsel’s [G¨ odel, 1938a] and the lecture notes for a lecture at Yale [G¨ odel, *1941], he used it in a way that he knew—in the second case, explicitly—went beyond what Hilbert meant. Early in his career, he believed that finitism (in Hilbert’s sense) is openended, in the sense that no correct formal system can be known to formalize all finitist proofs and, in particular, all possible finitist proofs of consistency of first-order number theory, P A; but starting in the Dialectica paper.. (shrink)

If it could be shown that one of Gentzen's consistency proofs for pure number theory could be shown to be finitistically acceptable, an important part of Hilbert's program would be vindicated. This paper focuses on whether the transfinite induction on ordinal notations needed for Gentzen's second proof can be finitistically justified. In particular, the focus is on Takeuti's purportedly finitistically acceptable proof of the well-ordering of ordinal notations in Cantor normal form. The paper begins with a historically informed discussion of (...) finitism and its limits, before introducing Gentzen and Takeuti's respective proofs. The rest of the paper is dedicated to investigating the finitistic acceptability of Takeuti's proof, including a small but important fix to that proof. That discussion strongly suggests that there is a philosophically interesting finitist standpoint that Takeuti's proof, and therefore Gentzen's proof, conforms to. (shrink)