Proof theory is a branch of mathematical logic that 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 syntactic in nature, in contrast to model theory, which is
semantic in nature. 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.[1] 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.
History
Although the formalisation of logic was much advanced by the work of such figures as Gottlob
Frege, Giuseppe Peano, Bertrand Russell,
and Richard Dedekind, the story of modern proof theory is often 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 initially seemed to bode well for
Hilbert's aim of reducing all mathematics to a finitist formal system; then his incompleteness theorems showed that this is unattainable. All of this work was carried
out with the proof calculi 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 (simultaneously with and independently of Jaskowski) and the
sequent calculus, made fundamental advances in the formalisation of intuitionistic
logic, introduced the important idea of analytic proof, and provided the first
combinatorial proof of the consistency of Peano arithmetic.
Formal and informal proof
The informal proofs of everyday mathematical practice are unlike the formal proofs of proof theory. They are
rather like high-level sketches that would allow an expert to reconstruct a formal proof at least in principle, given enough time
and patience. For most mathematicians, writing a fully formal proof would have all the drawbacks of programming in
machine code.
Formal proofs are constructed with the help of computers in automated theorem
proving. Significantly, these proofs can be checked automatically, also by computer. (Checking formal proofs is usually
trivial, whereas finding proofs is typically quite hard.) An informal proof in the mathematics literature, by contrast, requires
weeks of peer review to be checked, and may still contain errors.
Kinds of proof calculi
The three most well-known styles of proof calculi are:
Each of these can give a complete and axiomatic formalization of propositional
or predicate logic of either the classical or
intuitionistic flavour, almost any modal
logic, and 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.
Consistency proofs
-
As previously mentioned, 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
UNIQ7e2081744689cb01-math-6558f93830a3cf9b00000002 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.
The failure of the program was induced by Kurt Gödel's incompleteness theorems, which showed that any ω-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 
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 ω-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
-
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
-
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
-
See also
References
- ^ Wang, Hao (1981). Popular Lectures on Mathematical Logic.
Van Nostrand Reinhold Company, 3–4. ISBN 0442231091.
- J. Avigad, E.H. Reck, 2001 .“Clarifying the nature of the infinite”: the development of metamathematics and proof theory. Carnegie-Mellon
Technical Report CMU-PHIL-120.
- A. S. Troelstra, H. Schwichtenberg. Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science). Cambridge
University Press. ISBN 0-521-77911-1
- G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, Collected Papers of Gerhard Gentzen.
North-Holland, 1969.
- L.Moreno-Armella & B.Sriraman (2005).Structural Stability and Dynamic Geometry: Some Ideas on Situated Proof.
International Reviews on Mathematical Education. Vol. 37, no.3, pp.130-139
[1]
This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)
