An 'elementary' perspective on reasoning about probability spaces

This paper is concerned with a two-sorted probabilistic language, denoted by $\textsf{QPL}$, which contains quantifiers over events and over reals, and can be viewed as an elementary language for reasoning about probability spaces. The fragment of $\textsf{QPL}$ containing only quantifiers over reals is a variant of the well-known 'polynomial' language from Fagin et al. (1990, Inform. Comput., 87, 78-128). We shall prove that the $\textsf{QPL}$-theory of the Lebesgue measure on $\left [ 0, 1 \right ]$ is decidable, and moreover, all atomless spaces have the same $\textsf{QPL}$-theory. Also, we shall introduce the notion of elementary invariant for $\textsf{QPL}$ and use it to translate the semantics for $\textsf{QPL}$ into the setting of elementary analysis. This will allow us to obtain further decidability results as well as to provide exact complexity upper bounds for a range of interesting undecidable theories.