from PART TWO - The Age of Reason
Published online by Cambridge University Press: 05 May 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.
To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.
Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.
Find out more about the Kindle Personal Document Service.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.