From Foundations to Science: Justifying and Unwinding Proofs
Zbornik radova, Tome 2 (1977) no. 10, p. 63
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.
@article{ZR_1977_2_10_a4,
author = {Georg Kreisel},
title = {From {Foundations} to {Science:} {Justifying} and {Unwinding} {Proofs}},
journal = {Zbornik radova},
pages = {63 },
year = {1977},
volume = {2},
number = {10},
language = {en},
url = {http://geodesic.mathdoc.fr/item/ZR_1977_2_10_a4/}
}
Georg Kreisel. From Foundations to Science: Justifying and Unwinding Proofs. Zbornik radova, Tome 2 (1977) no. 10, p. 63 . http://geodesic.mathdoc.fr/item/ZR_1977_2_10_a4/