The leading exponent of the formalist philosophy of mathematics was David Hilbert (1862–1943), who pioneered in a development of logic known as proof theory or metamathematics. From the time of his first papers on the foundations of mathematics, Hilbert stressed the importance of the axiomatic method and its superiority over the genetic approach, by which concepts are extended piecemeal as the need arises. Once a theory is axiomatized, however, it invites a number of general questions concerning the logical relations holding between its propositions, and Hilbert was soon to consider as central among such questions the problem of establishing consistency, or freedom from contradiction. Hilbert did not himself think that there was any support for the allegations of inconsistency in analysis, as made by Hermann Weyl. Nevertheless, he wished to consolidate once and for all the foundations of mathematics and to give them such clarity...