Switch to: References

Citations of:

Tychonoff's theorem in the framework of formal topologies

Sara Negri & Silvio Valentini

Journal of Symbolic Logic 62 (4):1315-1332 (1997)

Add citations

You must login to add citations.

Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.details Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...) Download Export citation Bookmark 44 citations
Cosheaves and connectedness in formal topology.Steven Vickers - 2012 - Annals of Pure and Applied Logic 163 (2):157-174.details Download Export citation Bookmark 1 citation
Compactness in locales and in formal topology.Steven Vickers - 2006 - Annals of Pure and Applied Logic 137 (1-3):413-438.details If a locale is presented by a “flat site”, it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and sufficient condition is derived for compactness of the locale . Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies. A predicative proof of the binary Tychonoff theorem is given, including a characterization of the finite covers of the product by basic opens. The discussion (...) Download Export citation Bookmark 8 citations
The problem of the formalization of constructive topology.Silvio Valentini - 2005 - Archive for Mathematical Logic 44 (1):115-129.details Abstract.Formal topologies are today an established topic in the development of constructive mathematics. One of the main tools in formal topology is inductive generation since it allows to introduce inductive methods in topology. The problem of inductively generating formal topologies with a cover relation and a unary positivity predicate has been solved in [CSSV]. However, to deal both with open and closed subsets, a binary positivity predicate has to be considered. In this paper we will show how to adapt to (...) Download Export citation Bookmark 10 citations
The intensional side of algebraic-topological representation theorems.Sara Negri - 2017 - Synthese 198 (Suppl 5):1121-1143.details Stone representation theorems are a central ingredient in the metatheory of philosophical logics and are used to establish modal embedding results in a general but indirect and non-constructive way. Their use in logical embeddings will be reviewed and it will be shown how they can be circumvented in favour of direct and constructive arguments through the methods of analytic proof theory, and how the intensional part of the representation results can be recovered from the syntactic proof of those embeddings. Analytic (...) Download Export citation Bookmark 1 citation

1