The Proof Mining Seminar is a joint LOS/ILDS seminar, featuring talks on recent results in proof mining.
Proof mining is a paradigm of research, concerned with the extraction of hidden finitary and combinatorial content from proofs that make use of highly infinitary principles. The new information is obtained after a logical analysis, using proof-theoretic tools, and can be both of a quantitative nature, such as algorithms and effective bounds, as well as of a qualitative nature, such as uniformities in the bounds or weakenings of the premises.
All seminars, except where otherwise indicated, will be on Wednesdays between 16:00 and 18:00, Bucharest time. The seminars are held remotely.
To receive announcements about the seminar, please send an email to proof-mining-seminar@ilds.ro.
Organizers: Ulrich Kohlenbach, Laurențiu Leuștean, Andrei Sipoș
Wednesday, July 31, 2024
Morenikeji Neri (University of Bath)
Proof mining and probability
Abstract:
Due to previous ad hoc case studies, the insight was made that a significant proportion of results in probability theory (and finite measure theory, in general) made use of infinite unions and sigma additivity in a very sparing way, allowing for a formalisation amenable to bound extraction, in the style of the classical proof mining metatheorems. This talk will discuss aspects of recently developed formal systems stemming from this perspective. While these systems entail many subtle details and features, we shall focus on those that allow us to discuss their key achievements. This includes a novel extension of Bezem’s majorizability that explains the uniformities in the extracted bounds of previous case studies and the formalisation of a strategy that transfers quantitative deterministic results to their corresponding probabilistic analogues. This is joint work with Nicholas Pischke.