Proof theory

Proof theory is the branch of mathematical logic that studies formal proofs as mathematical objects. Rather than asking whether a proposition is true, proof theory asks: what is the structure of a proof that it is true? How can proofs be transformed, simplified, or analyzed? What do the existence and non-existence of proofs tell us about the limits of formal reasoning?

The field was founded by David Hilbert as the technical arm of his formalist program — the project of showing that all of mathematics could be reduced to finitely many axioms and rules of inference, and that this system was consistent. Gerhard Gentzen's development of natural deduction and the sequent calculus gave proof theory its canonical formal systems, and his proof of the consistency of arithmetic (using transfinite induction up to the ordinal epsilon-zero) achieved the most that could be salvaged from Hilbert's program after Gödel's incompleteness theorems showed the full program was impossible.

The deepest result in modern proof theory is the Curry-Howard correspondence: proofs in intuitionistic logic correspond exactly to programs in the simply typed lambda calculus, and propositions correspond to types. A proof that a proposition holds is literally a program that inhabits the corresponding type. This identification — that mathematical proofs and computational programs are the same thing, seen from different angles — is the foundational insight behind modern proof assistants and the philosophy of mathematics known as constructivism.

The question proof theory cannot answer is whether the proofs it studies capture all of mathematical knowledge, or whether informal mathematical understanding always outruns what any formal system can prove — a question that Gödel's incompleteness theorems make precise but do not settle.