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.
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
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.
This has led, in particular, to: In parallel to the rise and fall of Hilbert's program, the foundations of structural proof theory were being founded.
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 rules, and the consequences of accepting propositions in the elimination rules, an idea that has proved very important in proof theory.
[2] 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,[3] 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.
Gentzen's natural deduction calculus also supports a notion of analytic proof, as shown by Dag Prawitz.
[4] 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.
Gödel's second incompleteness theorem is often interpreted as demonstrating that finitistic consistency proofs are impossible for theories of sufficient strength.
The point is to capture the notion of a proof predicate of a reasonably rich formal theory.
Some of the basic results concerning the incompleteness of Peano Arithmetic and related theories have analogues in provability logic.
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.
Some very recent research has involved applications of graded provability algebras to the ordinal analysis of arithmetical theories.
Much recent research has focused on combinatorial principles that do not fit neatly into this framework, like RT22 (Ramsey's theorem for pairs).
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.
An informal proof in the mathematics literature, by contrast, requires weeks of peer review to be checked, and may still contain errors.