Book contents
- Frontmatter
- Contents
- Introduction
- Speakers and Titles
- Decorated linear order types and the theory of concatenation
- Cardinal preserving elementary embeddings
- Proof interpretations and majorizability
- Proof mining in practice
- Cardinal structure under AD
- Three lectures on automatic structures
- Pillay's conjecture and its solution—a survey
- Proof theory and meaning: On the context of deducibility
- Bounded super real closed rings
- Analytic combinatorics of the transfinite: A unifying Tauberian perspective
- References
Proof mining in practice
Published online by Cambridge University Press: 01 March 2011
- Frontmatter
- Contents
- Introduction
- Speakers and Titles
- Decorated linear order types and the theory of concatenation
- Cardinal preserving elementary embeddings
- Proof interpretations and majorizability
- Proof mining in practice
- Cardinal structure under AD
- Three lectures on automatic structures
- Pillay's conjecture and its solution—a survey
- Proof theory and meaning: On the context of deducibility
- Bounded super real closed rings
- Analytic combinatorics of the transfinite: A unifying Tauberian perspective
- References
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.
- Type
- Chapter
- Information
- Logic Colloquium 2007 , pp. 82 - 91Publisher: Cambridge University PressPrint publication year: 2010