David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 54 (1):57-64 (1989)
In this paper, we show that non-well-founded sets can be defined constructively by formalizing Hallnäs' limit definition of these within Martin-Löf's theory of types. A system is a type W together with an assignment of ᾱ ∈ U and α̃ ∈ ᾱ → W to each α ∈ W. We show that for any system W we can define an equivalence relation = w such that α = w β ∈ U and = w is the maximal bisimulation. Aczel's proof that CZF can be interpreted in the type V of iterative sets shows that if the system W satisfies an additional condition (*), then we can interpret CZF minus the set induction scheme in W. W is then extended to a complete system W * by taking limits of approximation chains. We show that in W * the antifoundation axiom AFA holds as well as the axioms of CFZ -
|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
No citations found.
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.
Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. Journal of Philosophical Logic 18 (4):399 - 422.
Nicola Gambino & Peter Aczel (2006). The Generalised Type-Theoretic Interpretation of Constructive Set Theory. Journal of Symbolic Logic 71 (1):67 - 103.
Wolfgang Merkle & Nenad Mihailović (2004). On the Construction of Effectively Random Sets. Journal of Symbolic Logic 69 (3):862-878.
Jacob Lurie (1999). Anti-Admissible Sets. Journal of Symbolic Logic 64 (2):407-435.
Jan Smith (1984). An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions. Journal of Symbolic Logic 49 (3):730-753.
Peter Dybjer (2000). A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic 65 (2):525-549.
Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.
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 downloads8 ( #192,639 of 1,410,540 )
Recent downloads (6 months)1 ( #178,988 of 1,410,540 )
How can I increase my downloads?