Interpreting inductive-inductive definitions as indexed inductive definitions

Date(s): Friday 12th November 2010 (15:00-16:00)
Contact: Nils Anders Danielsson
Description: Speaker: Fredrik Nordvall Forsberg (Swansea)
Abstract:Induction is a powerful and important principle of definition, especially so in dependent type theory and constructive mathematics.Induction-induction (named in reference to Dybjer and Setzer'sinduction-recursion) is an induction principle which gives the possibility to simultaneously introduce a set A together with an A-indexed set B (i.e. for every a : A, B(a) is a set). Both A and B(a) are inductively defined, and the constructors for A can also refer to B and vice versa.In recent work, we have formalised inductive-inductive definitions and thus made meta-mathematical analysis of the theory possible. In this talk, I will sketch the first result of this kind. I will show that the theory of inductive-inductive definitions can be interpreted in the theory of indexed inductive definitions. In particular, this shows that both theories have the same proof-theoretical strength.

School of Computer Science

University of Nottingham
Jubilee Campus
Wollaton Road
Nottingham, NG8 1BB

For all enquires please visit:
www.nottingham.ac.uk/enquire