PROOF THEORY

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 subject of proof theory as a technical part of mathematical logic by means of which his program was to be carried out; its methods are described below.

In 1931 Kurt Gödel's second incompleteness theorem raised a prima facie obstacle to HP for the system Z of elementary number theory (also called Peano arithmetic—PA) since all previously recognized forms of finitary 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 finitary notions and reasoning could unquestionably be formalized. These obstacles led workers in proof theory to modify HP in two ways. The first was to seek reductions of various formal systems S to more constructive systems S′. The second was to shift the aims from foundational ones to more mathematical ones. Examples of the first modification are the reductions of PA to intuitionistic arithmetic HA and Gentzen's consistency proof of PA by finitary reasoning coupled with quantifier-free transfinite induction up to the ordinal ε₀, TI(ε₀), both obtained in the 1930s. The second modification of proof theory was promoted especially by Georg Kreisel starting in the early 1950s; he showed how constructive mathematical information could be extracted from nonconstructive proofs in number theory. The pursuit of proof theory along the first of these lines has come to be called relativized Hilbert program or reductive proof theory, while that along the second line is sometimes called the program of unwinding proofs or, perhaps better, extractive proof theory. In recent years there have been a number of applications of the latter both in mathematics and in theoretical computer science. Keeping the philosophical relevance and limitations of space in mind, the following account is devoted entirely to developments in reductive proof theory, though the two sides of the subject often go hand in hand.

Methods of Finitary Proof Theory

Hilbert introduced a special formalism called the epsilon calculus to carry out his program (the nomenclature is related neither to the ordinal ε₀ nor to the membership symbol in set theory), and he proposed a particular substitution method for that calculus. Following Hilbert's suggestions, Wilhelm Ackermann and John von Neumann obtained the first significant results in finitary proof theory in the 1920s. Then, in 1930, another result of the same character for more usual logical formalisms was obtained by Jacques Herbrand, but there were troublesome aspects of his work. In 1934 Gerhard Gentzen introduced new systems, the so-called sequent calculi, to provide a very clear and technically manageable vehicle for proof theory, and reobtained Herbrand's fundamental theorem via his cut-elimination theorem. Roughly speaking, the latter tells us that every proof of a statement in quantificational logic can be normalized to a direct proof in which there are no detours ("cuts") at any stage via formulas of a complexity higher than what appears at later stages. Sequents have the form Γ→Δ, where Γ and Δ are finite sequences of formulas (possibly empty). Γ→Δ is derivable in Gentzen's calculus LK just in case the formula A ⊃ B is derivable in one of the usual calculi for classical predicate logic, where A is the conjunction of formulas in Γ and B is the disjunction of those in Δ.

Introduction of Infinitary Methods to Proof Theory

Gentzen's theorem as it stood could not be used to establish the consistency of PA, where the scheme of induction resists a purely logical treatment, and for this reason he was forced to employ a partial cut-elimination argument whose termination was guaranteed by the principle TI(ε₀). Beginning in the 1950s, Paul Lorenzen and then, much more extensively, Kurt Schütte began to employ certain infinitary extensions of Gentzen's calculi (cf. Schütte, 1960, 1977). This was done first of all for elementary number theory by replacing the usual rule of universal generalization by the so-called ω-rule, in the form: from Γ→Δ,A(n ) for each n = 0,1,2, …, infer Γ→Δ,(x)A(x). Now derivations are well-founded trees (whose tips are the axioms A→A), and each such is assigned an ordinal as length in a natural way. For this calculus LK_ω, one has a full cut-elimination theorem, and every derivation of a statement in PA can be transformed into a cut-free derivation of the same in LK_ω whose length is less than ε₀. Though infinite, the derivation trees involved are recursive and can be described finitarily, to yield another consistency proof of PA by TI(ε₀). Schütte extended these methods to systems RA_α of ramified analysis (α an ordinal) in which existence of sets is posited at finite and transfinite levels up to α, referring at each stage only to sets introduced at lower levels. Using a suitable extension of LK_ω to RA_α, Schütte obtained cut-elimination theorems giving natural ordinal bounds for cut-free derivations in terms of the so-called Veblen hierarchy of ordinal functions. In 1963 he and Solomon Feferman independently used this to characterize (in that hierarchy) the ordinal of predicative analysis, defined as the first α for which TI(α) cannot be justified in a system RA_β for β<α. William Tait (1968) obtained a uniform treatment of arithmetic, ramified analysis, and related unramified systems by means of the cut-elimination theorem for LK extended to a language with formulas built by countably infinite conjunctions (with the other connectives as usual). Here the appropriate new rule of inference is: from Γ→Δ,A_n, for each n = 0,1,2, …, infer Γ→Δ,A, where A is the conjunction of all the A_n's.

Brief mention should also be made of the extensions of the other methods of proof theory mentioned above, concentrating on elimination of quantifiers rather than cut elimination. In the 1960s Burton Dreben and his students corrected and extended the Herbrand approach (cf. Dreben and Denton, 1970). Tait (1965) made useful conceptual reformulations of Hilbert's substitution method; a number of applications of this method to subsystems of analysis have been obtained in the 1990s by Grigori Mints (1994). Another approach stems from Gödel's functional interpretation, first presented in a lecture in 1941 but not published until 1958 in the journal Dialectica ; besides the advances with this made by Clifford Spector in 1962, more recently there have been a number of further applications both to subsystems of arithmetic and to subsystems of analysis (cf. Feferman 1993). Finally, mention should be made of the work of Dag Prawitz (1965) on systems of natural deduction, which had also been introduced by Gentzen in 1934 but not further pursued by him; for these a process of normalization takes the place of cut elimination. While each of these other methods has its distinctive merits and advantages, it is the methods of sequent calculi in various finitary and infinitary forms that have received the most widespread use.

Proof Theory of Impredicative Systems

The proof theory of impredicative systems of analysis was initiated by Gaisi Takeuti in the 1960s. He used partial cut-elimination results and established termination by reference to certain well-founded systems of ordinal diagrams (cf. Takeuti 1987). In 1972 William Howard determined the ordinal of a system ID₁ of one arithmetical inductive definition, in the so-called Bachmann hierarchy of ordinal functions; the novel aspect of this was that it makes use of a name for the first uncountable ordinal in order to produce the countable (and in fact recursive) ordinal of ID₁. In a series of contributions by Harvey Friedman, Tait, Feferman, Wolfram Pohlers, Wilfried Buchholz, and Wilfried Sieg stretching from 1967 into the 1980s, the proof theory of systems of iterated inductive definitions ID_α and related impredicative subsystems of analysis was advanced substantially. The proof-theoretic ordinals of the ID_α were established by Pohlers in terms of higher Bachmann ordinal function systems (cf. Buchholz et al. 1981). The methods here use cut-elimination arguments for extensions of LK involving formulas built by countably and uncountably long conjunctions. In addition, novel "collapsing" arguments are employed to show how to collapse suitable uncountably long derivations to countable ones in order to obtain the countable (again recursive) ordinal bounds for these systems. An alternative functorial approach to the treatment of iterated inductive definitions was pioneered by Jean-Yves Girard (1985).

In 1982 Gerhard Jäger initiated the use of the so-called admissible fragments of Zermelo-Fraenkel set theory as an illuminating tool in the proof theory of predicatively reducible systems (cf. Jäger 1986). This was extended by Jäger and Pohlers (1982) to yield the proof-theoretical ordinal of a strong impredicative system of analysis; that makes prima facie use of the name of the first (recursively) inaccessible ordinal. Michael Rathjen (1994) has gone beyond this to measure the ordinals of much stronger systems of analysis and set theory in terms of systems of recursive ordinal notations involving the names of very large (recursively) inaccessible ordinals, analogous to the so-called large cardinals in set theory.

Significance of the Work for hp and Reductive Proof Theory

Ironically for the starting point with Hilbert's aims to eliminate the "completed infinite" from the foundations of mathematics, these developments have required the use of highly infinitary concepts and objects to explain the proof-theoretical transformations involved in an understandable way. It is true that in the end these can be explained away in terms of transfinite induction applied to suitable recursive ordinal notation systems. Even so, one finds few who believe that one's confidence in the consistency of the systems of analysis and set theory that have been dealt with so far has been increased as a result of this body of work. However, while the intrinsic significance of the determination of the proof-theoretic ordinals of such systems has not been established, that work can still serve behind the scenes as a tool in reductive proof theory. It is argued in Feferman (1988) that one has obtained thereby foundationally significant reductions, for example of various (prima facie) infinitary systems to finitary ones, impredicative to predicative ones, and nonconstructive to constructive ones. With a field that is still evolving at the time of writing, it is premature to try to arrive at more lasting judgments of its permanent value.

See also Gödel, Kurt; Gödel's Incompleteness Theorems; Hilbert, David; Logic, History of; Mathematics, Foundations of; Neumann, John von; Set Theory.

Bibliography

Buchholz, W., S. Feferman, W. Pohlers, and W. Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Lecture Notes in Mathematics 897. New York: Springer-Verlag, 1981.

Buchholz, W., and K. Schütte. Proof Theory of Impredicative Systems. Naples, 1988.

Dreben, B., and J. Denton. "Herbrand-Style Consistency Proofs." In Intuitionism and Proof Theory, edited by J. Myhill, A. Kino, and R. E. Vesley, 419–433. Amsterdam: North-Holland, 1970.

Feferman, S. "Gödel's Dialectica Interpretation and Its Two-Way Stretch." In Computational Logic and Proof Theory, edited by G. Gottlob et al. Lecture Notes in Computer Science 713. New York: Springer-Verlag, 1993.

Feferman, S. "Hilbert's Program Relativized: Proof-Theoretical and Foundational Reductions." Journal of Symbolic Logic 53 (1988): 364–384.

Gentzen, G. The Collected Papers of Gerhard Gentzen, edited by M. Szabo. Amsterdam: North-Holland, 1969.

Girard, J.-Y. "Introduction to ∏¹₂ Logic." Synthese 62 (1985).

Girard, J.-Y. Proof Theory and Logical Complexity. Naples: Bibliopolis, 1987.

Hilbert, D., and P. Bernays. Grundlagen der Mathematik. Vols. 1–2, 2nd ed. Berlin: Springer, 1968–1970.

Howard. W. "A System of Abstract Constructive Ordinals." Journal of Symbolic Logic 37 (1972): 355–374.

Jäger, G. Theories for Admissible Sets: A Unifying Approach to Proof Theory. Naples: Bibliopolis, 1986.

Jäger, G., and W. Pohlers. "Eine beweistheoretische Untersuchung von (Δ¹₂-CA)+(BI) und verwandter Systeme." Sitzungsber. Bayerische Akad. Wissenschaft Math. Nat. Klasse (1982): 1–28.

Kreisel, G. "A Survey of Proof Theory." Journal of Symbolic Logic 33 (1965): 321–388.

Mints, G. E. "Gentzen-Type Systems and Hilbert's Epsilon Substitution Method. I." In Logic, Methodology, and Philosophy of Science IX, edited by D. Prawitz et al. Amsterdam and New York: Elsevier, 1994.

Mints, G. E. Selected Papers in Proof Theory. Naples: Bibliopolis, 1992.

Myhill, J., A. Kino, and R. E. Vesley, eds. Intuitionism and Proof Theory. Amsterdam: North-Holland, 1970.

Pohlers, W. "Contributions of the Schütte School in Munich to Proof Theory." In Proof Theory, edited by G. Takeuti. Amsterdam: North-Holland, 1987.

Pohlers, W. Proof Theory: An Introduction. Lecture Notes in Mathematics 1407. New York: Springer-Verlag, 1989.

Prawitz, D. Natural Deduction. Stockholm: Almqvist and Wiksell, 1965.

Rathjen, M. "Admissible Proof Theory and Beyond." In Logic, Methodology, and Philosophy of Science IX, edited by D. Prawitz et al. Amsterdam and New York: Elsevier, 1994.

Schütte, K. Beweistheorie. Berlin: Springer, 1960.

Schütte, K. Proof Theory. Berlin: Springer-Verlag, 1977.

Sieg, W. "Hilbert's Program Sixty Years Later." Journal of Symbolic Logic 53 (1988): 338–348.

Simpson, S. G. "Partial Realizations of Hilbert's Program." Journal of Symbolic Logic 53 (1988): 349–363.

Tait, W. "Normal Derivability in Classical Logic." In The Syntax and Semantics of Infinitary Languages, edited by J. Barwise. Lecture Notes in Mathematics 72. New York: Springer-Verlag, 1968.

Tait, W. "The Substitution Method." Journal of Symbolic Logic 30 (1965): 175–192.

Takeuti, G. Proof Theory. 2nd ed. Amsterdam: North-Holland, 1987.

Solomon Feferman (1996)