Dissertation, University of California, Berkeley, Spring 2001
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 socalled 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 191718, 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 prooftheoretical 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 secondorder version of primitive recursive arithmetic which, surprisingly, explicitly uses a finitistic version of transfinite induction up to ?^{??}. He also gave a faulty consistency proof for a system of secondorder arithmetic based on Hilbert's epsilonsubstitution 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 nonprimitive 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.
Chapter 2 appeared as Completeness before Post; the version here corrects some misprints and contains a few minor additions. A revised version of Chapter 3 is The practice of finitism.
See also: The Development of Mathematical Logic from Russell to Tarski · Hilbert's "Verunglückter Beweis" · Completeness before Post · The practice of finitism · Hilbert's Program · The Epsilon calculus
1 Introduction  1 

1 

4 

7 

11 
2 Completeness before Post: Bernays, Hilbert, and the Development of Propositional Logic  15 

15 

17 

17 

21 

23 

25 

27 

29 

31 

35 

36 

41 
3 The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program  56 

56 

58 

61 

66 

68 

73 

75 

77 

83 

85 

91 

94 
4 Finitism and Mathematical Knowledge  109 

109 

111 

114 

114 

121 

125 

128 

132 

134 

141 

147 
Bibliography  155 