proof theory



Proof theory is the part of mathematical logic concerned with the notion of proof. It was introduced by David Hilbert under the name Beweistheorie as part of Hilbert's program. Since Gödel's incompleteness theorem put an end to the original version of Hilbert’s program, proof theory has broadened its scope to include the following:

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

  • Reductive proof theory This is modern version of Hilbert's program, in which we don’t hope to secure all of mathematics with finitistic means, but rather ask: what rests on what? That is, we find reductions between various systems, showing for example that some classical systems can be reduced to constructive systems, or some systems which use a priori impredicative principles can nevertheless be reduced to predicative systems. See also: reverse mathematics.

  • Ordinal analysis Here one analyzes the provably well-founded recursive ordinals and provably total recursive functions? of a theory by devising suitable proof calculi

  • Proof mining Here one 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.


Revised on June 14, 2016 11:57:18 by Urs Schreiber (