Compactness in Locales and in Formal Topology

Research output: Contribution to journalArticlepeer-review

Colleges, School and Institutes


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 suffcient condition is derived for compactness of the locale (and also forits openness). 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 is then related to the double powerlocale.


Original languageEnglish
Pages (from-to)413-438
Number of pages26
JournalAnnals of Pure and Applied Logic
Issue number1-3
Publication statusPublished - 1 Jan 2006