Structural proof theory is concerned with the structure of proofs and perspicuous proof calculi for elucidating this structure. This leads to the study of sequent calculi and of natural deduction.

Reductive proof theory is the modern version of Hilbert's program: Instead of hoping to secure all of mathematics with finitistic means, one ask: what rests on what?

That is, one asks for reductions between various formal systems, showing for example that some classical systems can be reduced to constructive systems, or some systems which use a prioriimpredicative principles can nevertheless be reduced to predicative systems. See also: reverse mathematics.

Proof mining analyzes proofs of specific statements in order to extract more information than the mere truth of the statement, for instance witnesses or bounds on witnesses of existential statements.