Topological inductive definitions

Annals of Pure and Applied Logic 163 (11):1471-1483 (2012)

In intuitionistic generalized predicative systems as constructive set theory, or constructive type theory, two categories have been proposed to play the role of the category of locales: the category FSp of formal spaces, and its full subcategory FSpi of inductively generated formal spaces. Considered in impredicative systems as the intuitionistic set theory IZF, FSp and FSpi are both equivalent to the category of locales. However, in the mentioned predicative systems, FSp fails to be closed under basic constructions such as that of finite products, while FSpi is complete , but does not contain some naturally occurring classes of formal spaces. Moreover, completeness of FSpi only holds under the assumption of strong principles for the existence of inductively defined sets.In this paper, working in the context of constructive set theory, the category ImLoc of imaginary locales is introduced. ImLoc is complete already over weak formulations of constructive set theory, contains FSp and FSpi as full subcategories, and, as FSp and FSpi, is equivalent to the category of locales in IZF.Applications of the concept of imaginary locale to a proof of a point-free version of Tychonoff embedding theorem, and to set-representation theorems, are then presented
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2011.12.005
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 38,984
External links

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

Inductively Generated Formal Topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
Aspects of General Topology in Constructive Set Theory.Peter Aczel - 2006 - Annals of Pure and Applied Logic 137 (1):3-29.
Heyting-Valued Interpretations for Constructive Set Theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1):164-188.
On the Constructive Dedekind Reals.Robert S. Lubarsky & Michael Rathjen - 2008 - Logic and Analysis 1 (2):131-152.
On the Collection of Points of a Formal Space.Giovanni Curi - 2006 - Annals of Pure and Applied Logic 137 (1):126-146.

View all 13 references / Add more references

Citations of this work BETA

Abstract Inductive and Co-Inductive Definitions.Giovanni Curi - 2018 - Journal of Symbolic Logic 83 (2):598-616.

Add more citations

Similar books and articles

Quantifiers, Games and Inductive Definitions.Peter Aczel - 1975 - In Stig Kanger (ed.), Journal of Symbolic Logic. Elsevier. pp. 1--14.
Functional Interpretation and Inductive Definitions.Jeremy Avigad & Henry Towsner - 2009 - Journal of Symbolic Logic 74 (4):1100-1120.
Global Inductive Definability.Jon Barwise & Yiannis N. Moschovakis - 1978 - Journal of Symbolic Logic 43 (3):521-534.
Monotone Inductive Definitions in Explicit Mathematics.Michael Rathjen - 1996 - Journal of Symbolic Logic 61 (1):125-146.
Dynamic Topological S5.Philip Kremer - 2009 - Annals of Pure and Applied Logic 160 (1):96-116.


Added to PP index

Total views
4 ( #936,914 of 2,319,413 )

Recent downloads (6 months)
2 ( #598,472 of 2,319,413 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature