A finite axiomatization of inductive-recursive denitions

Abstract

Induction-recursion is a schema which formalizes the principles for introducing new sets in Martin-Löf ‘s type theory. It states that we may inductively dene a set while simultaneously dening a function from this set into an arbitrary type by structural recursion. This extends the notion of an inductively dened set substantially and allows us to introduce universes and higher order universes (but not a Mahlo universe). In this article we give a nite axiomatization of inductive-recursive denitions. We prove consistency by constructing a set-theoretic model which makes use of one Mahlo cardinal.