From Foundations to Science: Justifying and Unwinding Proofs

Georg Kreisel

The first part of this paper recapitulates the general scheme of using techniques developed for discredited foundational aims; specifically, proof theoretic techniques developed for carrying out HiIbert's programme. Since this programme relies on formalization, that is, mechanization, an obvious use is in the mechanical 'handling' of proofs. - The second part of the paper considers three different kinds of 'handling:' finding, checking and unwinding (transforming) proofs. The principal, generally neglected conclusion is that mechanical unwinding presents the most promising application of proof theoretic techniques; particularly where the passage from the informal proof considered to a formalization of its relevant features is not particularly problematic. Examples of such cases are proposed.