# Primitive-recursion done with very feeble predicative universes

**Date**: Wednesday 17 January 2018, 14:00 – 15:00**Location**: Mathematics Level 8, MALL 2, School of Mathematics**Type**: Proofs, Constructions and Computations, Seminars, Pure Mathematics**Cost**: Free

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