Arnold Beckmann and Andreas Weiermann
Mathematical Logic Quarterly, Volume 46, Issue 4, Pages 517-536
Publication year: 2000

Inspired from Buchholz’ ordinal analysis of ID_1 and Beckmann’s analysis of the simple typed λ – calculus we classify the derivation lengths for Gödel’s system T in the λ – formulation (where the η – rule is included).