Constructive version of Boolean algebra.

*(English)*Zbl 1272.03160Complete Boolean algebras, because of Tarski’s representation theorem which relates them with powersets, do not fit in a constructive and predicative foundation. In the constructive but impredicative framework, Joyal and Tierney have shown that discrete locales characterise powersets, while in the constructive and predicative framework, Sambin has shown that overlap algebras provide a constructive version of complete Boolean algebras.

This article takes one step further starting from Sambin’s achievements. In fact, after introducing overlap algebras and their relation with formal topology, it proves that, classically, every complete Boolean algebra is an overlap algebra. From this point, it introduces a suitable notion of morphism for overlap algebras which, in a classical interpretation, reduces to the one of maps preserving arbitrary joins. Thus, the authors deduce that the category of complete Boolean algebras is classically equivalent to the sub-category of overlap algebras whose morphisms also preserve finite meets.

Then, the article introduces the notion of discrete formal topology, thus giving a predicative characterisation of discrete locales: in particular, every atomic overlap algebra is isomorphic to the powerset of its atoms. Also, constructively, the power-collection of a set \(X\) is proved to be isomorphic to the free overlap algebra over \(X\).

By extending and enriching in many ways the notions of overlap algebra and overlap morphism, the authors show that the corresponding categories are all equivalent to the category of Boolean algebras with maps preserving joins.

The paper contains a number of relevant and useful results for anyone who is interested in studying or using Boolean algebras in a constructive and predicative framework. Furthermore, it clearly shows how constructive mathematics provides a richer point of view over classical concepts – Boolean algebras in this case – where fine information and how it is preserved plays a fundamental role in the generation of the structures of interest.

This article takes one step further starting from Sambin’s achievements. In fact, after introducing overlap algebras and their relation with formal topology, it proves that, classically, every complete Boolean algebra is an overlap algebra. From this point, it introduces a suitable notion of morphism for overlap algebras which, in a classical interpretation, reduces to the one of maps preserving arbitrary joins. Thus, the authors deduce that the category of complete Boolean algebras is classically equivalent to the sub-category of overlap algebras whose morphisms also preserve finite meets.

Then, the article introduces the notion of discrete formal topology, thus giving a predicative characterisation of discrete locales: in particular, every atomic overlap algebra is isomorphic to the powerset of its atoms. Also, constructively, the power-collection of a set \(X\) is proved to be isomorphic to the free overlap algebra over \(X\).

By extending and enriching in many ways the notions of overlap algebra and overlap morphism, the authors show that the corresponding categories are all equivalent to the category of Boolean algebras with maps preserving joins.

The paper contains a number of relevant and useful results for anyone who is interested in studying or using Boolean algebras in a constructive and predicative framework. Furthermore, it clearly shows how constructive mathematics provides a richer point of view over classical concepts – Boolean algebras in this case – where fine information and how it is preserved plays a fundamental role in the generation of the structures of interest.

Reviewer: Marco Benini (Buccinasco)