# 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.