Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Overlap Algebras as Almost Discrete Locales

Francesco Ciraulo

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.

Overlap Algebras as Almost Discrete Locales

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.

Paper Structure

This paper contains 11 sections, 10 theorems, 13 equations.

Table of Contents

  1. Introduction
  2. Preliminaries about frames and locales
  3. Sublocales
  4. The sublocale generated by a family of elements.
  5. The nucleus "generated" by a closure operator.
  6. Boolean locales
  7. Fact:
  8. Overlap algebras
  9. O-algebras are smallest strongly dense sublocales
  10. Discrete spaces and spatial o-algebras
  11. A Brouwerian counterexample

Key Result

Proposition 2.1

If there exists a locale $X$ with the following two properties then $\Omega$ is Boolean, that is, LEM holds.

Theorems & Definitions (20)

  • Proposition 2.1
  • proof
  • Definition 3.1
  • Definition 3.2
  • Proposition 3.3
  • proof
  • Proposition 3.4
  • proof
  • Lemma 3.5
  • proof
  • ...and 10 more