Overlap Algebras as Almost Discrete Locales

TL;DR

This paper explores the concept of almost discrete locales in constructive logic, proposing that Sambin's overlap algebras serve as a constructive analogue to Boolean locales, which are classically discrete but not constructively so.

Contribution

It introduces overlap algebras as a constructive substitute for Boolean locales, highlighting their properties and relation to discrete locales under intuitionistic logic.

Findings

Overlap algebras include all discrete locales

They are the smallest strongly dense sublocales of overt locales

They coincide with Boolean locales when LEM holds

Abstract

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.