Kreisel's "shift of emphasis'' and contemporary proof mining

Studies in Logic, Vol. 16, No. 3 (2023): 1–35   PII: 1674­3202(2023)­03­0001­35

Ulrich Kohlenbach

Abstract.

The contemporary “proof mining” paradigm has its historical roots in Georg Kreisel’s program of “unwinding of proofs”. In this paper we elaborate on the tremendous influence Kreisel’s ideas have had and still have on this applied reorientation of proof theory and discuss some logical aspects of “proof mining”.