The locale of random sequences
The naive approach to formalising the notion of random sequence is to define a sequence to be random if it satisfies all probabilistic laws. This does not work because there are no such sequences. Existing mathematical theories of randomness circumvent this problem by restricting to subclasses of probabilistic laws. Typically, such subclasses are defined by invoking computability considerations, or by using notions of logical definability. Such definitions have led to the rich and successful mathematical theory of algorithmically random sequences.
The purpose of this talk is to rescue the naive approach to randomness. I will show that there is a meaningful sense in which the sequences that satisfy all probabilistic laws form a natural and non-trivial "space". The tool needed to make sense of this idea is locale theory. The aim of the talk is to present sufficient background on randomness and locale theory to lead up to the eventual very natural definition of the "locale of random sequences". Finally, I'll discuss some interesting properties of this "space".