Primitive-recursion done with very feeble predicative universes

Peter Hancock. Part of the proofs, constructions and computations seminar series.

Schwichtenberg (60's) showed that the numerical functions definable by closed terms of the simply typed lambda calculus (NB: no Nat!) are precisely the "generalised polynomials", defined from linear functions, sg, and sgbar by addition, multiplication and composition. One non-example is the parity function, others are exponentiation and predecessor.  These functions *can* be represented in a more liberal sense by certain metamathematical objects, in which type-operations such as (X |-> X->X) play a key role.

However, to iterate such operations (to define tetration from exponentiation, or subtraction from predecessor) internally needs universes that are closed under the relevant type operations.  I'll show a way to obtain all the primitive recursive functions, by iterating (externally) a type-2 universe operator. Some discussion of what exactly is universal about my universes may be attempted.

One might conjecture that all the functions in Godel's T are obtainable with suitable externally indexed universe operators.