Proof theory, studied as a branch of mathematical logic, represents proofs as formal mathematical objects, so facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures, such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is closer to syntax, while model theory is more purely semantical. Together with model theory, axiomatic set theory, and recursion theory, proof theory is one of the so-called four pillars of the foundations of mathematics.
That represents the position as of about 1940 onwards. The subject of proof theory has a significant if somewhat opaque prehistory as metamathematics, the proposed theory under development from the start of the twentieth century, for a generation, under the influence of David Hilbert. The aim, of a convincing consistency proof for mathematics, was not to be realised, for reasons later understood: proof theory can only sweep the metaphysical dust into tidier heaps under carpets with more attractive patterns. Hilbert's ideas seem to have been based on an analogy, in fact false, with the elimination theory of algebraic geometry familiar to him from his early work in algebra. The real insights of proof theory, such as cut-elimination and the isolation of the structural rules, were not to come from this direction.
Proof theory can also be considered a branch of philosophical logic, where the primary interest is in the idea of a proof-theoretic semantics, an idea which depends upon technical ideas in structural proof theory to be feasible.
Although the formalisation of logic was much advanced by the work of such figures as Gottlob Frege, Peano, Russell and Dedekind, conventially the story of modern proof theory is seen as being established by David Hilbert, who initiated what is called Hilbert's program in the Foundations of mathematics. Kurt Gödel's seminal work on proof theory first advanced, then refuted this program: his completeness theorem seemed to bring Hilbert's dream of reducing all mathematics to a small, finitarily meaningful core within reach, then his incompleteness theorems showed that the dream was unattainable. All of this work was carried out with the proof calculus called the Hilbert systems .
In parallel with the proof theoretic work of Gödel, Gerhard Gentzen was laying the foundations of what is now known as structural proof theory. In a few short years, Gentzen introduced the core formalisms of natural deduction and the sequent calculus, made fundamental advances in the formalisation of intuitionistic logic, introduced the seminal idea of analytic proof, and provided the first combinatorial proof of the consistency of Peano Arithmetic.
Formal and informal proof
However, the proofs used in everyday mathematic practice are almost never like the formal proofs in proof theory. They are rather like high-level sketches that would allow an expert to reconstruct a formal proof at least in principle, and given enough time and patience. For most mathematicians, writing a fully formal proof would have all the drawbacks of programming in machine code.
Formal proof are constructed, with the help of computers, in automated theorem proving. Significantly, these proofs can be checked automatically by computer. (Checking formal proofs is usually trivial, whereas finding proofs is typically not computable for an expressive logic.) An informal proof in the mathematics literature, by contrast, requires weeks of peer review to be checked, and may still contain bugs.
Kinds of proof calculus
The three most well known proof calculi are:
- The Hilbert-style calculi
- The natural deduction calculus
- The sequent calculus
To say these are proof calculi, rather than proof systems, is to say they are flexible frameworks for the study of many kinds of logical consequence relations. Each of these can formalise propositional or predicate logics of either the classical or intuitionistic flavour, or almost any modal logic studied, many substructural logics, such as relevance logic or linear logic. Indeed it is unusual to find a logic that resists being represented in one of these calculi; Jaakko Hintikka 's independence-friendly logic being perhaps the most well-known of these awkward customers.
Main article: Consistency proof
As we have discussed, the spur for the mathematical investigation of proofs in formal theories was Hilbert's program. The central idea of this program was that if we could give finitary proofs of consistency for all the sophisticated formal theories needed by mathematicians, then we could ground these theories by means of a metamathematical argument, which shows that all of their purely univeral assertions (more technically their provable Pi-0-1 sentences) are finitarily true; once so grounded we do not care about the non-finitary meaning of their existential theorems, regarding these as pseudo-meaningful stipulations of the existence of ideal entities.
And again, we have discussed the failure of the program due to Kurt Gödel's incompleteness theorems, which showed that any omega-consistent theory that is sufficiently strong to express certain simple arithmetic truths, cannot prove its own consistency, which on Gödel's formulation is a Pi-0-1 sentence.
Much investigation has been carried out on this topic since, which has in particular led to:
- Refinement of Gödel's result, particularly J. Barkley Rosser's refinement, weakening the above requirement of omega-consistency to 1-consistency;
- Axiomatisation of the core of Gödel's result in terms of a modal language, provability logic;
- Transfinite iteration of theories, due to Alan Turing and Solomon Feferman;
- The recent discovery of self-verifying theories, systems strong enough to talk about themselves, but too weak to carry out the diagonal argument that is the key to Gödel's unprovability argument.
Structural proof theory
Main article: Structural proof theory
Structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof. The notion of analytic proof was introduced by Gentzen for the sequent calculus; there the analytic proofs are those that are cut-free. His natural deduction calculus also supports a notion of analytic proof, as shown by Dag Prawitz; the definition is slightly more complex, we say the analytic proofs are the normal forms, which are related to the notion of normal form in term rewriting. More exotic proof calculi such as Jean-Yves Girard's proof nets also support a notion of analytic proof.
Structural proof theory is connected to type theory by means of the Curry-Howard correspondence, which observes a structural analogy between the process of normalisation in the natural deduction calculus and beta reduction in the typed lambda calculus. This provides the foundation for the intuitionistic type theory developed by Per Martin-Löf , and is often extended to a three way correspondence, the third leg of which are the cartesian closed categories.
In linguistics, type-logical grammar , categorial grammar and Montague grammar apply formalisms based on structural proof theory to give a formal natural language semantics .
Main article: Tableau systems
Tableau systems apply the central idea of analytic proof from structural proof theory to provide decision procedures and semi-decision procedures for a wide range of logics.
Main article: Ordinal analysis
Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for theories formalising arithmetic and analysis.
Main article: Substructural logic
- A. S. Troelstra, H. Schwichtenberg. Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0521779111
- G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, Collected Papers of Gerhard Gentzen. North-Holland, 1969.