Proof theory
|
|
Proof theory, studied as a branch of mathematical logic, represents proofs as formal mathematical objects, 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 since the start of the twentieth century, which was, 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 only 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.
| Contents |
History
Although the formalisation of logic was much advanced by the work of such figures as Gottlob Frege, Peano, Russell and Dedekind, conventionally 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.
Formal and informal proof
However, the proofs used in everyday mathematical 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:
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.
Consistency proofs
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 universal 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 simple 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.
Tableau systems
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.
Ordinal analysis
Main article: Ordinal analysis
Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for theories formalising arithmetic and analysis.
Substructural logics
Main article: Substructural logic
See also
Selected bibliography
- 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.pl:Teoria dowodu