Francesco Ciraulo - Overlap Algebras as Almost Discrete Locales

lmcs:7525 - Logical Methods in Computer Science, December 8, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:21)2023
Overlap Algebras as Almost Discrete LocalesArticle

Authors: Francesco Ciraulo

    Boolean locales are "almost discrete", in the sense that a spatial Boolean locale is just a discrete locale (that is, it corresponds to the frame of open subsets of a discrete space, namely the powerset of a set). This basic fact, however, cannot be proven constructively, that is, over intuitionistic logic, as it requires the full law of excluded middle (LEM). 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.


    Volume: Volume 19, Issue 4
    Published on: December 8, 2023
    Accepted on: September 15, 2023
    Submitted on: May 28, 2021
    Keywords: Mathematics - Logic,Mathematics - Category Theory,Mathematics - General Topology
    Funding:
      Source : OpenAIRE Graph
    • Computing with Infinite Data; Funder: European Commission; Code: 731143

    Consultation statistics

    This page has been seen 1133 times.
    This article's PDF has been downloaded 199 times.