Cut-elimination (Gentzen Hauptsatz)

Gentzen's Hauptsatz: every LK (or LJ) proof can be transformed into a cut-free proof. Gentzen 1935. Immediate corollaries: subformula property, consistency of first-order logic, and the Herbrand and interpolation theorems. Extending to…