Martin-Löf tests and random sequences

A sequence $(U_n{)}_{n\ge 0}$ is uniformly effectively open when there is one computably enumerable relation $W\subseteq \mathbb{N}\times \{0,1{\}}^{\ast }$ such that $U_n={\bigcup }_{(n,\sigma )\in W}[\sigma ]$ for every $n$. Thus a single algorithm, given no oracle, enumerates all pairs $(n,\sigma )$ and thereby enumerates the cylinders at every level uniformly. This notion uses only the cylinders of Effectively open sets in Cantor space and requires no choice principle.

For open $U$ write $\mu (U):={\mu }_o(U)$, the choice-free fair-coin open content of Choice-free fair-coin content on open subsets of binary sequence space.

A Martin-Löf test is a uniformly effectively open sequence with $\mu (U_n)\le 2^{-n}$. A sequence $X\in 2^{\omega }$ is Martin-Löf random when $X\mathrm{\notin }{\bigcap }_n{U}_n$ for every such test. Computable enumerability, cylinders, and open content are as in Effectively open sets in Cantor space. Under countable choice this is the usual Borel fair-coin measure of each $U_n$; the test definition itself requires no choice principle.