概率理论中证明分析的系统方法
A systematic way of analysing proofs in probability theory
AI总结：
本文提出一种系统方法，通过形式化外测度定义翻译，提取概率存在性陈述的可计算界，并首次证明了高阶均匀有界性原理的证明论处理。
摘要：
在扩展的有限类型算术系统中，我们利用外测度的形式表示来定义一种翻译，从而系统地形式化概率陈述。主要结果是这种翻译产生了类似于证明挖掘的新型概率逻辑元定理，保证了从非有效证明中提取可计算界。我们进一步展示了如何利用Kohlenbach提出的集合论上不成立的均匀有界性原理，在不影响结果界计算复杂性的情况下，复制概率测度的逻辑强连续性性质。这特别提供了在界提取定理中消除σ-可加性原理的正式视角，此前仅在证明挖掘实践中零散观察到。在此背景下，我们首次通过Kohlenbach的单调变体的哥德尔功能解释，对高阶均匀有界性原理及相关反集合原理进行了证明论处理，具有独立价值。所有这些新元定理提供了系统证明论方法，用于提取文献中各种概率定理的量化信息，证明了最近对概率理论和随机优化的应用。本文是将证明挖掘方法应用于概率理论的最新进展中的重要逻辑贡献，显著扩展了第一和第三作者[Forum Math. Sigma, 13, e187 (2025)]之前的工作。
英文摘要：
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 $σ$-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ödel'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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
