arnold beckmann
Analyzing Gödel's T via expanded head reduction trees
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).