A systematic way of analysing proofs in probability theory

Abstract

Over extended systems of finite type arithmetic, we utilize a formal representation of the outer measure to define a translation which allows for the systematic formalization of probabilistic statements. As a main result, this translation gives rise to novel probabilistic logical metatheorems in the style of proof mining, guaranteeing the extractability of computable bounds from (non-effective) proofs of probabilistic existence statements. We further show how the set-theoretically false principle of uniform boundedness due to Kohlenbach can be used to replicate logically strong continuity properties of probability measures in the context of these bound extraction theorems in a tame way, i.e. without affecting the computational complexity of the resulting bounds in question, all the while guaranteeing the validity of those bounds even over finitely additive probability spaces. This in particular provides a formal perspective on the elimination of the principle of $\sigma$-additivity during bound extraction, as previously only observed ad hoc in the practice of proof mining. In that context, we for the first time provide a proof-theoretic treatment of higher-type uniform boundedness principles and related contra-collection principles via Kohlenbach's monotone variant of G\"odel's functional interpretation, which is of independent interest. All together, these new metatheorems provide a systematic proof-theoretic approach towards extracting various types of quantitative information for probabilistic theorems considered in the literature, justifying a range of recent applications to probability theory and stochastic optimization. This paper represents a major logical contribution to a recent advance of bringing the methods of proof mining to bear on probability theory, significantly extending previous work by the first and third author [Forum Math. Sigma, 13, e187 (2025)] in that direction.