Abstract

The background to the development of proof theory since 1960 is contained in the article (MATHEMATICS, FOUNDATIONS OF), Vol. 5, pp. 208- 209. Brie y, Hilbert's program (H.P.), inaugurated in the 1920s, aimed to secure the foundations of mathematics by giving nitary consistency proofs of formal systems such as for number theory, analysis and set theory, in which informal mathematics can be represented directly. These systems are based on classical logic and implicitly or explicitly depend on the assumption of \completed in nite" totalities. Consistency of a system S (containing a modicum of elementary number theory) is su cient to ensure that any nitary meaningful statement about the natural numbers which is provable in S is correct under the intended interpretation. Thus, in Hilbert's view, consistency of S would serve to eliminate the \completed in nite" in favor of the \potential in nite" and thus secure the body of mathematics represented in S. Hilbert established the subject of proof theory as a technical part of mathematical logic by means of which his program was to be carried out its methods will be described below. In 1931, Godel's second incompleteness theorem raised a prima facieobstacle to H.P. for the system Z of elementary number theory (also called Peano Arithmetic, and denoted below by PA) since all previously recognized forms of nitary reasoning could be formalized within it. In any case, Hilbert's program could not possibly succeed for any system such as set theory in which all nitary notions and reasoning could unquestionably be formalized. These obstacles led workers in proof theory to modify H.P. in two kinds of ways. The rst was to seek reductions of various formal systems S to more constructive systems S 0. The second was to shift the aims from foundational ones to more mathematical ones. Examples of 1 the former move are the reductions of PA to intuitionistic arithmetic HA, and Gentzen's consistency proof of PA by nitary reasoning coupled with quanti er-free trans nite induction up to the ordinal , TI( 0), both obtained in the 1930s (cf..