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.