Metric Boolean algebras and constructive measure theory (Q1407569)

The authors present two approaches to constructive measure theory: one using the metric completion of a Boolean algebra, the other using the \(\sigma\)-completion. In the former approach the measure of an event can be computed as a constructive real number. In the latter approach this value is a hyperarithmetical real. By considering metric completions of Boolean algebras -- an approach first suggested by Kolmogorov -- the authors give a simple construction of certain measures, e.g.~of the Lebesgue measure on the unit interval. The integration spaces of Bishop and Cheng turn out to give examples of such metric Boolean algebras. By proving a constructive version of Kolmogorov's 0-1 law, the authors indicate how one can obtain a substantial part of the Bishop/Cheng integration theory in an elementary and pointfree way. It should however be noted that, for instance, the concept of almost everywhere convergence can not be treated in this way since it is not a topological concept. Next, the authors analyse the notion of Borel subsets and show that the algebra of such subsets can be characterised in a pointfree and constructive way by an initiality condition. Thus the authors give a solution to the `Borel measure problem'. The measure on Borel sets is defined first using the non-constructive principle known as LPO, and only then in a constructive way. As is well known, it is impossible to constructively assign a measure to all open sets of the real line. To avoid this problem, the authors use a measure with values in the hyperarithmetical reals, as opposed to the ordinary (constructive) real numbers. These hyperarithmetical reals stem from a sheaf model construction by the same authors [Arch. Math. Logic 39, No. 1, 53--74 (2000; Zbl 0947.03078)].