[Prev][Next][Index][Thread]

Paper: A Finite Axiomatization of Inductive-Recursive Definitions

We would like to announce the availablity of the following articles 
under the addresses

        http://www.math.uu.se/~setzer/articles/welcome.html
 and 
        http://www.md.chalmers.se/~peterd

As always, comments are welcome.

Peter Dybjer, Anton Setzer
--------------------------------------------------------------------

   A Finite Axiomatization of Inductive-Recursive Definitions
   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

         Peter Dybjer                       Anton Setzer
Chalmers University of Technology        Uppsala University

Abstract: 

Induction-recursion is the main principle for introducing new sets in 
Martin-Loef's Type Theory. It states that we may inductively define a set 
while simultaneously defining a function from this set into an arbitrary
type by structural recursion. This extends the notion of an
inductively defined set substantially and allows to introduce 
universes and higher order universes (but no Mahlo universe).

In this article we give a finite axiomatization of 
inductive-recursive definitions. We will prove consistency by constructing
a set theoretic model, which makes use of one Mahlo cardinal.