Metric Boolean algebras and constructive measure theory

 This work concerns constructive aspects of measure theory. By considering metric completions of Boolean algebras – an approach first suggested by Kolmogorov – one can give a very simple construction of e.g. the Lebesgue measure on the unit interval. The integration spaces of Bishop and Cheng turn out to give examples of such Boolean algebras. We analyse next the notion of Borel subsets. We show that the algebra of such subsets can be characterised in a pointfree and constructive way by an initiality condition. We then use our work to define in a purely inductive way the measure of Borel subsets.

Authors and Affiliations

1. Department of Computer Science, Chalmers University of Technology and Gothenburg University, SE-412 96 Göteborg, Sweden. e-mail: coquand@cs.chalmers.se, , , , , , SE

   Thierry Coquand

2. Department of Mathematics, Uppsala University, P.O. Box 480, SE-751 06 Uppsala, Sweden. e-mail: palmgren@math.uu.se, , , , , , SE

   Erik Palmgren

Received: 9 November 2000 / Revised version: 23 March 2001 / Published online: 12 July 2002

Reprints and permissions