View source for Proof theory

{{short description|Branch of mathematical logic}}
{{more footnotes|date=October 2025}}
'''Proof theory''' is a major branch<ref name=wang>According to {{harvtxt|Wang|1981|pp=3–4}}, proof theory is one of four domains mathematical logic, together with [[model theory]], [[axiomatic set theory]], and [[recursion theory]]. {{harvtxt|Barwise|1977}} consists of four corresponding parts, with part D being about "Proof Theory and Constructive Mathematics".</ref> of [[mathematical logic]] and [[theoretical computer science]] within which [[Mathematical proof|proof]]s are treated as formal [[mathematical object]]s, facilitating their analysis by mathematical techniques. Proofs are typically presented as [[Recursive data type|inductively defined]] [[data structures]] such as [[list (computer science)|lists]], boxed lists, or [[Tree (data structure)|tree]]s, which are constructed according to the [[axiom]]s and [[rule of inference|rules of inference]] of a given logical system. Consequently, proof theory is [[syntax (logic)|syntactic]] in nature, in contrast to [[model theory]], which is [[Formal semantics (logic)|semantic]] in nature.

Some of the major areas of proof theory include [[structural proof theory]], [[ordinal analysis]], [[provability logic]], [[proof-theoretic semantics]], [[reverse mathematics]], [[proof mining]], [[automated theorem proving]], and [[proof complexity]]. Much research also focuses on applications in computer science, linguistics, and philosophy.

==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 [[Grundlagen der Mathematik|''Foundations of Mathematics'']]. 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 [[arithmetical hierarchy|<math>\Pi^0_1</math> 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 [[Gödel's incompleteness theorems|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 <math>\Pi^0_1</math>  sentence. However, modified versions of Hilbert's program emerged and research has been carried out on related topics. This has led, in particular, 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 discovery of [[self-verifying theories]], systems strong enough to talk about themselves, but too weak to carry out the [[diagonal lemma|diagonal argument]] that is the key to Gödel's unprovability argument.

In parallel to the rise and fall of Hilbert's program, the foundations of [[structural proof theory]] were being founded. [[Jan Łukasiewicz]]  suggested in 1926 that one could improve on [[Hilbert system]]s as a basis for the axiomatic presentation of logic if one allowed the drawing of conclusions from assumptions in the inference rules of the logic.  In response to this, [[Stanisław Jaśkowski]] (1929) and [[Gerhard Gentzen]] (1934) independently provided such systems, called calculi of [[natural deduction]], with Gentzen's approach introducing the idea of symmetry between the grounds for asserting propositions, expressed in [[introduction rule]]s, and the consequences of accepting propositions in the [[elimination rule]]s, an idea that has proved very important in proof theory.<ref>{{harvtxt|Prawitz|1965|p=98}}.</ref>  Gentzen (1934) further introduced the idea of the [[sequent calculus]], a calculus advanced in a similar spirit that better expressed the duality of the logical connectives,{{sfn|Girard|Taylor|Lafont|2003}} and went on to make fundamental advances in the formalisation of intuitionistic logic,  and provide the first [[combinatorial proof]] of the consistency of [[Peano arithmetic]].  Together, the presentation of natural deduction and the sequent calculus introduced the fundamental idea of [[analytic proof]] to proof theory.

==Structural proof theory==
{{Main|Structural proof theory}}

Structural proof theory is the subdiscipline of proof theory that studies the specifics of [[proof calculi]]. The three most well-known styles of proof calculi are:
*The [[Hilbert system|Hilbert calculi]]
*The [[natural deduction calculus|natural deduction calculi]]
*The [[sequent calculus|sequent calculi]]

Each of these can give a complete and axiomatic formalization of [[propositional logic|propositional]] or [[predicate logic]] of either the [[classical logic|classical]] or [[intuitionistic logic|intuitionistic]] flavour, almost any [[modal logic]], and many [[substructural logic]]s, such as [[relevance logic]] or [[linear logic]].  Indeed, it is unusual to find a logic that resists being represented in one of these calculi.

Proof theorists are typically interested in 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-elimination theorem|cut-free]]. Much of the interest in cut-free proofs comes from the {{vanchor|subformula property}}: every formula in the end sequent of a cut-free proof is a subformula of one of the premises. This allows one to show consistency of the sequent calculus easily; if the empty sequent were derivable it would have to be a subformula of some premise, which it is not. Gentzen's midsequent theorem, the Craig interpolation theorem, and Herbrand's theorem also follow as corollaries of the cut-elimination theorem. 

Gentzen's 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 [[Natural deduction#Consistency.2C completeness.2C and normal forms|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 net]]s also support a notion of analytic proof.

A particular family of analytic proofs arising in [[reductive logic]] are [[focused proof]]s which characterise a large family of goal-directed proof-search procedures. The ability to transform a proof system into a focused form is a good indication of its syntactic quality, in a manner similar to how admissibility of cut shows that a proof system is syntactically consistent.<ref>{{Citation|last1=Chaudhuri|first1=Kaustuv|title=Focused and Synthetic Nested Sequents|date=2016|pages=390–407|place=Berlin, Heidelberg|publisher=Springer Berlin Heidelberg|isbn=978-3-662-49629-9|last2=Marin|first2=Sonia|last3=Straßburger|first3=Lutz|series=Lecture Notes in Computer Science |volume=9634 |doi=10.1007/978-3-662-49630-5_23}}</ref>

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 category|cartesian closed categories]].

Other research topics in structural theory include analytic tableau, which 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, and the proof theory of substructural logics.

==Ordinal analysis==
{{Main|Ordinal analysis}}

Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for subsystems of arithmetic, analysis, and set theory. [[Gödel's second incompleteness theorem]] is often interpreted as demonstrating that finitistic consistency proofs are impossible for theories of sufficient strength. Ordinal analysis allows one to measure precisely the infinitary content of the consistency of theories. For a consistent recursively axiomatized theory T, one can prove in finitistic arithmetic that the well-foundedness of a certain transfinite ordinal implies the consistency of T. Gödel's second incompleteness theorem implies that the well-foundedness of such an ordinal cannot be proved in the theory T.

Consequences of ordinal analysis include (1) consistency of subsystems of classical second order arithmetic and set theory relative to constructive theories, (2) combinatorial independence results, and (3) classifications of provably total recursive functions and provably well-founded ordinals.

Ordinal analysis was originated by Gentzen, who proved the consistency of Peano Arithmetic using [[transfinite induction]] up to ordinal ε<sub>0</sub>. Ordinal analysis has been extended to many fragments of first and second order arithmetic and set theory. One major challenge has been the ordinal analysis of impredicative theories. The first breakthrough in this direction was Takeuti's proof of the consistency of Π{{su|p=1|b=1}}-CA<sub>0</sub> using the method of ordinal diagrams.

==Provability logic==
{{Main|Provability logic}}

''Provability logic'' is a [[modal logic]], in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich [[theory (mathematical logic)|formal theory]]. As basic axioms of the provability logic GL ([[Kurt Gödel|Gödel]]-[[Martin Hugo Löb|Löb]]), which captures provable in [[Peano Arithmetic]], one takes modal analogues of the Hilbert-Bernays derivability conditions and [[Löb's theorem]] (if it is provable that the provability of A implies A, then A is provable).

Some of the basic results concerning the incompleteness of Peano Arithmetic and related theories have analogues in provability logic. For example, it is a theorem in GL that if a contradiction is not provable then it is not provable that a contradiction is not provable (Gödel's second incompleteness theorem). There are also modal analogues of the fixed-point theorem. [[Robert Solovay]] proved that the modal logic GL is complete with respect to Peano Arithmetic. That is, the propositional theory of provability in Peano Arithmetic is completely represented by the modal logic GL. This straightforwardly implies that propositional reasoning about provability in Peano Arithmetic is complete and decidable.

Other research in provability logic has focused on first-order provability logic, [[Japaridze's polymodal logic|polymodal provability logic]] (with one modality representing provability in the object theory and another representing provability in the meta-theory), and [[interpretability logic]]s intended to capture the interaction between provability and interpretability. Some very recent research has involved applications of graded provability algebras to the ordinal analysis of arithmetical theories.

==Reverse mathematics==
{{Main|Reverse mathematics}}

Reverse mathematics is a program in [[mathematical logic]] that seeks to determine which axioms are required to prove theorems of mathematics.{{sfn|Simpson|2010}} The field was founded by [[Harvey Friedman (mathematician)|Harvey Friedman]]. Its defining method can be described as "going backwards from the [[theorem]]s to the [[axiom]]s", in contrast to the ordinary mathematical practice of deriving theorems from axioms. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the [[axiom of choice]] and [[Zorn's lemma]] are equivalent over [[ZF set theory]]. The goal of reverse mathematics, however, is to study possible axioms of ordinary theorems of mathematics rather than possible axioms for set theory.

In reverse mathematics, one starts with a framework language and a base theory—a core axiom system—that is too weak to prove most of the theorems one might be interested in, but still powerful enough to develop the definitions necessary to state these theorems.  For example, to study the theorem "Every bounded sequence of [[real number]]s has a [[supremum]]" it is necessary to use a base system that can speak of real numbers and sequences of real numbers.

For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem. To show that a system ''S'' is required to prove a theorem ''T'', two proofs are required. The first proof shows ''T'' is provable from ''S''; this is an ordinary mathematical proof along with a justification that it can be carried out in the system ''S''. The second proof, known as a '''reversal''', shows that ''T'' itself implies ''S''; this proof is carried out in the base system. The reversal establishes that no axiom system ''S&prime;'' that extends the base system can be weaker than ''S'' while still proving&nbsp;''T''.

One striking phenomenon in reverse mathematics is the robustness of the ''Big Five'' axiom systems. In order of increasing strength, these systems are named by the initialisms RCA<sub>0</sub>, WKL<sub>0</sub>, ACA<sub>0</sub>, ATR<sub>0</sub>, and Π{{su|p=1|b=1}}-CA<sub>0</sub>. Nearly every theorem of ordinary mathematics that has been reverse mathematically analyzed has been proven equivalent to one of these five systems. Much recent research has focused on combinatorial principles that do not fit neatly into this framework, like RT{{su|p=2|b=2}} (Ramsey's theorem for pairs).

Research in reverse mathematics often incorporates methods and techniques from [[recursion theory]] as well as proof theory.

==Functional interpretations==
Functional interpretations are interpretations of non-constructive theories in functional ones. Functional interpretations usually proceed in two stages. First, one "reduces" a classical theory C to an intuitionistic one I. That is, one provides a constructive mapping that translates the theorems of C to the theorems of I. Second, one reduces the intuitionistic theory I to a quantifier free theory of functionals F. These interpretations contribute to a form of Hilbert's program, since they prove the consistency of classical theories relative to constructive ones. Successful functional interpretations have yielded reductions of infinitary theories to finitary theories and impredicative theories to predicative ones.

Functional interpretations also provide a way to extract constructive information from proofs in the reduced theory. As a direct consequence of the interpretation one usually obtains the result that any recursive function whose totality can be proven either in I or in C is represented by a term of F. If one can provide an additional interpretation of F in I, which is sometimes possible, this characterization is in fact usually shown to be exact. It often turns out that the terms of F coincide with a natural class of functions, such as the primitive recursive or polynomial-time computable functions. Functional interpretations have also been used to provide ordinal analyses of theories and classify their provably recursive functions.

The study of functional interpretations began with Kurt Gödel's interpretation of intuitionistic arithmetic in a quantifier-free theory of functionals of finite type. This interpretation is commonly known as the [[Dialectica interpretation]]. Together with the double-negation interpretation of classical logic in intuitionistic logic, it provides a reduction of classical arithmetic to intuitionistic arithmetic.

==Formal and informal proof==<!-- This section is linked from [[Black–Scholes]] and [[Mathematical proof]]-->
{{Main |Formal 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 is too pedantic and long-winded to be in common use.

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 simple, whereas ''finding'' proofs ([[automated theorem proving]]) is generally hard. An informal proof in the mathematics literature, by contrast, requires weeks of [[peer review]] to be checked, and may still contain errors.

==Proof-theoretic semantics==
{{Main|Proof-theoretic semantics|Logical harmony}}

In [[linguistics]], [[type-logical grammar]], [[categorial grammar]] and [[Montague grammar]] apply formalisms based on structural proof theory to give a formal [[natural language semantics]].

==See also==
{{Portal|Philosophy}}
* [[Intermediate logic]]
* [[Model theory]]
* [[Proof (truth)]]
* [[Proof techniques]]
* [[Sequent calculus]]

==Notes==
<references/>

==References==
* J. Avigad and 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.
* {{cite book|last1=Barwise |first1=Jon |author-link=Jon Barwise |year=1977 |title=Handbook of Mathematical Logic |series=Studies in Logic and the Foundations of Mathematics |volume=90 |isbn=072042285X |oclc=2347202 |publisher=North-Holland Publishing Company |lccn=76026032}} {{IAp|https://archive.org/details/handbookofmathem0090unse}}
* S. Buss, ed. (1998) ''[https://books.google.com/books?id=MfTMDeCq7ukC&dq=%22Handbook+of+Proof+Theory%22&pg=PP1 Handbook of Proof Theory].'' Elsevier.
* G. Gentzen (1935/1969).  "[https://www.jstor.org/stable/20009142 Investigations into logical deduction]". In M. E. Szabo, ed. ''Collected Papers of Gerhard Gentzen''. North-Holland.  Translated by Szabo from "Untersuchungen über das logische Schliessen", ''Mathematisches Zeitschrift'' v. 39, pp.&nbsp;176–210, 405&nbsp;431.
* {{cite book|last1=Girard |first1=J.-Y. |author-link1=Jean-Yves Girard |last2=Taylor |first2=P. |last3=Lafont |first3=Y. |year=2003 |orig-date=1989 |publisher=Cambridge University Press |url=https://www.irif.fr/~mellies//mpri/mpri-ens/biblio/proofs-and-types.pdf |title=Proofs and Types |isbn=0521371813}}
* {{Prawitz Natural Deduction|1965}} {{sfn whitelist|CITEREFPrawitz1965}}
* {{cite book |first=S. G. |last=Simpson |title=Subsystems of Second-order Arithmetic |edition=2 |year=2010 |publisher=Cambridge University Press |series=Perspectives in logic |isbn=9780521150149 |oclc=528432422}}
* [[A. S. Troelstra]] and H. Schwichtenberg (1996). ''Basic Proof Theory'', Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, {{isbn|0-521-77911-1}}.
* {{cite book|last=Wang |first=Hao |author-link=Hao Wang (academic) |title=Popular Lectures on Mathematical Logic |year=1981 |isbn=9780442231095 |publisher=[[Van Nostrand (publisher)|Van Nostrand Reinhold Company]] |oclc=6087107 |url=https://archive.org/details/popularlectureso0000wang |url-access=registration}}

==External links==
{{Commonscat}}
*{{Springer |title=Proof theory |id=p/p075430}}
*J. von Plato (2008). [http://plato.stanford.edu/entries/proof-theory-development/ The Development of Proof Theory]. [[Stanford Encyclopedia of Philosophy]].

{{Mathematical logic}}
{{Authority control}}

[[Category:Proof theory| ]]
[[Category:Mathematical logic| P]]
[[Category:Metalogic]]