Research Areas
Proof Theory
The axiomatic method was developed by David Hilbert around the turn of the twentieth century, as a tool to be used in the partly philosophical and partly mathematical study of mathematics itself. Hilbert had been influenced by a number of developments in mathematics in the late nineteenth century, including the use of models of non-Euclidean geometries for independence and relative consistency arguments in geometry; the use of abstract algebraic and analytic methods in number theory; and the use of emerging set-theoretic notions in analysis. In each of these fields, as well as in other sufficiently developed fields like physics, Hilbert viewed the axiomatic method as means for providing a systematic organization of the subject, as well as for investigating issues like consistency, independence, and completeness.
The second problem posed by Hilbert in 1900 to the International Congress of Mathematicians in Paris raised the issue of establishing the consistency of such axiomatic theories. It wasn't until almost two decades later, however, that this problem could be formulated in a clear and methodologically sound way. Doing so involved extensive foundational work by Hilbert and his collaborators (among them Paul Bernays and Wilhelm Ackermann), who, strongly influenced by Russell and Whitehead's Principia Mathematica, helped to lay the groundwork for modern mathematical logic. Around 1922, Hilbert introduced the subject of proof theory as a means of addressing the consistency problem: viewing proofs in formalized axiomatic theories as objects of investigation, the new theory was 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 finitist means. But the broader use of the axiomatic method to model various aspects of mathematical practice still provides a valuable tool in addressing issues in the foundations, philosophy, and methodology of mathematics. And Proof Theory has grown in many ways since Hilbert's time, to the point where the subject can now be viewed as a general study of deductive systems and their properties. Complementing the traditional, metamathematical branch, there are now branches known as structural proof theory, where one studies structural properties of derivations, especially with respect to transformations and canonical forms; and proof complexity, where one studies the efficiency of proof systems with respect to various measures of proof length.
Wilfried Sieg and Jeremy Avigad have worked extensively in Proof Theory. With co-authors Wilfried Buchholz, Solomon Feferman, and Wolfram Pohlers, Sieg has written an influential proof-theoretic study of subsystems of analysis and theories of inductive definitions. He also investigated systematically ways of extracting computational information from proofs in fragments of arithmetic. He is currently involved in automated proof search, developing and implementing proof-theoretic techniques and subject-specific heuristics for finding natural proofs in logic and parts of mathematics. The automated theorem prover AProS, the result of these efforts, has proved at an abstract level Goedel's incompleteness theorems.
Avigad uses proof theory to explore the role of abstract, infinitary, and nonconstructive methods in mathematics, and is interested in ways of understanding such methods in concrete, combinatorial, or algorithmic terms. Towards that end, he has used a variety of approaches (including cut-elimination, realizability, functional interpretations, and forcing) to study a range of axiomatic theories, from theories of admissible sets to weak fragments of arithmetic. He is also interested in formal verification of mathematics using mechanized proof assistants, and ways in which a proof-theoretic understanding of mathematics can help support verification efforts.
Both Sieg and Avigad are especially interested in the 19th century mathematical developments that gave rise to Hilbert's program. Sieg has worked on the evolution of proof theory and Hilbert's foundational views; relatedly, he is involved in two editorial projects. The Hilbert Project is devoted to editing unpublished notes for lectures of Hilbert (from roughly 1895 through the 1920s); the Bernays Project aims for the translation of Bernays' essays in the philosophy of mathematics. Avigad has studied nineteenth century developments in number theory, and has used such historical case studies to obtain a better philosophical understanding of modern mathematical methods.
There are, of course, other strands of research at Carnegie Mellon related to proof theory. In Computer Science, Frank Pfenning investigates logical frameworks for proof search, Steve Rudich studies issues in computational complexity and proof complexity; in mathematics, Peter Andrews has been pursuing theorem proving in higher order logic, and Rick Statman has done work on proof complexity and the lambda calculus.
Avigad has used a mechanized proof assistant called Isabelle to formally verify the prime number theorem. This is one of the most complex mathematical theorems to be verified to date. He is currently developing proof-theoretic methods that can be used to support such verification efforts. For more information, see Avigad’s home page and the formalization project page.