Editing Proof theory (section)

==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.