pith. machine review for the scientific record.
sign in

arxiv: 2604.08078 · v1 · submitted 2026-04-09 · 🧮 math.LO

A systematic way of analysing proofs in probability theory

Morenikeji Neri , Paulo Oliva , Nicholas Pischke This is my paper

Pith reviewed 2026-05-10 18:27 UTC · model grok-4.3

classification 🧮 math.LO
keywords proof miningprobability theorylogical metatheoremsuniform boundednessfinite type arithmeticfunctional interpretationouter measurestochastic optimization
0
0 comments X

The pith

A formal translation of probabilistic statements into arithmetic yields computable bounds from non-effective proofs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a systematic method for analyzing proofs in probability theory by defining a translation of probabilistic statements into systems of finite type arithmetic, based on a formal representation of the outer measure. This translation supports new logical metatheorems that guarantee the extraction of computable bounds from proofs of probabilistic existence statements, even when the original proofs are non-effective. The authors further incorporate a uniform boundedness principle to handle continuity properties of measures in a computationally controlled way. The resulting bounds remain valid over finitely additive probability spaces, providing a formal justification for practices that eliminate reliance on full σ-additivity during quantitative analysis.

Core claim

By translating probabilistic statements via the outer measure in extended finite type arithmetic, the authors obtain metatheorems ensuring computable bound extraction from non-effective proofs of probabilistic existence claims. Kohlenbach's uniform boundedness principle is used to replicate continuity properties of probability measures without raising the complexity of the bounds, while ensuring the bounds hold even in finitely additive settings. This yields a proof-theoretic treatment of higher-type uniform boundedness and contra-collection principles via monotone functional interpretation, and formalizes the elimination of σ-additivity in bound extraction.

What carries the argument

The translation of probabilistic statements into arithmetic using a formal outer measure, which enables bound extraction through monotone functional interpretation while incorporating uniform boundedness principles.

If this is right

  • Computable bounds become extractable from non-effective proofs of probabilistic existence statements.
  • Extracted bounds remain valid when probability spaces satisfy only finite additivity rather than σ-additivity.
  • Higher-type uniform boundedness principles admit a proof-theoretic treatment via monotone functional interpretation.
  • A systematic method is provided for obtaining quantitative information from proofs of theorems in probability and stochastic optimization.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach may allow extraction of explicit rates of convergence in results from stochastic optimization.
  • It opens the possibility of applying similar translations to other areas of analysis involving measures.
  • Automated tools for bound extraction could be developed by implementing the translation in proof assistants.

Load-bearing premise

The uniform boundedness principle can replicate the continuity properties of probability measures without changing the computational complexity of the extracted bounds and while remaining valid over finitely additive spaces.

What would settle it

Identification of a specific probabilistic existence statement whose extracted bound via the translation fails to be computable or fails to hold when only finite additivity is assumed.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript develops a translation of probabilistic statements into systems of finite type arithmetic via a formal representation of the outer measure. This translation yields new logical metatheorems guaranteeing the extraction of computable bounds from non-effective proofs of probabilistic existence statements. The paper further shows that Kohlenbach's (set-theoretically false) principle of uniform boundedness can be incorporated to recover continuity properties of probability measures without raising the computational complexity of the extracted bounds, while ensuring the bounds remain valid over finitely additive spaces. It also supplies a proof-theoretic treatment of higher-type uniform boundedness and contra-collection principles under the monotone functional interpretation.

Significance. If the metatheorems and the claimed preservation of bound complexity hold, the work supplies a systematic, general framework for proof mining in probability theory that justifies and extends recent ad-hoc applications to stochastic optimization. The formal elimination of σ-additivity via tame use of uniform boundedness and the independent analysis of higher-type UB principles via monotone FI are notable strengths. The manuscript credits its extension of the authors' prior Forum Math. Sigma paper and provides a logical foundation for quantitative results in the area.

major comments (2)
  1. [§4] §4 (treatment of UB in the monotone interpretation): the claim that the outer-measure translation permits application of monotone FI to higher-type uniform boundedness and contra-collection without raising majorant degree or introducing new functional dependencies requires an explicit verification that the translation commutes with the majorization relation. The manuscript implicitly assumes this commutation preserves the type level of extracted terms relative to prior ad-hoc cases, but no concrete argument or example is supplied to confirm that additional quantifier alternations from the probabilistic encoding are neutralized.
  2. [Main metatheorem] Main metatheorem (bound-extraction theorem via the translation): the central guarantee of computable bounds from probabilistic existence statements rests on the translation allowing the principles to be treated 'in a tame way.' A load-bearing gap is the absence of a detailed check that the extracted bounds remain computationally unchanged when the translation is applied to statements involving continuity properties of measures; without this, the assertion that validity over finitely additive spaces is achieved without complexity cost cannot be assessed.
minor comments (2)
  1. [Abstract] Abstract: the phrase 'extended systems of finite type arithmetic' is used without a brief pointer to the precise base theory (e.g., a variant of E-PA^ω or PA^ω with additional constants); adding this would improve readability for readers outside proof mining.
  2. [Introduction] Notation: the outer-measure encoding and the precise definition of the probabilistic translation are introduced without an early summary table or diagram contrasting it with the direct formalization used in the authors' prior work; this would help readers track the differences.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. The comments highlight areas where the manuscript would benefit from greater explicitness, and we plan to incorporate revisions to address them directly while preserving the core contributions.

read point-by-point responses

  1. Referee: [§4] §4 (treatment of UB in the monotone interpretation): the claim that the outer-measure translation permits application of monotone FI to higher-type uniform boundedness and contra-collection without raising majorant degree or introducing new functional dependencies requires an explicit verification that the translation commutes with the majorization relation. The manuscript implicitly assumes this commutation preserves the type level of extracted terms relative to prior ad-hoc cases, but no concrete argument or example is supplied to confirm that additional quantifier alternations from the probabilistic encoding are neutralized.

    Authors: We agree that an explicit verification is needed to confirm that the outer-measure translation commutes with the majorization relation without increasing majorant degree or introducing new dependencies. In the revised version we will insert a dedicated lemma in §4 establishing this commutation by induction on the structure of the translated formulas. The lemma will show that the probabilistic encoding, being monotone and quantifier-alternation preserving at the relevant type levels, does not alter the majorization relation. A short illustrative example involving a uniform boundedness statement for a simple probabilistic predicate will be added to demonstrate that the extracted terms retain the same type and majorant complexity as in the ad-hoc cases treated previously. revision: yes

  2. Referee: [Main metatheorem] Main metatheorem (bound-extraction theorem via the translation): the central guarantee of computable bounds from probabilistic existence statements rests on the translation allowing the principles to be treated 'in a tame way.' A load-bearing gap is the absence of a detailed check that the extracted bounds remain computationally unchanged when the translation is applied to statements involving continuity properties of measures; without this, the assertion that validity over finitely additive spaces is achieved without complexity cost cannot be assessed.

    Authors: We accept that a more detailed verification is required to substantiate that the extracted bounds remain computationally unchanged under the translation when continuity properties of measures are involved. The revised manuscript will contain an expanded subsection attached to the main metatheorem that supplies this check. It will include a proposition verifying that the translated uniform boundedness principle, when combined with the outer-measure representation, yields bounds of identical majorant degree to the untranslated case. The argument proceeds by showing that the additional continuity axioms are realized by the same majorizing functionals already present in the monotone interpretation, thereby confirming that validity over finitely additive spaces incurs no extra computational cost. A proof sketch and a reference to the relevant clauses of the translation definition will be provided. revision: yes

Circularity Check

0 steps flagged

New outer-measure translation and monotone interpretation of UB principles yield independent metatheorems

full rationale

The paper constructs a fresh translation of probabilistic statements into statements over finite-type arithmetic via an outer-measure representation, then applies Kohlenbach's monotone functional interpretation to obtain bound-extraction metatheorems; the treatment of higher-type uniform boundedness and contra-collection axioms is presented as a first-time proof-theoretic analysis whose validity over finitely additive spaces follows directly from the translation's design rather than from any prior result by the same authors. The cited earlier paper supplies background context on ad-hoc observations but is not invoked to justify the new translation or the complexity-preservation claim. No equation or definition in the abstract reduces a claimed prediction or metatheorem to a fitted parameter or to the input data by construction, and the derivation chain remains self-contained against external benchmarks such as the monotone interpretation itself.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claims rest on a newly defined translation and the controlled use of a classically false principle inside a formal arithmetic system; these are not free parameters but constitute the novel technical content.

axioms (2)
  • standard math Extended systems of finite type arithmetic
    Base system in which the outer-measure representation and translation are defined.
  • ad hoc to paper Kohlenbach's principle of uniform boundedness
    Invoked to obtain continuity properties while keeping bounds tame; explicitly noted as set-theoretically false.
invented entities (1)
  • Formal translation via outer measure no independent evidence
    purpose: To convert probabilistic statements into logical ones amenable to bound extraction
    Newly defined device that enables the metatheorems; no independent evidence outside the paper is supplied.

pith-pipeline@v0.9.0 · 5599 in / 1395 out tokens · 144787 ms · 2026-05-10T18:27:04.536579+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

62 extracted references · 62 canonical work pages · 1 internal anchor

  1. [1]

    Arthan and P

    R. Arthan and P. Oliva. On the Borel–Cantelli Lemmas, the Erd˝ os–R´ enyi Theorem, and the Kochen–Stone Theorem.Journal of Logic and Analysis, 13(6):1–23, 2021

    work page 2021

  2. [2]

    Avigad, E

    J. Avigad, E. Dean, and J. Rute. A metastable dominated convergence theorem.Journal of Logic and Analysis, 4(3), 2012. 19pp

    work page 2012

  3. [3]

    Dialectica

    J. Avigad and S. Feferman. G¨ odel’s functional (“Dialectica”) interpretation. In S.R. Buss, editor,Handbook of Proof Theory, volume 137 ofStudies in Logic and the Foundations of Mathematics, pages 337–405. Elsevier, Amsterdam, 1998

    work page 1998

  4. [4]

    Avigad, P

    J. Avigad, P. Gerhardy, and H. Towsner. Local stability of ergodic averages.Transactions of the American Mathematical Society, 362(1):261–288, 2010

    work page 2010

  5. [5]

    Avigad and J

    J. Avigad and J. Iovino. Ultraproducts and metastability.New York Journal of Mathematics, 19:713–727, 2013

    work page 2013

  6. [6]

    Avigad and J

    J. Avigad and J. Rute. Oscillation and the mean ergodic theorem for uniformly convex Banach spaces. Ergodic Theory and Dynamical Systems, 35(4):1009–1027, 2015

    work page 2015

  7. [7]

    M. Bezem. Strongly majorizable functionals of finite type: a model for bar recursion containing discontin- uous functionals.The Journal of Symbolic Logic, 50:652–660, 1985

    work page 1985

  8. [8]

    Due˜ nez and J

    E. Due˜ nez and J. Iovino. Model theory and metric convergence I: Metastability and dominated convergence. In J. Iovino, editor,Beyond first order model theory, volume 1, pages 131–187. Chapman and Hall/CRC, New York, 2017

    work page 2017

  9. [9]

    D.Th. Egoroff. Sur les suites des fonctions mesurables.Comptes rendus hebdomadaires des s´ eances de l’Acad´ emie des sciences, 152:244–246, 1911

    work page 1911

  10. [10]

    Engr´ acia and F

    P. Engr´ acia and F. Ferreira. Bounded functional interpretation with an abstract type. In A. Rezus, editor, Contemporary Logic and Computing, volume 1 ofLandscapes in Logic, pages 87–112. College Publications, London, 2020. A SYSTEMATIC WAY OF ANALYSING PROOFS IN PROBABILITY THEORY 49

    work page 2020

  11. [11]

    Ferreira

    F. Ferreira. Injecting uniformities into Peano Arithmetic.Annals of Pure and Applied Logic, 157(2–3):122– 129, 2009

    work page 2009

  12. [12]

    Ferreira and P

    F. Ferreira and P. Oliva. Bounded functional interpretation.Annals of Pure and Applied Logic, 135:73–112, 2005

    work page 2005

  13. [13]

    Gerhardy and U

    P. Gerhardy and U. Kohlenbach. Strongly uniform bounds from semi-constructive proofs.Annals of Pure and Applied Logic, 141:89–107, 2006

    work page 2006

  14. [14]

    Gerhardy and U

    P. Gerhardy and U. Kohlenbach. General logical metatheorems for functional analysis.Transactions of the American Mathematical Society, 360:2615–2660, 2008

    work page 2008

  15. [15]

    G¨ odel.¨Uber eine bisher noch nicht ben¨ utzte Erweiterung des finiten Standpunktes.Dialectica, 12:280– 287, 1958

    K. G¨ odel.¨Uber eine bisher noch nicht ben¨ utzte Erweiterung des finiten Standpunktes.Dialectica, 12:280– 287, 1958

    work page 1958

  16. [16]

    Grzegorczyk, editor.Some classes of recursive functions, volume IV ofRozprawny Matematyczne

    A. Grzegorczyk, editor.Some classes of recursive functions, volume IV ofRozprawny Matematyczne. In- stytut Matematyczny Polskiej Akademi Nauk, Warsaw, 1953

    work page 1953

  17. [17]

    G¨ unzel and U

    D. G¨ unzel and U. Kohlenbach. Logical metatheorems for abstract spaces axiomatized in positive bounded logic.Advances in Mathematics, 290:503–551, 2016

    work page 2016

  18. [18]

    Halmos.Measure Theory, volume 18 ofGraduate Texts in Mathematics

    P.R. Halmos.Measure Theory, volume 18 ofGraduate Texts in Mathematics. Springer New York, NY, 1950

    work page 1950

  19. [19]

    D. Hilbert. ¨Uber das Unendliche.Mathematische Annalen, 95(1):161–190, 1926

    work page 1926

  20. [20]

    W.A. Howard. Hereditarily majorizable functionals of finite type. In A.S. Troelstra, editor,Metamathemat- ical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 ofLecture Notes in Mathematics, pages 454–461. Springer, New York, 1973

    work page 1973

  21. [21]

    H.J. Keisler. Probability Quantifiers. In J. Barwise and S. Feferman, editors,Model-Theoretic Logics, Perspectives in Mathematical Logic, pages 509–556. Springer Berlin, Heidelberg, 1985

    work page 1985

  22. [22]

    H.J. Keisler. Measures and forking.Annals of Pure and Applied Logic, 34(2):119–169, 1987

    work page 1987

  23. [23]

    Klenke.Probability Theory: A Comprehensive Course

    A. Klenke.Probability Theory: A Comprehensive Course. Universitext. Springer London, 2008

    work page 2008

  24. [24]

    Kohlenbach

    U. Kohlenbach. Effective bounds from ineffective proofs in analysis: an application of functional interpre- tation and majorization.The Journal of Symbolic Logic, 57:1239–1273, 1992

    work page 1992

  25. [25]

    Kohlenbach

    U. Kohlenbach. Analysing proofs in analysis. In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: From Foundations to Applications. European Logic Colloquium (Keele, 1993), pages 225–260. Oxford University Press, Oxford, 1996

    work page 1993

  26. [26]

    Kohlenbach

    U. Kohlenbach. Mathematically strong subystems of analysis with low rate of growth of provably recursive functionals.Archive for Mathematical Logic, 36:31–71, 1996

    work page 1996

  27. [27]

    Kohlenbach

    U. Kohlenbach. Relative constructivity.The Journal of Symbolic Logic, 63:1218–1238, 1998

    work page 1998

  28. [28]

    Kohlenbach

    U. Kohlenbach. The use of a logical principle of uniform boundedness in analysis. In A. Cantini, E. Casari, and P. Minari, editors,Logic and Foundations of Mathematics, volume 280 ofSynthese Library, pages 93–106. Kluwer Academic, Dordrecht, 1999

    work page 1999

  29. [29]

    Kohlenbach

    U. Kohlenbach. Some logical metatheorems with applications in functional analysis.Transactions of the American Mathematical Society, 357(1):89–128, 2005

    work page 2005

  30. [30]

    Kohlenbach

    U. Kohlenbach. A logical uniform boundedness principle for abstract metric and hyperbolic spaces.Elec- tronic Notes in Theoretical Computer Science, 165:81–93, 2006

    work page 2006

  31. [31]

    Kohlenbach.Applied Proof Theory: Proof Interpretations and their Use in Mathematics

    U. Kohlenbach.Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Mono- graphs in Mathematics. Springer Berlin, Heidelberg, 2008

    work page 2008

  32. [32]

    Kohlenbach

    U. Kohlenbach. A note on the monotone functional interpretation.Mathematical Logic Quarterly, 57(6):611–614, 2011

    work page 2011

  33. [33]

    Kohlenbach

    U. Kohlenbach. Proof-theoretic Methods in Nonlinear Analysis. In B. Sirakov, P. Ney de Souza, and M. Viana, editors,Proceedings ICM 2018, volume 2, pages 61–82. World Scientific, Singapore, 2019

    work page 2018

  34. [34]

    Kohlenbach and P

    U. Kohlenbach and P. Oliva. Proof Mining: A Systematic Way of Analysing Proofs in Mathematics. Proceedings of the Steklov Institute of Mathematics, 242:136–164, 2003

    work page 2003

  35. [35]

    Kohlenbach and P

    U. Kohlenbach and P. Safarik. Fluctuations, effective learnability and metastability in analysis.Annals of Pure and Applied Logic, 165(1):266–304, 2014

    work page 2014

  36. [36]

    G. Kreisel. On the Interpretation of Non-Finitist Proofs – Part I.The Journal of Symbolic Logic, 16(4):241– 267, 1951

    work page 1951

  37. [37]

    G. Kreisel. On the Interpretation of Non-Finitist Proofs – Part II. Interpretation of Number Theory. Applications.The Journal of Symbolic Logic, 17(1):43–58, 1952

    work page 1952

  38. [38]

    G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyt- ing, editor,Constructivity in Mathematics, Lecture Notes in Mathematics, pages 101–128. North-Holland Publishing Company, Amsterdam, 1959. 50 M. NERI, P. OLIVA, N. PISCHKE

    work page 1959

  39. [39]

    G. Kreisel. On weak completeness of intuitionistic predicate logic.The Journal of Symbolic Logic, 27:139– 158, 1962

    work page 1962

  40. [40]

    S. Kuroda. Intuitionistische Untersuchungen der formalistischen Logik.Nagoya Mathematical Journal, 2:35– 47, 1951

    work page 1951

  41. [41]

    P.A. Loeb. Conversion from nonstandard to standard measure spaces and applications in probability theory. Transactions of the American Mathematical Society, 211:113–122, 1975

    work page 1975

  42. [42]

    M. Neri. Quantitative Strong Laws of Large Numbers.Electronic Journal of Probability, 30(20), 2024. 22pp

    work page 2024

  43. [43]

    M. Neri. A finitary Kronecker’s lemma and large deviations in the strong law of large numbers.Annals of Pure and Applied Logic, 176(6), 2025. 103569, 31pp

    work page 2025

  44. [44]

    M. Neri. Oscillations in the Strong Law of Large Numbers, 2025. preprint available athttps://kejineri. github.io

    work page 2025

  45. [45]

    M. Neri. The pointwise ergodic theorem on finitely additive spaces, 2025. preprint available athttps: //arxiv.org/abs/2511.01676

    work page arXiv 2025

  46. [46]

    Neri and N

    M. Neri and N. Pischke. Proof mining and probability theory.Forum of Mathematics, Sigma, 13, 2025. e187, 47pp

    work page 2025

  47. [47]

    M. Neri, N. Pischke, and T. Powell. Generalized learnability of stochastic principles. In A. Beckmann, I. Oitavem, and F. Manea, editors,Proceedings of the 21st Conference on Computability in Europe, volume 15764 ofLecture Notes in Computer Science, pages 333–348. Springer, Berlin Heidelberg, 2025

    work page 2025

  48. [48]

    M. Neri, N. Pischke, and T. Powell. On the asymptotic behaviour of stochastic processes, with appli- cations to supermartingale convergence, Dvoretzky’s approximation theorem, and stochastic quasi-Fej´ er monotonicity, 2025. preprint available athttps://arxiv.org/abs/2504.12922

    work page internal anchor Pith review arXiv 2025

  49. [49]

    M. Neri, N. Pischke, and T. Powell. Generalized fluctuation bounds for stochastic algorithms in the presence of compactness, 2026. preprint available athttps://arxiv.org/abs/2602.22741

    work page arXiv 2026

  50. [50]

    Neri and T

    M. Neri and T. Powell. On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales.Transactions of the American Mathematical Society, Series B, 12:974–1019, 2025

    work page 2025

  51. [51]

    Neri and T

    M. Neri and T. Powell. A quantitative Robbins-Siegmund theorem.Annals of Applied Probability, 36(1):636–651, 2026

    work page 2026

  52. [52]

    N. Pischke. Mean-square and linear convergence of a stochastic proximal point algorithm in metric spaces of nonpositive curvature, 2025. preprint available athttps://arxiv.org/abs/2510.10697

    work page arXiv 2025

  53. [53]

    N. Pischke. On Busemann subgradient methods for stochastic minimization in Hadamard spaces, 2026. preprint available athttps://arxiv.org/abs/2602.08127

    work page arXiv 2026

  54. [54]

    Pischke and T

    N. Pischke and T. Powell. Asymptotic regularity of a generalised stochastic Halpern scheme, 2024. preprint available athttps://arxiv.org/abs/2411.04845

    work page arXiv 2024

  55. [55]

    Powell and A

    T. Powell and A. Wan. An approximate zero-one law via the Dialectica interpretation, 2025. preprint available athttps://arxiv.org/abs/2508.20849

    work page arXiv 2025

  56. [56]

    Bhaskara Rao and M

    K.P.S. Bhaskara Rao and M. Bhaskara Rao.Theory of Charges, volume 109 ofPure and Applied Mathe- matics. Academic Press, London, 1983

    work page 1983

  57. [57]

    Sch¨ onfinkel.¨Uber die Bausteine der mathematischen Logik.Mathematische Annalen, 92:305–316, 1924

    M. Sch¨ onfinkel.¨Uber die Bausteine der mathematischen Logik.Mathematische Annalen, 92:305–316, 1924

    work page 1924

  58. [58]

    Scott and P

    D. Scott and P. Krauss. Assigning probabilities to logical formulas. In J. Hintikka and P. Suppes, editors, Aspects of Inductive Logic, volume 43 ofStudies in Logic and the Foundations of Mathematics, pages 219–264. North-Holland, Amsterdam, 1966

    work page 1966

  59. [59]

    C. Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In J.C.E. Dekker, editor,Recursive Function Theory, volume 5 ofProceedings of Symposia in Pure Mathematics, pages 1–27. American Mathematical Society, Providence, RI, 1962

    work page 1962

  60. [60]

    T. Tao. Norm convergence of multiple ergodic averages for commuting transformations.Ergodic Theory and Dynamical Systems, 28:657–688, 2008

    work page 2008

  61. [61]

    Tao.Structure and Randomness: Pages from Year One of a Mathematical Blog, chapter Soft Analy- sis, Hard Analysis, and the Finite Convergence Principle, pages 17–29

    T. Tao.Structure and Randomness: Pages from Year One of a Mathematical Blog, chapter Soft Analy- sis, Hard Analysis, and the Finite Convergence Principle, pages 17–29. American Mathematical Society, Providence, RI, 2008

    work page 2008

  62. [62]

    Troelstra, editor.Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 ofLecture Notes in Mathematics

    A.S. Troelstra, editor.Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 ofLecture Notes in Mathematics. Springer, Berlin, 1973

    work page 1973