?
An ‘elementary’ perspective on reasoning about probability spaces
This paper is concerned with a two-sorted probabilistic language, denoted by 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 QPL containing only quantifiers over reals is a variant of the well-known ‘polynomial’ language from [Fagin et al. 1990, Section 6]. We shall prove that the QPL-theory of the Lebesgue measure on [0, 1] is decidable, and moreover, all atomless spaces have the same QPL-theory. Also we shall introduce the notion of elementary invariant for QPL, and use it to translate the semantics for 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.