Intermediate · a field of logic
Proof Theory
Proofs as objects of study: natural deduction, the sequent calculus, and cut-elimination, the structure of demonstration itself.
- The problem
- What is a proof, as a mathematical object, and can every detour through a lemma be eliminated?
- The turning point
- Gentzen’s cut-elimination (Hauptsatz): every sequent proof can be rewritten without the cut rule, yielding the subformula property.
- An open question
- How far can ordinal analysis measure the strength of strong theories, and what lies past current reach?
The Canon
- Collected Papers 1934–35
- Proof Theory
To study it
- Basic Proof Theory
- Proofs and Types
- Structural Proof Theory