### В Мокуме рекомендуют

FIVE STAGES OF ACCEPTING CONSTRUCTIVE MATHEMATICS, ANDREJ BAUER

The passage from spaces to locales has at least two additional benefits [23]: the Banach–Tarski “paradoxical” decomposition of the unit ball [2] does not work with locales even though we keep the axiom of choice, and the naive definition of random reals does. Let us briefly explain the latter one. An appealing intuitive definition of a random real x∈[0,1] is that it has no special properties, i.e., that it avoids every null set. This will not do, of course, since a singleton is a null set, and so no particular real can be random. Thus, if we attempt to define the space of random reals as the intersection of all full subsets of [0,1], we are left with an empty space. However, the intersection of all

The passage from spaces to locales has at least two additional benefits [23]: the Banach–Tarski “paradoxical” decomposition of the unit ball [2] does not work with locales even though we keep the axiom of choice, and the naive definition of random reals does. Let us briefly explain the latter one. An appealing intuitive definition of a random real x∈[0,1] is that it has no special properties, i.e., that it avoids every null set. This will not do, of course, since a singleton is a null set, and so no particular real can be random. Thus, if we attempt to define the space of random reals as the intersection of all full subsets of [0,1], we are left with an empty space. However, the intersection of all

*sublocales*of [0,1] with full measure is a nontrivial sublocale of [0,1] whose measure is still full. This is the locale of random sequences. It is nonspatial, has no points, it disrupts the traditional notion of space, and it captures our intuitive ideas about randomness in a way that usual spaces cannot.