SAS

Abstract

Our proof theoretic programme, which is a form of a revised Hilbert's Programme, is to prove the consistency of proof theoretically strong theories via an ordinal analysis to predicatively justified extensions of Martin-Loef Type Type Theory. This gives rise to new data types, which can be used outside type theory as well. We will report on 3 extensions found this way: induction-recursion, induction-induction and weakly final coalgebras in dependent type theory.

Induction-recursion was originally introduced by Peter Dybjer in order to obtain a type theory which includes all possible extensions of type theory considered as acceptable at that time. We consider a closed formalisation by having one data type the elements of which are representatives of arbitrary inductive-recursive definitions. This data type has been applied to generic programming.

A (proof theoretic weak) variant of induction-recursion is called induction-induction, and has been investigated in collaboration with my PhD student Fredrik Forsberg. Variants of this concept occur frequently in mathematics, when one defines a set simultaneously with an order on it, and both are defined mutually inductively. An example are Conway's surreal numbers.

Finally we look at weakly final coalgebras in dependent type theory, where the role of elimination and and introduction rules are interchanged.