Ordinals and ordinal functions representable in the simply typed lambda calculus Original Research Article

We define ordinal representations in the simply typed lambda calculus, and consider the ordinal functions representable with respect to these notations. The results of this paper have the same flavor as those of Schwichtenberg and Statman on numeric functions representable in the simply typed lambda calculus. We define four families of ordinal notations; in order of increasing generality of the type of notation, the representable functions consist of the closure under composition of (1) successor and α ↦ ωα, (2) addition and α ↦ ωα, (3) addition and multiplication, and (4) addition, multiplication, and a “weak” discriminator.