A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory
Dybjer, Peter
J. Symbolic Logic, Tome 65 (2000) no. 1, p. 525-549 / Harvested from Project Euclid
The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Lof's universe a la Tarski. A set U$_0$ of codes for small sets is generated inductively at the same time as a function T$_0$, which maps a code to the corresponding small set, is defined by recursion on the way the elements of U$_0$ are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is implicit in Martin-Lof's intuitionistic type theory. We extend previously given schematic formulations of inductive definitions in type theory to encompass a general notion of simultaneous induction-recursion. This enables us to give a unified treatment of several interesting constructions including various universe constructions by Palmgren, Griffor, Rathjen, and Setzer and a constructive version of Aczel's Frege structures. Consistency of a restricted version of the extension is shown by constructing a realisability model in the style of Allen.
Publié le : 2000-06-14
Classification: 
@article{1183746062,
     author = {Dybjer, Peter},
     title = {A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory},
     journal = {J. Symbolic Logic},
     volume = {65},
     number = {1},
     year = {2000},
     pages = { 525-549},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183746062}
}
Dybjer, Peter. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. J. Symbolic Logic, Tome 65 (2000) no. 1, pp.  525-549. http://gdmltest.u-ga.fr/item/1183746062/