Francesco Ciraulo ; Michele Contente - Overlap Algebras: a Constructive Look at Complete Boolean Algebras

lmcs:5417 - Logical Methods in Computer Science, February 13, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:13)2020
Overlap Algebras: a Constructive Look at Complete Boolean AlgebrasArticle

Authors: Francesco Ciraulo ; Michele Contente

    The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although classically equivalent to that of a complete Boolean algebra, has powersets and other natural structures as instances. In this paper we study the category of overlap algebras as an extension of the category of sets and relations, and we establish some basic facts about mono-epi-isomorphisms and (co)limits; here a morphism is a symmetrizable function (with classical logic this is just a function which preserves joins). Then we specialize to the case of morphisms which preserve also finite meets: classically, this is the usual category of complete Boolean algebras. Finally, we connect overlap algebras with locales, and their morphisms with open maps between locales, thus obtaining constructive versions of some results about Boolean locales.


    Volume: Volume 16, Issue 1
    Published on: February 13, 2020
    Accepted on: October 11, 2019
    Submitted on: May 1, 2019
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic
    Funding:
      Source : OpenAIRE Graph
    • Computing with Infinite Data; Funder: European Commission; Code: 731143

    Consultation statistics

    This page has been seen 1576 times.
    This article's PDF has been downloaded 610 times.