| Summary: | 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.
|
|---|