Proof theory, a form of metamathematics, studies the ways in which proofss are used in mathematics. However, in contrast to common mathematics, statements and proofs in proof theory are purely formal. This means that they are specified in a formal language that usually employs some symbolic logic.
Therefore, on the one hand, proof theory admits no ambiguity. On the other hand, it is restricted to those statements that can be expressed in the chosen language. In this strictly formal sense, proof theory is not necessarily a form of metamathematics, but can have immediate applications in artificial intelligence, where automated deduction plays an important role.
Proof theory studies how tautologies can be proven with the help of some formal calculus. Based on the axioms and rules of inference of such a system, derivations of logical statements are constructed. These derivations constitute formal proofs of the statements.
As such, proof theory is related to syntax in logic; model theory correspondingly relates to semantics. The method of proof theory is to consider proofs as combinatorial objects, or examples of data structures, in their own right. As such they may be manipulated or operated on systematically, the set of all proofs in a formal language being itself a formal language.
In some situations, the term proof theory may be used to refer to a concrete calculus. For example, one may state that there is no proof theory for second-order logic, meaning that there is no syntactical calculus for this logic that simultaneously (1) is sound, and (2) is complete, and (3) admits a proof-checking algorithm. First-order logic and many logics "below" admit a proof theory.
Historically, the field was established by David Hilbert, generally considered one of the greatest mathematicians of the late 19th and early 20th century. The major step forward technically speaking was the work of Gerhard Gentzen on the method of cut-elimination. See the pages sequent and sequent calculus.
Proof theory, model theory, axiomatic set theory, and recursion theory are the so-called "four theories" of the foundations of mathematics.