David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 65 (2):525-549 (2000)
The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löf's universe á 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-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
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
Erik Palmgren (2006). Regular Universes and Formal Spaces. Annals of Pure and Applied Logic 137 (1):299-316.
Similar books and articles
Erik Palmgren (1991). A Construction of Type: Type in Martin-Löf's Partial Type Theory with One Universe. Journal of Symbolic Logic 56 (3):1012-1015.
John Bell (2008). The Axiom of Choice and the Law of Excluded Middle in Weak Set Theories. Mathematical Logic Quarterly 54 (2):194-201.
Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. Journal of Philosophical Logic 18 (4):399 - 422.
Toshiyasu Arai (2004). Wellfoundedness Proofs by Means of Non-Monotonic Inductive Definitions I: Π₂⁰-Operators. Journal of Symbolic Logic 69 (3):830-850.
Lars Hallnäs (2006). On the Proof-Theoretic Foundation of General Definition Theory. Synthese 148 (3):589 - 602.
Klaus Aehlig (2005). Induction and Inductive Definitions in Fragments of Second Order Arithmetic. Journal of Symbolic Logic 70 (4):1087 - 1107.
Ralph Matthes (2002). Tarski's Fixed-Point Theorem and Lambda Calculi with Monotone Inductive Types. Synthese 133 (1-2):107 - 129.
Nicola Gambino & Peter Aczel (2006). The Generalised Type-Theoretic Interpretation of Constructive Set Theory. Journal of Symbolic Logic 71 (1):67 - 103.
Adam Obtułowicz (1989). Categorical and Algebraic Aspects of Martin-Löf Type Theory. Studia Logica 48 (3):299 - 317.
Added to index2009-01-28
Total downloads2 ( #345,621 of 1,099,035 )
Recent downloads (6 months)1 ( #287,293 of 1,099,035 )
How can I increase my downloads?