[Prev][Next][Index][Thread]
Paper: A Finite Axiomatization of InductiveRecursive Definitions

To: types@cs.indiana.edu

Subject: Paper: A Finite Axiomatization of InductiveRecursive Definitions

From: Peter Dybjer <peterd@cs.chalmers.se>

Date: Wed, 22 Apr 1998 15:26:41 +0200 (MET DST)

DeliveryDate: Wed, 22 Apr 1998 08:26:53 0500
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 InductiveRecursive Definitions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Peter Dybjer Anton Setzer
Chalmers University of Technology Uppsala University
Abstract:
Inductionrecursion is the main principle for introducing new sets in
MartinLoef'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
inductiverecursive definitions. We will prove consistency by constructing
a set theoretic model, which makes use of one Mahlo cardinal.