Carnegie Mellon University
Proof Theory

Proof Theory

One of the pioneers in mathematical logic was David Hilbert, who developed the axiomatic method around the turn of the twentieth century as a tool for partly philosophical and partly mathematical study of mathematics itself. Hilbert viewed the axiomatic method as a means for providing a systematic organization of the subject, as well as for investigating issues like consistency, independence, and completeness.

The second of Hilbert's famous problems raised the consistency problem for axiomatic theories, in particular for arithmetic. In 1922, Hilbert introduced the new subject of proof theory for addressing the problem: viewing proofs in formalized theories as objects of investigation, the goal being to establish - using only restricted finitist means - that such proofs cannot lead to a contradiction. Gödel's 1931 incompleteness theorems show that one cannot achieve Hilbert's specific goal of demonstrating the consistency of set-theoretic mathematics using only finitist means, but the use of his axiomatic method still provides a valuable tool for addressing issues in the foundations, philosophy, and methodology of mathematics. Proof theory has turned into a fascinating area of research at the intersection of philosophy, mathematics and, increasingly, computer science. Both Sieg and Avigad have worked extensively in proof theory.

Sieg's papers in proof theory fall into three groups. In the first, some in collaboration with Feferman, strong impredicative systems of classical analysis were reduced to a variety of constructive ones. The foundationally most significant systems to which reductions were achieved concern higher constructive number classes. (These papers were published in the influential volume "Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies" Sieg edited jointly with W. Buchholz, S. Feferman, and W. Pohlers.) In the second group of papers, fragments of arithmetic were investigated and methods for the direct treatment of classical systems were developed ("Herbrand analysis"); these methods were also used to determine the class of provably recursive functions of weak subsystems of analysis containing a form of König's Lemma. Finally, the third group of papers deals with a quite different part of the subject, proof systems of natural deduction. Here Sieg developed methods for establishing normal form theorems semantically and thus provide the theoretical underpinnings for an automated search for proofs; see below.

Avigad has explored and extended a number of proof-theoretic methods of reducing classical theories to constructive ones, in the sense of Hilbert's program; and of locating that computational content that is implicit in classical reasoning. Such methods include cut-elimination, double-negation translations, realizability, functional interpretation, forcing, and model-theoretic methods. He is interested not only in obtaining a better philosophical and foundational understanding of contemporary mathematics, but also in applying these insights in purely mathematical domains. For example, in the field of "proof mining," one tries to extract computational or otherwise explicit information from nonconstructive arguments in ordinary mathematics. Avigad is particularly interested in uses of infinitary analytic methods in number theory and combinatorics.