Cut-Elimination and the Subformula Property

Gentzen proved the cut-elimination theorem (his Hauptsatz) in a 1934 paper. This implies that if a formula is provable, then it is provable "without detours". In particular, we have the "subformula property" that all formulae in a (cut-free) derivation are subformulae of the endsequent formulas. Other consequences include consistency of predicate calculus, decidability of intuitionistic propositional logic, and unprovability of excluded middle in intuitionistic propositional logic.

In a 1971 paper, Andrews proved cut-elimination for a system of elementary type theory. Andrews also proves weak normalization for simply typed lambda terms. Actually, since via the Curry-Howard isomorphism cut elimination in intuitionistic implicational logic corresponds to beta-normalization of simply typed lambda terms (see Hindley 1997, Chapter 6), this can also be considered a cut elimination result. (Isn't that clever?) Leivant surveys the cut elimination results in higher-order logic.