- Proof theory
**Proof theory**is a branch ofmathematical logic that represents proofs as formalmathematical object s, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defineddata structures such as plain lists, boxed lists, or trees, which are constructed according to theaxiom s and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast tomodel theory , which is semantic in nature. Together withmodel theory ,axiomatic set theory , andrecursion theory , proof theory is one of the so-called "four pillars" of thefoundations of mathematics .cite book

last = Wang

first = Hao

authorlink = Hao Wang (academic)

title = Popular Lectures on Mathematical Logic

publisher = Van Nostrand Reinhold Company

year = 1981

isbn = 0442231091

pages = 3–4] Proof theory can also be considered a branch ofphilosophical logic , where the primary interest is in the idea of aproof-theoretic semantics , an idea which depends upon technical ideas instructural 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 , andRichard Dedekind , the story of modern proof theory is often seen as being established byDavid Hilbert , who initiated what is calledHilbert's program in thefoundations 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 theHilbert 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 ofnatural deduction (simultaneously with and independently of Jaskowski) and thesequent calculus , made fundamental advances in the formalisation of intuitionistic logic, introduced the important idea ofanalytic proof , and provided the first combinatorial proof of the consistency ofPeano 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

interactive theorem proving . Significantly, these proofs can be checked automatically, also by computer. (Checking formal proofs is usually trivial, whereas "finding" proofs (automated theorem proving ) is typically quite hard.) An informal proof in the mathematics literature, by contrast, requires weeks ofpeer review to be checked, and may still contain errors.**Kinds of proof calculi**The three most well-known styles of

proof calculi are:

*The Hilbert calculi

*The natural deduction calculi

*The sequent calculiEach of these can give a complete and axiomatic formalization of propositional or

predicate logic of either the classical or intuitionistic flavour, almost anymodal logic , and manysubstructural logic s, such asrelevance logic orlinear 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 $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.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 $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, particularlyJ. 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 toAlan Turing andSolomon Feferman ;

*The recent discovery ofself-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.**tructural 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 byDag 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 asJean-Yves Girard 'sproof net s also support a notion of analytic proof.Structural proof theory is connected to

type theory by means of theCurry-Howard correspondence , which observes a structural analogy between the process of normalisation in the natural deduction calculus and beta reduction in thetyped lambda calculus . This provides the foundation for theintuitionistic type theory developed byPer 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 andMontague grammar apply formalisms based on structural proof theory to give a formalnatural 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**Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for theories formalising arithmetic and analysis.

**ubstructural logics****ee also***

Proof techniques

*Intermediate logics **References***J. Avigad, E.H. Reck, 2001 . [

*http://www.andrew.cmu.edu/user/avigad/Papers/infinite.pdf “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" [*http://www.springerlink.com/content/n602313107541846/?p=74ab8879ce75445da488d5744cbc3818&pi=0*]

*Wikimedia Foundation.
2010.*

### Look at other dictionaries:

**Proof theory**— proof theory … Philosophy dictionary**proof theory**— The study of the relations of deducibility among sentences in a logical calculus . Deducibility is defined purely syntactically, that is, without reference to the intended interpretation of the calculus. See also model theory … Philosophy dictionary**Structural proof theory**— In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof. Contents 1 Analytic proof 2 Structures and connectives 3 Cut elimination in the sequent… … Wikipedia**Proof**— may refer to: * A rigorous, compelling argument ** Formal proof ** Mathematical proof ** Proof theory, a branch of mathematical logic that represents proofs as formal mathematical objects ** Logical argument ** Evidence (law), tested evidence or… … Wikipedia**Theory (mathematical logic)**— This article is about theories in a formal language, as studied in mathematical logic. For other uses, see Theory (disambiguation). In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. Usually… … Wikipedia**Proof calculus**— In mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules. The specific inference rules of a member of such a family characterize the theory of a… … Wikipedia**Theory**— The word theory has many distinct meanings in different fields of knowledge, depending on their methodologies and the context of discussion.In science a theory is a testable model of the manner of interaction of a set of natural phenomena,… … Wikipedia**Proof mining**— In proof theory (a branch of mathematical logic), proof mining is a research program [cite book title = Applied Proof Theory: Proof Interpretations and Their Use in Mathematics author = Ulrich Kohlenbach publisher = Springer Verlag, Berlin year … Wikipedia**Proof complexity**— In computer science, proof complexity is a measure of efficiency of automated theorem proving methods that is based on the size of the proofs they produce. The methods for proving contradiction in propositional logic are the most analyzed. The… … Wikipedia**Proof procedure**— In logic, and in particular proof theory, a proof procedure for a given logic is a systematic method for producing proofs in some proof calculus of (provable) statements.There are several types of proof calculi. The most popular are natural… … Wikipedia