Constructive Proofs and Algorithms
Gilles Dowek · Cambridge University Press eBooks · 2015
what does the notion of constructive proof have to do with the subject of this book, namely computation? The notions of computation and algorithm did not originally play such an important part in the theory of constructivity as in, say, the theory of computability. However, behind the notion of constructive proof lay the notion of algorithm. CUT ELIMINATION We have seen that proofs of existence resting on the principle of excluded middle do not always contain a witness. On the other hand, a proof of existence that does not use the excluded middle always seems to contain one, either explicitly or implicitly. Is it always so, and can this be demonstrated? Naturally, the possibility of finding a witness in a proof does not depend solely on whether the demonstration uses the excluded middle; it also depends on the axioms used. For example, an axiom of the form “there exists …” is a proof of existence in itself, yet this proof produces no witness. The question of the presence or absence of witnesses in proofs that do not use the excluded middle thus branches into as many questions as there are theories – arithmetic, geometry, Church's type theory, set theory, and, to begin with, the simplest of all theories: the axiom-free theory. One of the first demonstrations that a proof of existence constructed without calling upon the principle of excluded middle always includes a witness (at least implicitly) rests on an algorithm put forward in 1935 by Gerhard Gentzen, called the “cut elimination algorithm.” This algorithm, unlike those we have mentioned up to this point, is not applied to numbers, functional expressions, or computation rules – it is applied to proofs. A proof can contain convoluted arguments, which are called “cuts.”Gentzen's algorithm aims at eliminating those cuts by reorganizing the proof in a more straightforward way.