Derivation Lengths Classification of Gödel's T Extending Howard's Assignment

Gunnar Wilken, Andreas Weiermann

Let T be Goedel's system of primitive recursive functionals of finite type in the lambda formulation. We define by constructive means using recursion on nested multisets a multival…