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)

After a brief flirtation with logicism around 1917, David Hilbertproposed his own program in the foundations of mathematics in 1920 and developed it, in concert with collaborators such as Paul Bernays andWilhelm Ackermann, throughout the 1920s. The two technical pillars of the project were the development of axiomatic systems for everstronger and more comprehensive areas of mathematics, and finitisticproofs of consistency of these systems. Early advances in these areaswere made by Hilbert (and Bernays) in a series of lecture courses atthe (...) University of Göttingen between 1917 and 1923, and notably in Ackermann's dissertation of 1924. The main innovation was theinvention of the -calculus, on which Hilbert's axiom systemswere based, and the development of the -substitution methodas a basis for consistency proofs. The paper traces the developmentof the ``simultaneous development of logic and mathematics'' throughthe -notation and provides an analysis of Ackermann'sconsistency proofs for primitive recursive arithmetic and for thefirst comprehensive mathematical system, the latter using thesubstitution method. It is striking that these proofs use transfiniteinduction not dissimilar to that used in Gentzen's later consistencyproof as well as non-primitive recursive definitions, and that thesemethods were accepted as finitistic at the time. (shrink)

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)

The Bernays-Müller debate was a dispute in the early 1920s between Paul Bernays and Aloys Müller regarding various philosophical issues related to “Hilbert’s program.” The debate is sometimes mentioned as a sidenote in discussions of Hilbert’s program, but there is little or no discussion of the debate itself in the secondary literature. This article aims to fill this gap and to provide a detailed analysis of the background of the debate, its contents, and the impact on its protagonists.

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)