Geodesic
Proof mining and probability theory
Forum of Mathematics, Sigma, Tome 13 (2025) no. 1, p. e187

Voir la notice de l'article provenant de la source Cambridge University Press

We extend the theoretical framework of proof mining by establishing general logical metatheorems that allow for the extraction of the computational content of theorems with prima facie “noncomputational” proofs from probability theory, thereby unlocking a major branch of mathematics as a new area of application for these methods. Concretely, we first devise proof-theoretically tame logical systems that allow for the formalization of proofs involving algebras of sets together with probability contents, that is probability measures which are only assumed to be finitely additive. Based on these systems, we provide extensions for the tame treatment of Lebesgue integrals on probability contents as well as $\sigma $-algebras and associated probability measures, all via intensional approaches. All these systems are then shown to be amenable to proof-theoretic metatheorems in the style of proof mining which guarantee the extractability of effective and tame bounds from large classes of ineffective existence proofs in probability theory. Moreover, these extractable bounds are guaranteed to be highly uniform in the sense that they will be independent of all parameters relating to the underlying probability space, particularly regarding events or measures of them. As such, these results in particular provide the first logical explanation for the success and the observed uniformities of the previous ad hoc case studies of proof mining in these areas and further illustrate their extent. Lastly, we establish a general proof-theoretic transfer principle that allows for the lift of quantitative information on a relationship between different modes of convergence for sequences of real numbers to sequences of random variables. 
Neri, Morenikeji; Pischke, Nicholas. Proof mining and probability theory. Forum of Mathematics, Sigma, Tome 13 (2025) no. 1, p. e187. doi: 10.1017/fms.2025.10138
@article{10_1017_fms_2025_10138,
     author = {Neri, Morenikeji and Pischke, Nicholas},
     title = {Proof mining and probability theory},
     journal = {Forum of Mathematics, Sigma},
     pages = {e187},
     year = {2025},
     volume = {13},
     number = {1},
     doi = {10.1017/fms.2025.10138},
     url = {http://geodesic.mathdoc.fr/articles/10.1017/fms.2025.10138/}
}
TY  - JOUR
AU  - Neri, Morenikeji
AU  - Pischke, Nicholas
TI  - Proof mining and probability theory
JO  - Forum of Mathematics, Sigma
PY  - 2025
SP  - e187
VL  - 13
IS  - 1
UR  - http://geodesic.mathdoc.fr/articles/10.1017/fms.2025.10138/
DO  - 10.1017/fms.2025.10138
ID  - 10_1017_fms_2025_10138
ER  - 
%0 Journal Article
%A Neri, Morenikeji
%A Pischke, Nicholas
%T Proof mining and probability theory
%J Forum of Mathematics, Sigma
%D 2025
%P e187
%V 13
%N 1
%U http://geodesic.mathdoc.fr/articles/10.1017/fms.2025.10138/
%R 10.1017/fms.2025.10138
%F 10_1017_fms_2025_10138

[1] Arthan, R. and Oliva, P., ‘On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem’, J. Log. Anal. 13(6) (2021), 1–23. Google Scholar | DOI

[2] Avigad, J., Dean, E., and Rute, J., ‘A metastable dominated convergence theorem’, J. Log. Anal. 4(3) (2012), 1–19.10.4115/jla.2012.4.3 Google Scholar | DOI

[3] Avigad, J., Gerhardy, P., and Towsner, H., ‘Local stability of ergodic averages’, Trans. Amer. Math. Soc. 362(1) (2010), 261–288.10.1090/S0002-9947-09-04814-4 Google Scholar | DOI

[4] Avigad, J. and Iovino, J., ‘Ultraproducts and metastability’, New York J. Math. 19 (2013), 713–727. Google Scholar

[5] Bezem, M., ‘Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals’, J. Symb. Log. 50 (1985), 652–660. Google Scholar | DOI

[6] Bhaskara Rao, K.P.S. and Bhaskara Rao, M., ‘Theory of charges’, in Pure and Applied Mathematics. vol. 109 (Academic Press, London, 1983). Google Scholar

[7] Daniell, P.J., ‘A general form of integral’, Ann. Math. 19(4) (1918), 279–294.10.2307/1967495 Google Scholar | DOI

[8] Dueñez, E. and Iovino, J., ‘Model theory and metric convergence I: Metastability and dominated convergence’, in Iovino, J., editor, Beyond First Order Model Theory, vol. 1 (Chapman and Hall/CRC, New York, 2017), 131–187. Google Scholar | DOI

[9] Egoroff, D., ‘Sur les suites des fonctions mesurables’, Comptes rendus hebdomadaires des séances de l’Académie des sciences, 152 (1911), 244–246. Google Scholar

[10] Ferreira, F., Leuştean, L., and Pinto, P., ‘On the removal of weak compactness arguments in proof mining’, Adv. Math. 354 (2019), 106728. Google Scholar | DOI

[11] Ferreira, F. and Oliva, P., ‘Bounded functional interpretation’, Ann. Pure Appl. Logic 135 (2005), 73–112.10.1016/j.apal.2004.11.001 Google Scholar | DOI

[12] Gerhardy, P. and Kohlenbach, U., ‘General logical metatheorems for functional analysis’, Trans. Amer. Math. Soc. 360 (2008), 2615–2660.10.1090/S0002-9947-07-04429-7 Google Scholar | DOI

[13] Gödel, K., ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’, Dialectica 12 (1958), 280–287. Google Scholar | DOI

[14] Goldbring, I. and Towsner, H., ‘An approximate logic for measures’, Israel J. Math. 199(2) (2014), 867–913.10.1007/s11856-013-0054-3 Google Scholar | DOI

[15] Grzegorczyk, A., ‘Some classes of recursive functions’, in Rozprawny Matematyczne, (Instytut Matematyczny Polskiej Akademi Nauk, Warsaw, 1953). Google Scholar

[16] Günzel, D. and Kohlenbach, U., ‘Logical metatheorems for abstract spaces axiomatized in positive bounded logic’, Adv. Math. 290 (2016), 503–551. Google Scholar | DOI

[17] Halmos, P.R., Measure Theory, Graduate Texts in Mathematics (Springer, New York, NY, 1974). Google Scholar

[18] Hilbert, D., ‘Über das Unendliche’, Math. Ann. 95(1) (1926), 161–190. Google Scholar | DOI

[19] Howard, W.A., ‘Hereditarily majorizable functionals of finite type’, in Troelstra, A.S., editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis vol. 344 of Lecture Notes in Mathematics (Springer, New York, 1973), 454–461. Google Scholar

[20] Kohlenbach, U.. Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Eindeutigkeitsbeweisen. PhD thesis, (Goethe-Universität Frankfurt am Main, 1990). Google Scholar

[21] Kohlenbach, U., ‘Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization’, J. Symb. Log. 57(1992), 1239–1273.10.2307/2275367 Google Scholar | DOI

[22] Kohlenbach, U., ‘Pointwise hereditary majorization and some applications’, Arch. Math. Log. 31 (1992), 227–241.10.1007/BF01794980 Google Scholar | DOI

[23] Kohlenbach, U., ‘Analysing proofs in analysis’, in Hodges, W., Hyland, M., Steinhorn, C., and Truss, J., editors, Logic: From Foundations to Applications. European Logic Colloquium (Keele, 1993) (Oxford University Press, Oxford, 1996), 225–260. Google Scholar | DOI

[24] Kohlenbach, U., ‘Mathematically strong subystems of analysis with low rate of growth of provably recursive functionals’, Arch. Math. Log. 36 (1996), 31–71. Google Scholar | DOI

[25] Kohlenbach, U., ‘Some logical metatheorems with applications in functional analysis’, Trans. Amer. Math. Soc. 357(1) (2005), 89–128. Google Scholar | DOI

[26] Kohlenbach, U., ‘Applied Proof Theory: Proof Interpretations and their Use in Mathematics’, Springer Monographs in Mathematics (Springer-Verlag, Berlin Heidelberg, 2008). Google Scholar

[27] Kohlenbach, U., ‘Recent progress in proof mining in nonlinear analysis’, IFCoLog J. Log. App. 10(4) (2017), 3361–3410. Google Scholar

[28] Kohlenbach, U., ‘Proof-theoretic Methods in Nonlinear Analysis’, in Sirakov, B., Ney De Souza, P., and Viana, M., editors, Proc. ICM 2018, vol. 2 (World Scientific, Singapore, 2019), 61–82. Google Scholar

[29] Kohlenbach, U., ‘Local formalizations in nonlinear analysis and related areas and proof-theoretic tameness’, in Weingartner, P. and Leeb, H.-P., editors, Kreisel’s Interests. On the Foundations of Logic and Mathematics, vol. 41 of Tributes (College Publications, 2020), 45–61. Google Scholar

[30] Kohlenbach, U. and Nicolae, A., ‘A proof-theoretic bound extraction theorem for CAT()-spaces’, Stud. Log. 105 (2017), 611–624.10.1007/s11225-016-9702-z Google Scholar | DOI

[31] Kohlenbach, U. and Oliva, P., ‘Proof Mining: A systematic way of analysing proofs in mathematics’, Proceedings of the Steklov Institute of Mathematics 242 (2003), 136–164. Google Scholar

[32] Kolmogorov, A.N., ‘Sur la loi forte des grands nombres’, Comptes rendus de l’Académie des Sciences 191 (1930), 910–912. Google Scholar

[33] Kreisel, G., ‘On the interpretation of non-finitist proofs—Part I’, J. Symb. Log. 16(4) (1951), 241–267. Google Scholar

[34] Kreisel, G., ‘On the interpretation of non-finitist proofs–Part II. Interpretation of number theory. Applications’, J. Symb. Log. 17(1) (1952), 43–58.10.2307/2267457 Google Scholar | DOI

[35] Kreuzer, A., ‘Measure theory and higher order arithmetic’, Proc. Amer. Math. Soc., 143(12), (2015), 5411–5425. Google Scholar | DOI

[36] Kuroda, S., ‘Intuitionistische Untersuchungen der formalistischen Logik’, Nagoya Math. J. 2 (1951), 35–47.10.1017/S0027763000010023 Google Scholar | DOI

[37] Leuştean, L., ‘Proof mining in -trees and hyperbolic spaces’, Electronic Notes in Theoretical Computer Science 165 (2006), 95–106. Google Scholar | DOI

[38] Leuştean, L., ‘An application of proof mining to nonlinear iterations’, Ann. Pure App. Logic 165(9) (2014), 1484–1500.10.1016/j.apal.2014.04.015 Google Scholar | DOI

[39] Luzia, N., ‘A simple proof of the strong law of large numbers with rates’, Bull. Austral. Math. Soc. 97(3) (2018), 513–517. Google Scholar | DOI

[40] Macintyre, A., ‘The mathematical significance of proof theory’, Phil. Trans. Royal Soc. 363 (2005), 2419–2435. Google Scholar PubMed

[41] Macintyre, A., ‘The impact of Gödel’s incompleteness theorems on mathematics’, in Baaz, M., Papadimitriou, C.H., Putnam, H.W., Scott, D.S., and Harper, C.L.Jr., editors, Kurt Gödel and the foundations of mathematics: Horizons of truth, (Cambridge University Press, Cambridge, 2011), 3–25. Google Scholar | DOI

[42] Neri, M., ‘Quantitative strong laws of large numbers’, Electronic Journal of Probability 30(20) (2024), 1–22. Google Scholar

[43] Neri, M., ‘A finitary Kronecker’s lemma and large deviations in the strong law of large numbers’, Ann. Pure Appl. Logic 176(6) (2025), 103569, 1–31.10.1016/j.apal.2025.103569 Google Scholar | DOI

[44] Neri, M., Pischke, N., and Powell, T., ‘On the asymptotic behaviour of stochastic processes, with applications to supermartingale convergence, Dvoretzky’s approximation theorem, and stochastic quasi-Fejér monotonicity’, ArXiv e-prints, 2024. arXiv, math.OC, 2504.12922 Google Scholar

[45] Neri, M., Pischke, N., and Powell, T., ‘Generalized learnability of stochastic principles’, in Beckmann, A., Oitavem, I., and Manea, F., editors, Proceedings of the 21st Conference on Computability in Europe, vol. 15764 of LNCS (2025), 333–348. Google Scholar

[46] Neri, M. and Powell, T., ‘A quantitative Robbins-Siegmund theorem’, Annals of Applied Probability, 2025. to appear. Google Scholar

[47] Neri, M. and Powell, T., ‘On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales’, Transactions of the American Mathematical Society, Series B, 12 (2025), 974–1019.10.1090/btran/229 Google Scholar | DOI

[48] Oliva, P., Personal communication, November 2023. Google Scholar

[49] Paunescu, L. and Sipoş, A., ‘A proof-theoretic metatheorem for tracial von Neumann algebras’, Math. Log. Q. 69(1) (2023), 63–76.10.1002/malq.202200048 Google Scholar | DOI

[50] Pischke, N., ‘Logical Metatheorems for Accretive and (Generalized) Monotone Set-Valued Operators’, J. Math. Logic 24(2) (2024), 2350008, 1–59.10.1142/S0219061323500083 Google Scholar | DOI

[51] Pischke, N., ‘Proof Mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions’, Trans. Amer. Math. Soc. 377(10) (2024), 7475–7517. Google Scholar

[52] Pischke, N., ‘A proof-theoretic metatheorem for nonlinear semigroups generated by an accretive operator and applications’, Sel. Math. 31(2) (2025), 32, 1–67.10.1007/s00029-025-01027-8 Google Scholar | DOI

[53] Pischke, N. and Powell, T., ‘Asymptotic regularity of a generalised stochastic Halpern scheme’, ArXiv e-prints, 2024. arXiv, math.OC, 2411.04845. Google Scholar

[54] Schönfinkel, M., ‘Über die Bausteine der mathematischen Logik’, Math. Ann. 92 (1924), 305–316.10.1007/BF01448013 Google Scholar | DOI

[55] Siegmund, D., ‘Large deviation probabilities in the strong law of large numbers’, Zeitschrift für Wahrscheinlichkeitstheorie und verwandte Gebiete 31(2) (1975), 107–113.10.1007/BF00539435 Google Scholar | DOI

[56] Sipoş, A., ‘Proof mining in spaces’, J. Symb. Logic 84(4) (2019), 1612–1629.10.1017/jsl.2019.55 Google Scholar | DOI

[57] Specker, E., ‘Nicht konstruktiv beweisbare Sätze der Analysis’, J. Symb. Logic 14(3) (1949), 145–158. Google Scholar | DOI

[58] Spector, C., ‘Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics’, in Dekker, J.C.E., editor, Recursive Function Theory, Proceedings of Symposia in Pure Mathematics, vol. 5 (AMS, Providence, 1962), 1–27.10.1090/pspum/005/0154801 Google Scholar | DOI

[59] Tao, T., ‘Norm convergence of multiple ergodic averages for commuting transformations’ Ergod. Theory Dyn. Syst. 28 (2008), 657–688.10.1017/S0143385708000011 Google Scholar | DOI

[60] Troelstra, A.S., editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, vol. 344 of Lecture Notes in Mathematics (Springer, Berlin, 1973). Google Scholar | DOI

[61] Troelstra, A.S. and Van Dalen, D., editors. ‘Constructivism in Mathematics, vol. 1’, vol. 121 of Studies in Logic and the Foundations of Mathematics (North-Holland, Amsterdam, 1988). Google Scholar

Cité par Sources :