Constructive version of Boolean algebra
Francesco Ciraulo, Maria Emilia Maietti, Paola Toto

TL;DR
This paper develops a constructive framework for Boolean algebras using overlap algebras, providing new characterizations and generalizations that align with constructive mathematics principles.
Contribution
It introduces a constructive approach to Boolean algebras via overlap algebras, including new properties, descriptions, and generalizations of morphisms.
Findings
Overlap morphisms correspond classically to join-preserving maps
Atomic overlap algebras are characterized in formal topology
Power-collections form free overlap algebras from sets
Abstract
The notion of overlap algebra introduced by G. Sambin provides a constructive version of complete Boolean algebra. Here we first show some properties concerning overlap algebras: we prove that the notion of overlap morphism corresponds classically to that of map preserving arbitrary joins; we provide a description of atomic set-based overlap algebras in the language of formal topology, thus giving a predicative characterization of discrete locales; we show that the power-collection of a set is the free overlap algebra join-generated from the set. Then, we generalize the concept of overlap algebra and overlap morphism in various ways to provide constructive versions of the category of Boolean algebras with maps preserving arbitrary existing joins.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Advanced Algebra and Logic
