Article contents
A general formulation of simultaneous inductive-recursive definitions in type theory
Published online by Cambridge University Press: 12 March 2014
Abstract
The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löfs universe à la Tarski. A set U0 of codes for small sets is generated inductively at the same time as a function T0, which maps a code to the corresponding small set, is defined by recursion on the way the elements of U0 are generated.
In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is implicit in Martin-Löf'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.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2000
References
REFERENCES
- 95
- Cited by