Proof Mining

Origin. Kreisel asked in the 1950s, under the name unwinding, what a proof yields beyond the truth of its conclusion. Kohlenbach turned the question into a systematic program from the 1990s, based on a monotone variant of Gödel's Dialectica interpretation (1996) and collected in Applied Proof Theory (2008). The results of the subject are theorems of analysis obtained by logical means, not theorems about logic.

Models. A classical proof of a ∀∃ statement supplies no witness, but it does supply a bound. The monotone functional interpretation extracts a majorant rather than an exact witness, and majorants are insensitive to the details of the proof, which is what makes the extracted estimates uniform in parameters ranging over bounded sets.

Formalism.

Goal: Classical proof of ∀x∃y.A(x,y). Extract Φ with ∀x∃y ≤ Φ(x).A(x,y). Bound, not exact witness. Effective and uniform.

Extraction pipeline: Negative translation: classical → intuitionistic. Monotone functional interpretation of the result. Majorant Φ read off the interpreting term.

Majorizability: s* ≥_ρ s ("s* majorizes s of type ρ"). Type 0: numerical ≥. Type ρ→σ: x* ≥_ρ x implies sx ≥_σ sx. Howard's relation; Bezem's strong variant adds monotonicity.

Metatheorems (Kohlenbach): Base A^ω: arithmetic in all finite types. Extended by abstract metric, hyperbolic, normed, CAT(0) spaces. ∀ over a bounded set ∃ ⟹ effective bound. Bound depends on parameters only through majorants.

Admissible non-effective principles: Weak König's lemma. Quantifier-free choice QF-AC. Markov's principle. Contribute nothing to the extracted bound.

Metastability: No rate of convergence in general. ∀k ∀g ∃n ∀i,j ∈ [n, n+g(n)]. d(x_i, x_j) < 2^{-k}. Rate of metastability Φ(k, g) is extractable.

Applications: Fixed point theory: rates of asymptotic regularity. Krasnoselskii–Mann iterations. Ergodic theory: metastable mean ergodic theorem. Approximation theory: moduli of uniqueness.

Logical techniques: Negative translation (Gödel–Gentzen, Kuroda). Dialectica and its monotone variant. A-translation (Friedman, Dragalin). Bar recursion for the analytical fragment.

Symbols.

Symbol	Unicode	Name	Meaning
Φ	U+03A6	Phi (capital)	The extracted bound, or the rate of metastability Φ(k, g)
ρ, σ	U+03C1, U+03C3	Rho, Sigma	Finite types
ω	U+03C9	Omega	Superscript ω marks a theory formulated in all finite types
≥	U+2265	Greater than or equal	Majorization at type 0 is numerical comparison
⟹	U+27F9	Implies	Metalevel: from a proof of this shape, that bound follows
→	U+2192	Arrow / Function type	Forms the higher type ρ→σ
∈	U+2208	Element of	i, j range over the window [n, n+g(n)]
∀	U+2200	Universal quantifier	The parameter quantifier, restricted to a bounded set
∃	U+2203	Existential quantifier	The quantifier whose witness is replaced by a bound
≥_ρ	—	Majorization at type ρ	s* ≥_ρ s: s* dominates s hereditarily
A^ω	—	Arithmetic in all finite types	Base system of Kohlenbach's metatheorems
T^ω	—	Higher-type theory	A theory extended to all finite types
∀∃	—	Prenex form	The shape of a statement with quantitative content
g	—	Counterfunction	The function quantified in the metastable formulation

Metatheory. Kreisel's unwinding produced isolated results case by case; Kohlenbach's metatheorems make the extraction systematic and say in advance what a proof will yield. They state that if a proof in A^ω — arithmetic in all finite types, extended by abstract metric, hyperbolic, normed or CAT(0) spaces — establishes a ∀∃ sentence of the admitted logical form, then an effective bound is extractable, and the bound is uniform: it depends on the parameters only through majorants for them, hence is independent of everything ranging over a bounded set, including the space itself, which enters only through a bound on the relevant distances. Weak König's lemma, quantifier-free choice and Markov's principle may be used freely and contribute nothing to the bound. The payoff is theorems of analysis: rates of asymptotic regularity for Krasnoselskii–Mann iterations, and the metastable mean ergodic theorem of Avigad, Gerhardy and Towsner (2010), whose finitary reading Tao pressed independently.

Applies to. Analysis. Fixed point theory. Ergodic theory. Approximation theory.

Limitations. What is extracted is a bound, not a rate of convergence, and this is not a defect of method: Specker (1949) constructed a computable monotone bounded sequence of rationals whose limit is not computable, so no procedure can extract a convergence rate from a proof of convergence alone. The substitute is a rate of metastability, which yields no error estimate by itself. The metatheorems also constrain the input — the sentence must have the admitted logical form, and the parameters must be majorizable, which is why bounded sets recur throughout the applications. Extraction is not mechanical: the proof must be formalized, or at least surveyed closely enough to identify the principles it uses, and the resulting numerical bounds are typically far from optimal, sharpening them being separate mathematical work.