  We study the logic obtained by endowing the language of first-order
arithmetic with second-order measure quantifiers. This new kind of
quantification allows us to express that the argument formula is true in a
certain portion of all possible interpretations of the quantified variable. We
show that first-order arithmetic with measure quantifiers is capable of
formalizing simple results from probability theory and, most importantly, of
representing every recursive random function. Moreover, we introduce a
realizability interpretation of this logic in which programs have access to an
oracle from the Cantor space.
