We investigate the strength of a randomness notion $mathcal R$ as a set-existence principle in second-order arithmetic: for each $Z$ there is an $X$ that is $mathcal R$-random relative to $Z$. We show that the equivalence between $2$-randomness and being infinitely often $C$-incompressible is provable in $mathsf{RCA}_0$. We verify that $mathsf{RCA}_0$ proves the basic implications among randomness notions: $2$-random $Rightarrow$ weakly $2$-random $Rightarrow$ Martin-L{o}f random $Rightarrow$ computably random $Rightarrow$ Schnorr random. Also, over $mathsf{RCA}_0$ the existence of computable randoms is equivalent to the existence of Schnorr randoms. We show that the existence of balanced randoms is equivalent to the existence of Martin-L{o}f randoms, and we describe a sense in which this result is nearly optimal.
Download