Proof mining in practice

Summary

Abstract. In this paper, we present some aspects of a recent application of proof mining by J. Avigad, H. Towsner and the author. In this case study, we analysed a proof of the Mean Ergodic Theorem and obtained a computable rate of convergence for the ergodic averages. Proof mining generally falls into two main categories: Establishing general metatheorems that classify theorems and proofs from which additional information may be extracted and carrying out case studies. The aim of presenting aspects of a proof analysis in detail in this paper is to illustrate how the general logical results and the techniques they rely on translate into a proof analysis in practice.

Introduction. ‘Proof mining’ is the subfield of mathematical logic concerned with extracting additional information from proofs in mathematics and computer sciences. This activity has its roots in Kreisel's so-called ‘unwinding’ program and is motivated by the following quote by G. Kreisel:

“What more do we know if we have proved a theorem by restricted means than if we merely know the theorem is true.”

Kreisel proposed to use techniques developed in proof theory (e.g. to settle questions of consistency) to analyse proofs and unwind the extra information hidden in them. This additional information can both be of qualitative nature, such as computable realizers and bounds, as well as of quantitative nature, such as uniformities or weakenings of premises.