Kreisel’s “unwinding” program. (English) Zbl 0889.03045

Feferman, Solomon

Odifreddi, Piergiorgio (ed.), Kreiseliana: about and around Georg Kreisel. Wellesley, MA: A K Peters. 247-273 (1996).

The author discusses Georg Kreisel’s programme to “unwind” the constructive content of prima-facie non-constructive mathematical proofs. The author sketches the steps towards this programme presenting the early notion of an “interpretation” providing the “finite sense” of “non-finitistic” proofs, especially the no-counterexample interpretation (n.c.i.). He mentions the different proofs of the n.c.i. and various applications, e.g. to Littlewood’s theorem of 1914 and to finiteness theorems. The assessment of these applications leads to a rather ambivalent conclusion: “My overall conclusion is that while the general theory of unwinding launched by Kreisel is eminently successful, the supposed applications to date are few and far between; moreover, in some prominent cases, their status even as applications has to be put in question” (p. 248).
For the entire collection see [Zbl 0894.03002].

Reviewer: V.Peckhaus (Erlangen)

MSC:

03F03	Proof theory in general (including proof-theoretic semantics)
03F65	Other constructive mathematics
03A05	Philosophical and critical aspects of logic and foundations

Keywords:

proof theory; finitism; Hilbert’s programme; Kreisel’s programme; non-finitist proofs; interpretation; no counterexample interpretation; Littlewood’s theorem; finiteness theorems