An 'elementary' perspective on reasoning about probability spaces.

This article investigates the two-sorted quantified probabilistic language |$\textsf{QPL}$|, which includes quantifiers over both events and real numbers, serving as an elementary framework for reasoning about probability spaces. It establishes that the |$\textsf{QPL}$|-theory of the Lebesgue measure on the unit interval |$[0,1]$| is decidable and that all atomless probability spaces share the same |$\textsf{QPL}$|-theory. The paper introduces the concept of an elementary invariant, a function encoding the atomic structure of a probability space, and proves that two spaces are elementarily equivalent if and only if their elementary invariants coincide. Furthermore, it develops a translation of |$\textsf{QPL}$| semantics into the language of elementary analysis (second-order arithmetic), enabling the derivation of decidability results for classes of spaces with finitely many atoms and complexity upper bounds for analytical classes of probability spaces. Notably, it shows that for any analytical class of spaces containing all infinite discrete spaces, the |$\textsf{QPL}$|-theory is precisely as complex as complete second-order arithmetic.