Abstract

Proof theory arose as a mathematical solution to a problem in the philosophy of mathematics. In the first third of the twentieth century, debates raged among philosophers and mathematicians about the safety of mathematical reasoning. David Hilbert proposed to safeguard classical mathematics by formalizing it using the then-new tools of symbolic logic, and using philosophically uncontentious methods to prove that these formal systems are free from contradiction, i.e., consistent. To carry out this project, Gerhard Gentzen developed a number of formal systems in the 1930s, and proved the consistency of elementary number theory. The chapter surveys the historical background of the development of proof theory arising out of the foundational debate and Hilbert’s program, discusses the significance of Gentzen’s work, and outlines some developments in proof theory after Gentzen.