The background to the development of "proof theory" since 1960 is contained in the entry "Mathematics, Foundations of." Briefly, Hilbert's program (HP), inaugurated in the 1920s, aimed to secure the foundations of mathematics by giving finitary 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 infinite" totalities. Consistency of a system S (containing a modicum of elementary number theory) is sufficient to ensure that any finitarily meaningful statement about the natural numbers that is provable in S is correct under the intended interpretation. Thus, in David Hilbert's view, consistency of S would serve to eliminate the "completed infinite" in favor of the "potential infinite" and thus secure the body of mathematics represented in S. Hilbert established the...