Overlap Algebras as Almost Discrete Locales
From MaRDI portal
Publication:6137844
DOI10.46298/LMCS-19(4:21)2023arXiv1601.04830OpenAlexW2264357731MaRDI QIDQ6137844FDOQ6137844
Publication date: 16 January 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: Boolean locales are "almost discrete", in the sense that a spatial Boolean locale is the same thing as the frame of open subsets of a discrete space, that is, the powerset of a set. This basic fact, however, cannot be proven constructively, that is, over intuitionistic logic. Actually, Boolean locales are almost discrete if and only if the law of excluded middle (LEM) holds. In fact, discrete locales are never Boolean constructively, except for the trivial locale. So, what is an almost discrete locale constructively? Our claim is that Sambin's Overlap Algebras have good enough features to deserve to be called that. Namely, they include the class of discrete locales, they arise as smallest strongly dense sublocales (of overt locales), and hence they coincide with the Boolean locales if LEM holds.
Full work available at URL: https://arxiv.org/abs/1601.04830
Cites Work
- Frames and Locales
- An extension of the Galois theory of Grothendieck
- Title not available (Why is that?)
- Title not available (Why is that?)
- On some peculiar aspects of the constructive theory of point-free spaces
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The overlap algebra of regular opens
- Constructive version of Boolean algebra
- Regular opens in constructive topology and a representation theorem for overlap algebras
- Title not available (Why is that?)
This page was built for publication: Overlap Algebras as Almost Discrete Locales
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137844)
