Hightlights in Proof Theory

Abstract

This is a survey of some of the principal developments in proof theory from its inception in the 1920s, at the hands of David Hilbert, up to the 1960s. Hilbert’s aim was to use this as a tool in his finitary consistency program to eliminate the “actual infinite” in mathematics from proofs of purely finitary statements. One of the main approaches that turned out to be the most useful in pursuit of this program was that due to Gerhard Gentzen, in the 1930s, via his calculi of “sequents” and his Cut-Elimination Theorem for them. Following that we trace how and why prima facie infinitary concepts, such as ordinals, and infinitary methods, such as the use of infinitely long proofs, gradually came to dominate proof-theoretical developments.

This is the first of three lectures that I delivered at the conference, Proof Theory: History and Philosophical Significance, held at the University of Roskilde, Denmark, Oct. 31—Nov. 1, 1997. I wish to thank the organizers, Prof. Stig Andur Pedersen and Prof. Vincent F. Hendricks for inviting me to present these lectures, and especially for their substantial work in preparing them for publication with the assistance of Mr. Klaus Frovin Jørgensen, from their audio tapes and my transparencies. I have edited the resulting articles for coherence and readability, but otherwise have maintained their character as lectures, as originally given.